PL1/LpInclusions.lean

All source files · Download exact source

SHA-256: 43f4184579314ad6e16caef67bc709030cdce810c064e958eb6e0c70b8413849

1import PL1.WalshModel2import Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp34/-! # Canonical contractive inclusions between Lp spaces on a probability space -/56noncomputable section7open MeasureTheory8open scoped ENNReal910namespace PL111namespace ProbabilityLp1213variable {𝕜 : Type*} [RCLike 𝕜]14variable {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ]15variable (p q : ℝ≥0∞) [Fact (1 ≤ p)] [Fact (1 ≤ q)] (hpq : p ≤ q)1617def inclusionFun (f : Lp 𝕜 q μ) : Lp 𝕜 p μ :=18  ((Lp.memLp f).mono_exponent hpq).toLp f1920theorem coeFn_inclusionFun (f : Lp 𝕜 q μ) : inclusionFun μ p q hpq f =ᵐ[μ] f :=21  ((Lp.memLp f).mono_exponent hpq).coeFn_toLp2223theorem inclusionFun_add (f g : Lp 𝕜 q μ) :24    inclusionFun μ p q hpq (f + g) = inclusionFun μ p q hpq f + inclusionFun μ p q hpq g := by25  apply Lp.ext26  filter_upwards [coeFn_inclusionFun μ p q hpq (f + g), coeFn_inclusionFun μ p q hpq f,27    coeFn_inclusionFun μ p q hpq g, Lp.coeFn_add f g,28    Lp.coeFn_add (inclusionFun μ p q hpq f) (inclusionFun μ p q hpq g)]29      with x hfg hf hg hadd hadd'30  simp only [hfg, hadd, hadd', Pi.add_apply, hf, hg]3132theorem inclusionFun_smul (c : 𝕜) (f : Lp 𝕜 q μ) :33    inclusionFun μ p q hpq (c • f) = c • inclusionFun μ p q hpq f := by34  apply Lp.ext35  filter_upwards [coeFn_inclusionFun μ p q hpq (c • f), coeFn_inclusionFun μ p q hpq f,36    Lp.coeFn_smul c f, Lp.coeFn_smul c (inclusionFun μ p q hpq f)] with x hcf hf hsmul hsmul'37  simp only [hcf, hsmul, hsmul', Pi.smul_apply, hf]3839theorem norm_inclusionFun_le (f : Lp 𝕜 q μ) : ‖inclusionFun μ p q hpq f‖ ≤ ‖f‖ := by40  rw [Lp.norm_def, Lp.norm_def, eLpNorm_congr_ae (coeFn_inclusionFun μ p q hpq f)]41  exact ENNReal.toReal_mono (Lp.memLp f).2.ne42    (eLpNorm_le_eLpNorm_of_exponent_le hpq (Lp.aestronglyMeasurable f))4344def inclusion : Lp 𝕜 q μ →L[𝕜] Lp 𝕜 p μ :=45  LinearMap.mkContinuous46    { toFun := inclusionFun μ p q hpq47      map_add' := inclusionFun_add μ p q hpq48      map_smul' := inclusionFun_smul μ p q hpq }49    1 (fun f => by50      change ‖inclusionFun μ p q hpq f‖ ≤ 1 * ‖f‖51      simpa only [one_mul] using norm_inclusionFun_le μ p q hpq f)5253theorem coeFn_inclusion (f : Lp 𝕜 q μ) : inclusion μ p q hpq f =ᵐ[μ] f :=54  coeFn_inclusionFun μ p q hpq f5556theorem norm_inclusion_le_one : ‖inclusion (𝕜 := 𝕜) μ p q hpq‖ ≤ 1 := by57  apply ContinuousLinearMap.opNorm_le_bound _ zero_le_one58  intro f59  change ‖inclusionFun μ p q hpq f‖ ≤ 1 * ‖f‖60  simpa only [one_mul] using norm_inclusionFun_le μ p q hpq f6162theorem inclusion_toLp {f : Ω → 𝕜} (hf : MemLp f q μ) :63    inclusion μ p q hpq (hf.toLp f) = (hf.mono_exponent hpq).toLp f := by64  apply Lp.ext65  exact (coeFn_inclusion μ p q hpq _).trans66    (hf.coeFn_toLp.trans (hf.mono_exponent hpq).coeFn_toLp.symm)6768theorem inclusion_comp (r : ℝ≥0∞) [Fact (1 ≤ r)] (hqr : q ≤ r) :69    (inclusion (𝕜 := 𝕜) μ p q hpq).comp (inclusion μ q r hqr) =70      inclusion μ p r (hpq.trans hqr) := by71  ext f72  exact ((coeFn_inclusion μ p q hpq _).trans (coeFn_inclusion μ q r hqr f)).trans73    (coeFn_inclusion μ p r (hpq.trans hqr) f).symm7475end ProbabilityLp7677namespace Walsh7879variable {𝕜 : Type*} [RCLike 𝕜]8081abbrev l2ToL1 : Lp 𝕜 2 haar →L[𝕜] Lp 𝕜 1 haar :=82  ProbabilityLp.inclusion haar 1 2 (by norm_num)8384abbrev linftyToL2 : Lp 𝕜 ∞ haar →L[𝕜] Lp 𝕜 2 haar :=85  ProbabilityLp.inclusion haar 2 ∞ le_top8687theorem l2ToL1_scalarCharacter (F : Finset ℕ) :88    l2ToL1 (scalarCharacterLp 𝕜 2 F) = scalarCharacterLp 𝕜 1 F :=89  ProbabilityLp.inclusion_toLp haar 1 2 (by norm_num) (memLp_scalarCharacter 𝕜 2 F)9091end Walsh92end PL193