PL1/IntervalRetraction.lean

All source files · Download exact source

SHA-256: d7d0bfa248bd6a870c0fc043fdc5850c5ab8d2134fd4717e2c14956dbaad8f0e

1import PL1.KernelL12import Mathlib.Probability.Kernel.Representation3import Mathlib.Probability.Kernel.CondDistrib45/-!6# A contractive retraction from interval L1 to a standard Borel probability L178A measurable sampler gives the isometric embedding. Its genuine regular9conditional distribution gives the contractive left inverse. This avoids a10separate classification theorem for atomless measure spaces.11-/1213noncomputable section14open MeasureTheory ProbabilityTheory Set Filter15open scoped ENNReal NNReal Topology ProbabilityTheory1617namespace PL1.IntervalRetraction1819variable {𝕜 Y : Type*} [RCLike 𝕜] [MeasurableSpace Y]20  [StandardBorelSpace Y] [Nonempty Y]21variable (μ : Measure Y) [IsProbabilityMeasure μ]2223/-- An actual measurable sampler of μ on the unit interval. -/24def samplingMap : unitInterval → Y := μ.exists_measurable_map_eq.choose2526theorem measurable_samplingMap : Measurable (samplingMap μ) :=27  μ.exists_measurable_map_eq.choose_spec.12829theorem map_samplingMap : (volume : Measure unitInterval).map (samplingMap μ) = μ :=30  μ.exists_measurable_map_eq.choose_spec.23132theorem samplingMap_measurePreserving :33    MeasurePreserving (samplingMap μ) (volume : Measure unitInterval) μ :=34  ⟨measurable_samplingMap μ, map_samplingMap μ⟩3536/-- Isometric pullback along the sampler. -/37def pullback : Lp 𝕜 1 μ →ₗᵢ[𝕜] Lp 𝕜 1 (volume : Measure unitInterval) :=38  Lp.compMeasurePreservingₗᵢ 𝕜 (samplingMap μ) (samplingMap_measurePreserving μ)3940theorem pullback_coeFn (u : Lp 𝕜 1 μ) :41    (pullback μ u : unitInterval → 𝕜) =ᵐ[volume] (fun x => u (samplingMap μ x)) :=42  Lp.coeFn_compMeasurePreserving u (samplingMap_measurePreserving μ)4344/-- The conditional law of the original interval point given its sample. -/45def returnKernel : Kernel Y unitInterval := condDistrib id (samplingMap μ) volume4647instance returnKernel_isMarkovKernel : IsMarkovKernel (returnKernel μ) := by48  unfold returnKernel49  infer_instance5051theorem returnKernel_comp : returnKernel μ ∘ₘ μ = (volume : Measure unitInterval) := by52  have h := condDistrib_comp_map (measurable_samplingMap μ).aemeasurable53    (measurable_id.aemeasurable : AEMeasurable (id : unitInterval → unitInterval) volume)54  simpa only [map_samplingMap, Measure.map_id, returnKernel] using h5556/-- A conditional sample remains in the fiber of the original sample. -/57theorem returnKernel_map_samplingMap :58    (returnKernel μ).map (samplingMap μ) =ᵐ[μ] Kernel.id := by59  have h := condDistrib_comp (measurable_samplingMap μ).aemeasurable60    (measurable_id.aemeasurable : AEMeasurable (id : unitInterval → unitInterval) volume)61    (measurable_samplingMap μ)62  have hs := condDistrib_self (μ := (volume : Measure unitInterval)) (measurable_samplingMap μ).aemeasurable63  rw [map_samplingMap] at h hs64  simpa only [returnKernel, Function.comp_id] using h.symm.trans hs6566/-- Averaging over the conditional law is a genuine contraction. -/67def retraction : Lp 𝕜 1 (volume : Measure unitInterval) →L[𝕜] Lp 𝕜 1 μ :=68  KernelL1.averageCLM μ volume (returnKernel μ) (returnKernel_comp μ)6970theorem norm_retraction_le : ‖retraction (𝕜 := 𝕜) μ‖ ≤ 1 :=71  KernelL1.norm_averageCLM_le μ volume (returnKernel μ) (returnKernel_comp μ)7273theorem retraction_coeFn (u : Lp 𝕜 1 (volume : Measure unitInterval)) :74    (retraction μ u : Y → 𝕜) =ᵐ[μ] (fun y => ∫ x, u x ∂returnKernel μ y) :=75  KernelL1.average_coeFn μ volume (returnKernel μ) (returnKernel_comp μ) u7677/-- The interval averaging operator is a left inverse of isometric pullback. -/78@[simp] theorem retraction_pullback (u : Lp 𝕜 1 μ) : retraction μ (pullback μ u) = u := by79  apply Lp.ext80  have hcoe : ∀ᵐ y ∂μ, (pullback μ u : unitInterval → 𝕜) =ᵐ[returnKernel μ y]81      (fun x => u (samplingMap μ x)) := by82    apply Measure.ae_ae_of_ae_comp83    rw [returnKernel_comp]84    exact pullback_coeFn μ u85  filter_upwards [retraction_coeFn μ (pullback μ u), returnKernel_map_samplingMap μ, hcoe]86    with y hy hmap hcoey87  rw [hy, integral_congr_ae hcoey]88  rw [← integral_map (measurable_samplingMap μ).aemeasurable89    ((Lp.stronglyMeasurable u).aestronglyMeasurable)]90  rw [Kernel.map_apply _ (measurable_samplingMap μ)] at hmap91  rw [hmap]92  change (∫ z, u z ∂Measure.dirac y) = u y93  exact integral_dirac' u y (Lp.stronglyMeasurable u)9495theorem retraction_comp_pullback :96    (retraction (𝕜 := 𝕜) μ).comp (pullback μ).toContinuousLinearMap =97      ContinuousLinearMap.id 𝕜 (Lp 𝕜 1 μ) := by98  apply ContinuousLinearMap.ext99  intro u100  exact retraction_pullback μ u101102end PL1.IntervalRetraction103104105106