PL1/InterpolationBochner.lean

All source files · Download exact source

SHA-256: d541cf01bb4897f6a83de228f65f0b65106943d513c74f4b5e3d77bfd16e4eca

1import PL1.MainInterpolation2import PL1.KFunctionalIntegralMeasurable34/-! # The interpolation norm as the ordinary integrable real density -/56noncomputable section7open MeasureTheory Filter8open scoped ENNReal NNReal910namespace PL1.Interpolation11open Noise Walsh IntrinsicGraph1213variable (K : Type*) [RCLike K] (rates : ℕ → ℝ≥0)1415theorem mem_intrinsic_iff_integrable (f : Lp K 1 haar) :16    f ∈ (evalZero (dyadicSystem K rates).analysis).range ↔17      IntegrableOn (fun t : ℝ => t ^ (-3 / 2 : ℝ) * KFunctional.value K rates t f)18        (Set.Ioi (0 : ℝ)) := by19  rw [mem_intrinsic_iff, normIntegral_eq, lt_top_iff_ne_top,20    KFunctional.continuousNorm_ne_top_iff_integrableDensity]2122theorem density_nonneg_ae (f : Lp K 1 haar) :23    0 ≤ᵐ[volume.restrict (Set.Ioi (0 : ℝ))]24      (fun t : ℝ => t ^ (-3 / 2 : ℝ) * KFunctional.value K rates t f) := by25  filter_upwards [ae_restrict_mem measurableSet_Ioi] with t ht26  have ht0 : 0 ≤ t := (Set.mem_Ioi.mp ht).le27  exact mul_nonneg (Real.rpow_nonneg ht0 _) (KFunctional.value_nonneg K rates ht0 f)2829/-- On the finite domain, the norm is the ordinary real integral from the paper. -/30theorem normValue_eq_integral (x : (dyadicSystem K rates).IntrinsicSpace) :31    normValue K rates (evalZero (dyadicSystem K rates).analysis x) =32      ∫ t in Set.Ioi (0 : ℝ), t ^ (-3 / 2 : ℝ) *33        KFunctional.value K rates t (evalZero (dyadicSystem K rates).analysis x) := by34  let f := evalZero (dyadicSystem K rates).analysis x35  have hi := (mem_intrinsic_iff_integrable K rates f).mp ⟨x, rfl⟩36  have he := ofReal_integral_eq_lintegral_ofReal hi (density_nonneg_ae K rates f)37  rw [normValue, normIntegral_eq]38  change (KFunctional.continuousNorm K rates f).toReal = _39  change ENNReal.ofReal (∫ t in Set.Ioi (0 : ℝ),40    t ^ (-3 / 2 : ℝ) * KFunctional.value K rates t f) = KFunctional.continuousNorm K rates f at he41  rw [← he, ENNReal.toReal_ofReal (integral_nonneg_of_ae (density_nonneg_ae K rates f))]4243end PL1.Interpolation44