PL1/KFunctionalIntegral.lean

All source files · Download exact source

SHA-256: d87b021ea07a588a3689aeebb6ea1e4c92f6e4973d1e7f9438aff7a2e4610f79

1import PL1.DyadicInterpolationNormComparison2import PL1.ExtendedDiscreteInterpolation34/-!5# Continuous interpolation integral for the actual generator graph67This is the usual real interpolation integral at parameters theta = 1/28and q = 1: the Lebesgue density is t^(-3/2) times the actual K-functional.9The extended value retains infinity outside the interpolation space.10-/1112noncomputable section13open MeasureTheory Set14open scoped ENNReal NNReal1516namespace PL1.KFunctional17open Noise Walsh ResolventEstimates DyadicInterpolation1819variable (K : Type*) [RCLike K] (rates : ℕ → ℝ≥0)2021def continuousNorm (f : Lp K 1 haar) : ℝ≥0∞ :=22  ∫⁻ t in Ioi (0 : ℝ), ENNReal.ofReal (t ^ (-3 / 2 : ℝ) * value K rates t f)2324theorem time_eq_dyadicTime (n : ℕ) : time n = (dyadicTime n : ℝ) := by25  simp only [time, dyadicTime, dyadicRatio_sq]2627theorem weight_eq_dyadicRatio (n : ℕ) : weight n = (dyadicRatio ^ n)⁻¹ := by28  rw [weight_eq_sqrt_two_pow]29  simp [dyadicRatio, inv_pow]3031theorem sample_eq_term (f : Lp K 1 haar) (n : ℕ) :32    sample (fun t => value K rates t f) (n + 1) =33      ENNReal.ofReal (DiscreteInterpolation.term K rates f n) := by34  rw [sample, weight_eq_dyadicRatio, time_eq_dyadicTime]35  rfl3637theorem discreteNorm_eq_extendedNorm (f : Lp K 1 haar) :38    discreteNorm (fun t => value K rates t f) = DiscreteInterpolation.extendedNorm K rates f := by39  simp only [discreteNorm, DiscreteInterpolation.extendedNorm, sample_eq_term,40    value_eq_norm_of_one_le K rates le_rfl]4142theorem tail_integral_eq (f : Lp K 1 haar) :43    (∫⁻ t in Ioi (1 : ℝ), ENNReal.ofReal (t ^ (-3 / 2 : ℝ) * value K rates t f)) =44      ENNReal.ofReal (2 * ‖f‖) :=45  tailIntegral_eq (norm_nonneg f) (fun _ ht => value_eq_norm_of_one_le K rates ht f)4647theorem continuousNorm_le_four_extendedNorm (f : Lp K 1 haar) :48    continuousNorm K rates f ≤ 4 * DiscreteInterpolation.extendedNorm K rates f := by49  rw [← discreteNorm_eq_extendedNorm]50  exact fullIntegral_le_four_discreteNorm51    (fun _ ht => value_nonneg K rates ht f) (monotoneOn_value K rates f)52    (fun t ht => (value_eq_norm_of_one_le K rates ht f).trans53      (value_eq_norm_of_one_le K rates le_rfl f).symm)5455theorem extendedNorm_le_five_continuousNorm (f : Lp K 1 haar) :56    DiscreteInterpolation.extendedNorm K rates f ≤ 5 * continuousNorm K rates f := by57  rw [← discreteNorm_eq_extendedNorm]58  exact discreteNorm_le_five_fullIntegral59    (fun _ ht => value_nonneg K rates ht f) (monotoneOn_value K rates f)60    (fun t ht => (value_eq_norm_of_one_le K rates ht f).trans61      (value_eq_norm_of_one_le K rates le_rfl f).symm)6263theorem continuousNorm_ne_top_iff (f : Lp K 1 haar) :64    continuousNorm K rates f ≠ ⊤ ↔ DiscreteInterpolation.extendedNorm K rates f ≠ ⊤ := by65  rw [← discreteNorm_eq_extendedNorm]66  exact fullIntegral_ne_top_iff_discreteNorm67    (fun _ ht => value_nonneg K rates ht f) (monotoneOn_value K rates f)68    (fun t ht => (value_eq_norm_of_one_le K rates ht f).trans69      (value_eq_norm_of_one_le K rates le_rfl f).symm)7071end PL1.KFunctional72