PL1/KernelL1.lean

All source files · Download exact source

SHA-256: af4c0f2f2e8110b44ee124faf455db4b31f9993bb8f3253147beaca60c167aa9

1import PL1.WeightedL12import Mathlib.Probability.Kernel.Composition.IntegralCompProd34noncomputable section5open MeasureTheory ProbabilityTheory Set Filter6open scoped ENNReal NNReal Topology ProbabilityTheory78namespace PL1.KernelL1910variable {𝕜 α β : Type*} [RCLike 𝕜] [MeasurableSpace α] [MeasurableSpace β]11variable (μ : Measure α) (ν : Measure β) (κ : Kernel α β)12variable [IsMarkovKernel κ] (hcomp : κ ∘ₘ μ = ν)1314/-- Integrate the genuine L1 representative against the transition probability. -/15def averageFunction (u : Lp 𝕜 1 ν) (x : α) : 𝕜 := ∫ y, u y ∂κ x1617include hcomp1819theorem integrable_comp (u : Lp 𝕜 1 ν) : Integrable (u : β → 𝕜) (κ ∘ₘ μ) := by20  rw [hcomp]21  exact L1.integrable_coeFn u2223theorem ae_integrable (u : Lp 𝕜 1 ν) : ∀ᵐ x ∂μ, Integrable (u : β → 𝕜) (κ x) :=24  Measure.ae_integrable_of_integrable_comp (integrable_comp μ ν κ hcomp u)2526theorem integrable_averageFunction (u : Lp 𝕜 1 ν) :27    Integrable (averageFunction ν κ u) μ := by28  apply Integrable.mono'29    (Measure.integrable_integral_norm_of_integrable_comp (integrable_comp μ ν κ hcomp u))30    (Lp.stronglyMeasurable u).integral_kernel.aestronglyMeasurable31  exact ae_of_all _ (fun x => norm_integral_le_integral_norm _)3233/-- The L1 class of integration against a probability kernel. -/34def average (u : Lp 𝕜 1 ν) : Lp 𝕜 1 μ :=35  (integrable_averageFunction μ ν κ hcomp u).toL1 _3637theorem average_coeFn (u : Lp 𝕜 1 ν) :38    (average μ ν κ hcomp u : α → 𝕜) =ᵐ[μ] averageFunction ν κ u :=39  (integrable_averageFunction μ ν κ hcomp u).coeFn_toL14041theorem norm_average_le (u : Lp 𝕜 1 ν) : ‖average μ ν κ hcomp u‖ ≤ ‖u‖ := by42  rw [L1.norm_eq_integral_norm, L1.norm_eq_integral_norm]43  calc44    (∫ x, ‖average μ ν κ hcomp u x‖ ∂μ) = ∫ x, ‖averageFunction ν κ u x‖ ∂μ :=45      integral_congr_ae ((average_coeFn μ ν κ hcomp u).fun_comp norm)46    _ ≤ ∫ x, ∫ y, ‖u y‖ ∂κ x ∂μ :=47      integral_mono (integrable_averageFunction μ ν κ hcomp u).norm48        (Measure.integrable_integral_norm_of_integrable_comp (integrable_comp μ ν κ hcomp u))49        (fun x => norm_integral_le_integral_norm _)50    _ = ∫ y, ‖u y‖ ∂ν := by51      have h := ProbabilityTheory.Kernel.integral_comp52        (κ := Kernel.const Unit μ) (η := κ) (a := ())53        (f := fun y => ‖u y‖)54        (by simpa [← Measure.comp_eq_comp_const_apply] using (integrable_comp μ ν κ hcomp u).norm)55      simpa [← Measure.comp_eq_comp_const_apply, hcomp] using h.symm5657theorem average_add (u v : Lp 𝕜 1 ν) :58    average μ ν κ hcomp (u + v) = average μ ν κ hcomp u + average μ ν κ hcomp v := by59  apply Lp.ext60  have huv : ∀ᵐ x ∂μ, (u + v : Lp 𝕜 1 ν) =ᵐ[κ x] (fun y => u y + v y) := by61    apply Measure.ae_ae_of_ae_comp62    rw [hcomp]63    exact Lp.coeFn_add u v64  filter_upwards [average_coeFn μ ν κ hcomp (u + v), average_coeFn μ ν κ hcomp u,65    average_coeFn μ ν κ hcomp v, Lp.coeFn_add (average μ ν κ hcomp u) (average μ ν κ hcomp v),66    ae_integrable μ ν κ hcomp u, ae_integrable μ ν κ hcomp v, huv] with x ha hu hv hab hui hvi huvx67  rw [ha, hab, Pi.add_apply, hu, hv]68  exact (integral_congr_ae huvx).trans (integral_add hui hvi)6970theorem average_smul (c : 𝕜) (u : Lp 𝕜 1 ν) :71    average μ ν κ hcomp (c • u) = c • average μ ν κ hcomp u := by72  apply Lp.ext73  have hcu : ∀ᵐ x ∂μ, (c • u : Lp 𝕜 1 ν) =ᵐ[κ x] (fun y => c • u y) := by74    apply Measure.ae_ae_of_ae_comp75    rw [hcomp]76    exact Lp.coeFn_smul c u77  filter_upwards [average_coeFn μ ν κ hcomp (c • u), average_coeFn μ ν κ hcomp u,78    Lp.coeFn_smul c (average μ ν κ hcomp u), hcu] with x ha hu hsm hcx79  rw [ha, hsm, Pi.smul_apply, hu]80  exact (integral_congr_ae hcx).trans (integral_smul c _)8182/-- A probability kernel whose average measure is ν induces a contraction L1(ν)→L1(μ). -/83def averageCLM : Lp 𝕜 1 ν →L[𝕜] Lp 𝕜 1 μ :=84  LinearMap.mkContinuous85    { toFun := average μ ν κ hcomp86      map_add' := average_add μ ν κ hcomp87      map_smul' := by intro c u; exact average_smul μ ν κ hcomp c u }88    1 (by intro u; simpa using norm_average_le μ ν κ hcomp u)8990@[simp] theorem averageCLM_apply (u : Lp 𝕜 1 ν) :91    averageCLM μ ν κ hcomp u = average μ ν κ hcomp u := rfl9293theorem norm_averageCLM_le : ‖averageCLM (𝕜 := 𝕜) μ ν κ hcomp‖ ≤ 1 :=94  ContinuousLinearMap.opNorm_le_bound _ (by norm_num)95    (fun u => by simpa using norm_average_le μ ν κ hcomp u)9697end PL1.KernelL19899100