PL1/KFunctionalIntegralMeasurable.lean

All source files · Download exact source

SHA-256: c9a161157634cacc793e72a66451921bd5354ebd6924f027f8d2ce941e3eb039

1import PL1.KFunctionalIntegral2import Mathlib.MeasureTheory.Constructions.BorelSpace.Order34/-! Measurability of the continuous interpolation density on positive time. -/56noncomputable section7open MeasureTheory Set Filter8open scoped ENNReal NNReal910namespace PL1.DyadicInterpolation1112theorem integrand_aemeasurable {k : ℝ → ℝ} (hmono : MonotoneOn k (Ici (0 : ℝ))) :13    AEMeasurable (integrand k) (volume.restrict (Ioi (0 : ℝ))) := by14  have hm : Monotone (fun t : ℝ => k (max t 0)) := by15    intro s t hst16    exact hmono (Set.mem_Ici.mpr (le_max_right s 0))17      (Set.mem_Ici.mpr (le_max_right t 0)) (max_le_max_right 0 hst)18  have hf : Measurable (fun t : ℝ => ENNReal.ofReal (t ^ (-3 / 2 : ℝ) * k (max t 0))) :=19    ENNReal.measurable_ofReal.comp ((measurable_id.pow_const _).mul hm.measurable)20  apply hf.aemeasurable.congr21  filter_upwards [ae_restrict_mem measurableSet_Ioi] with t ht22  simp only [integrand, max_eq_left (Set.mem_Ioi.mp ht).le]2324end PL1.DyadicInterpolation2526namespace PL1.KFunctional27open Noise Walsh2829variable (K : Type*) [RCLike K] (rates : ℕ → ℝ≥0)3031theorem interpolationDensity_aemeasurable (f : Lp K 1 haar) :32    AEMeasurable33      (fun t : ℝ => ENNReal.ofReal (t ^ (-3 / 2 : ℝ) * value K rates t f))34      (volume.restrict (Ioi (0 : ℝ))) :=35  DyadicInterpolation.integrand_aemeasurable (monotoneOn_value K rates f)3637theorem continuousNorm_ne_top_iff_integrableDensity (f : Lp K 1 haar) :38    continuousNorm K rates f ≠ ⊤ ↔39      IntegrableOn (fun t : ℝ => t ^ (-3 / 2 : ℝ) * value K rates t f) (Ioi (0 : ℝ)) := by40  have h := integrable_toReal_iff (interpolationDensity_aemeasurable K rates f)41    (Eventually.of_forall (fun _ => ENNReal.ofReal_ne_top))42  have heq : (fun t : ℝ => (ENNReal.ofReal (t ^ (-3 / 2 : ℝ) * value K rates t f)).toReal)43      =ᵐ[volume.restrict (Ioi (0 : ℝ))] (fun t => t ^ (-3 / 2 : ℝ) * value K rates t f) := by44    filter_upwards [ae_restrict_mem measurableSet_Ioi] with t ht45    have ht0 : 0 ≤ t := (Set.mem_Ioi.mp ht).le46    exact ENNReal.toReal_ofReal47      (mul_nonneg (Real.rpow_nonneg ht0 _) (value_nonneg K rates ht0 f))48  exact h.symm.trans (integrable_congr heq)4950end PL1.KFunctional51