PL1/KFunctionalNormLaws.lean

All source files · Download exact source

SHA-256: 23aa82464ff958ef57929a1743f42dab0b73d7256b8cfd87c80e2d6084b5ff66

1import PL1.KFunctionalIntegralMeasurable2import PL1.KFunctionalProperties34/-! Norm laws for the actual extended continuous interpolation integral. -/56noncomputable section7open MeasureTheory Set Filter8open scoped ENNReal NNReal910namespace PL1.KFunctional11open Noise Walsh1213variable (K : Type*) [RCLike K] (rates : ℕ → ℝ≥0)1415@[simp] theorem continuousNorm_zero : continuousNorm K rates 0 = 0 := by16  unfold continuousNorm17  calc18    _ = ∫⁻ _t in Ioi (0 : ℝ), (0 : ℝ≥0∞) := by19      apply setLIntegral_congr_fun measurableSet_Ioi20      intro t ht21      dsimp only22      rw [value_zero K rates (Set.mem_Ioi.mp ht).le, mul_zero, ENNReal.ofReal_zero]23    _ = 0 := by simp2425theorem continuousNorm_smul (a : K) (f : Lp K 1 haar) :26    continuousNorm K rates (a • f) = ENNReal.ofReal ‖a‖ * continuousNorm K rates f := by27  unfold continuousNorm28  calc29    _ = ∫⁻ t in Ioi (0 : ℝ), ENNReal.ofReal ‖a‖ *30        ENNReal.ofReal (t ^ (-3 / 2 : ℝ) * value K rates t f) := by31      apply setLIntegral_congr_fun measurableSet_Ioi32      intro t ht33      dsimp only34      rw [value_smul K rates (Set.mem_Ioi.mp ht).le]35      rw [show t ^ (-3 / 2 : ℝ) * (‖a‖ * value K rates t f) =36        ‖a‖ * (t ^ (-3 / 2 : ℝ) * value K rates t f) by ring,37        ENNReal.ofReal_mul (norm_nonneg a)]38    _ = _ := lintegral_const_mul' _ _ ENNReal.ofReal_ne_top3940theorem continuousNorm_add_le (f g : Lp K 1 haar) :41    continuousNorm K rates (f + g) ≤ continuousNorm K rates f + continuousNorm K rates g := by42  have h : (fun t : ℝ => ENNReal.ofReal (t ^ (-3 / 2 : ℝ) * value K rates t (f + g)))43      ≤ᵐ[volume.restrict (Ioi (0 : ℝ))]44      (fun t => ENNReal.ofReal (t ^ (-3 / 2 : ℝ) * value K rates t f) +45        ENNReal.ofReal (t ^ (-3 / 2 : ℝ) * value K rates t g)) := by46    filter_upwards [ae_restrict_mem measurableSet_Ioi] with t ht47    have ht0 : 0 ≤ t := (Set.mem_Ioi.mp ht).le48    have hp := Real.rpow_nonneg ht0 (-3 / 2 : ℝ)49    rw [← ENNReal.ofReal_add (mul_nonneg hp (value_nonneg K rates ht0 f))50      (mul_nonneg hp (value_nonneg K rates ht0 g)), ← mul_add]51    exact ENNReal.ofReal_le_ofReal52      (mul_le_mul_of_nonneg_left (value_add_le K rates ht0 f g) hp)53  have hi := lintegral_mono_ae h54  rw [lintegral_add_left' (interpolationDensity_aemeasurable K rates f)] at hi55  exact hi5657theorem two_norm_le_continuousNorm (f : Lp K 1 haar) :58    ENNReal.ofReal (2 * ‖f‖) ≤ continuousNorm K rates f := by59  change ENNReal.ofReal (2 * ‖f‖) ≤60    DyadicInterpolation.fullIntegral (fun t => value K rates t f)61  rw [DyadicInterpolation.fullIntegral_eq (norm_nonneg f)62    (fun _ ht => value_eq_norm_of_one_le K rates ht f)]63  exact le_add_self6465@[simp] theorem continuousNorm_eq_zero_iff (f : Lp K 1 haar) :66    continuousNorm K rates f = 0 ↔ f = 0 := by67  constructor68  · intro hf69    have h := two_norm_le_continuousNorm K rates f70    rw [hf] at h71    have hn := ENNReal.ofReal_eq_zero.mp (le_antisymm h bot_le)72    apply norm_eq_zero.mp73    linarith [norm_nonneg f]74  · rintro rfl75    exact continuousNorm_zero K rates7677end PL1.KFunctional78