PL1/LpOperatorLift.lean
All source files · Download exact source
SHA-256: 90225ac1ee2431b444b4f1461a4c21fc5b85fead1e92e6e6ce51cca00d679f28
1import PL1.LpInterpolation2import PL1.OperatorDomination34noncomputable section5open MeasureTheory6open scoped ENNReal78namespace PL1.LpInterpolation910variable {𝕜 F Ω : Type*} [RCLike 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F]11 [MeasurableSpace Ω] {μ : Measure Ω}1213theorem ae_norm_le_mul_of_unit_bound (V : F →L[𝕜] Lp 𝕜 1 μ)14 (M : ℝ) (_hM : 0 ≤ M)15 (hunit : ∀ f, ‖f‖ ≤ 1 → ∀ᵐ x ∂μ, ‖V f x‖ ≤ M) (f : F) :16 ∀ᵐ x ∂μ, ‖V f x‖ ≤ M * ‖f‖ := by17 by_cases hf : f = 018 · subst f19 filter_upwards [Lp.coeFn_zero (E := 𝕜) (p := 1) (μ := μ)] with x hx20 simp only [map_zero, hx, Pi.zero_apply, norm_zero, mul_zero, le_refl]21 have hfn : ‖f‖ ≠ 0 := norm_ne_zero_iff.mpr hf22 let g : F := ((‖f‖⁻¹ : ℝ) : 𝕜) • f23 have hg : ‖g‖ = 1 := by24 simp only [g, norm_smul, RCLike.norm_ofReal,25 abs_of_nonneg (inv_nonneg.mpr (norm_nonneg f)), inv_mul_cancel₀ hfn]26 have hfg : f = (‖f‖ : 𝕜) • g := by27 dsimp [g]28 rw [smul_smul, ← RCLike.ofReal_mul, mul_inv_cancel₀ hfn, RCLike.ofReal_one, one_smul]29 have hV : V f = (‖f‖ : 𝕜) • V g :=30 (congrArg V hfg).trans (map_smul V (‖f‖ : 𝕜) g)31 filter_upwards [hunit g hg.le, Lp.coeFn_smul (‖f‖ : 𝕜) (V g)] with x hx hsmul32 rw [hV, hsmul, Pi.smul_apply, norm_smul, RCLike.norm_ofReal,33 abs_of_nonneg (norm_nonneg f)]34 simpa only [mul_comm] using mul_le_mul_of_nonneg_left hx (norm_nonneg f)3536variable (V : F →L[𝕜] Lp 𝕜 1 μ) (p : ℝ≥0∞) (hp : 1 ≤ p) (hptop : p ≠ ∞)37 [Fact (1 ≤ p)] (M : ℝ) (hM : 0 ≤ M)38 (hunit : ∀ f, ‖f‖ ≤ 1 → ∀ᵐ x ∂μ, ‖V f x‖ ≤ M)3940def boundedLiftFun (f : F) : Lp 𝕜 p μ :=41 (memLp_of_ae_norm_bound (V f) p hp hptop (M * ‖f‖)42 (ae_norm_le_mul_of_unit_bound V M hM hunit f)).toLp (V f)4344omit [Fact (1 ≤ p)] in45theorem coeFn_boundedLiftFun (f : F) : boundedLiftFun V p hp hptop M hM hunit f =ᵐ[μ] V f :=46 MemLp.coeFn_toLp _4748omit [Fact (1 ≤ p)] in49theorem boundedLiftFun_add (f g : F) :50 boundedLiftFun V p hp hptop M hM hunit (f + g) =51 boundedLiftFun V p hp hptop M hM hunit f + boundedLiftFun V p hp hptop M hM hunit g := by52 apply Lp.ext53 filter_upwards [coeFn_boundedLiftFun V p hp hptop M hM hunit (f + g),54 coeFn_boundedLiftFun V p hp hptop M hM hunit f,55 coeFn_boundedLiftFun V p hp hptop M hM hunit g,56 Lp.coeFn_add (V f) (V g),57 Lp.coeFn_add (boundedLiftFun V p hp hptop M hM hunit f)58 (boundedLiftFun V p hp hptop M hM hunit g)] with x hfg hf hg hv hl59 rw [hfg, map_add, hv, hl, Pi.add_apply, Pi.add_apply, hf, hg]6061omit [Fact (1 ≤ p)] in62theorem boundedLiftFun_smul (c : 𝕜) (f : F) :63 boundedLiftFun V p hp hptop M hM hunit (c • f) =64 c • boundedLiftFun V p hp hptop M hM hunit f := by65 apply Lp.ext66 filter_upwards [coeFn_boundedLiftFun V p hp hptop M hM hunit (c • f),67 coeFn_boundedLiftFun V p hp hptop M hM hunit f,68 Lp.coeFn_smul c (V f),69 Lp.coeFn_smul c (boundedLiftFun V p hp hptop M hM hunit f)] with x hcf hf hv hl70 rw [hcf, map_smul, hv, hl, Pi.smul_apply, Pi.smul_apply, hf]7172omit [Fact (1 ≤ p)] in73theorem norm_boundedLiftFun_le (f : F) :74 ‖boundedLiftFun V p hp hptop M hM hunit f‖ ≤ (M + ‖V‖) * ‖f‖ := by75 have hpR : (1 : ℝ) ≤ p.toReal := by simpa using ENNReal.toReal_mono hptop hp76 have hp0 : 0 < p.toReal := lt_of_lt_of_le zero_lt_one hpR77 let C : ℝ := (M + ‖V‖) * ‖f‖78 have hC : 0 ≤ C := mul_nonneg (add_nonneg hM (norm_nonneg V)) (norm_nonneg f)79 have hpoint : ∀ᵐ x ∂μ, ‖V f x‖ₑ ≤ ENNReal.ofReal C := by80 filter_upwards [ae_norm_le_mul_of_unit_bound V M hM hunit f] with x hx81 have hle : ‖V f x‖ ≤ C := hx.trans (by dsimp [C]; gcongr; exact le_add_of_nonneg_right (norm_nonneg V))82 simpa only [ofReal_norm] using ENNReal.ofReal_le_ofReal hle83 have hL1 : eLpNorm (V f) 1 μ ≤ ENNReal.ofReal C := by84 rw [← Lp.enorm_def, ← ofReal_norm]85 apply ENNReal.ofReal_le_ofReal86 exact (V.le_opNorm f).trans (by dsimp [C]; gcongr; exact le_add_of_nonneg_left hM)87 have hb := eLpNorm_le_of_ae_bound (V f) (Lp.aestronglyMeasurable (V f))88 p hp hptop (ENNReal.ofReal C) (ENNReal.ofReal C) hpoint hL189 rw [← ENNReal.rpow_add_of_nonneg _ _90 (sub_nonneg.mpr ((div_le_one hp0).mpr hpR)) (by positivity), sub_add_cancel, ENNReal.rpow_one] at hb91 have h := ENNReal.toReal_mono ENNReal.ofReal_ne_top hb92 simpa only [boundedLiftFun, Lp.norm_toLp, ENNReal.toReal_ofReal hC] using h9394/-- A continuous linear Lp lift of an L1-valued operator whose unit-ball95images have a common essential bound. -/96def boundedLift : F →L[𝕜] Lp 𝕜 p μ :=97 LinearMap.mkContinuous98 { toFun := boundedLiftFun V p hp hptop M hM hunit99 map_add' := boundedLiftFun_add V p hp hptop M hM hunit100 map_smul' := boundedLiftFun_smul V p hp hptop M hM hunit }101 (M + ‖V‖) (norm_boundedLiftFun_le V p hp hptop M hM hunit)102103theorem coeFn_boundedLift (f : F) : boundedLift V p hp hptop M hM hunit f =ᵐ[μ] V f :=104 coeFn_boundedLiftFun V p hp hptop M hM hunit f105106theorem norm_boundedLift_apply_le (f : F) :107 ‖boundedLift V p hp hptop M hM hunit f‖ ≤108 (M * ‖f‖) ^ (1 - 1 / p.toReal) * ‖V f‖ ^ (1 / p.toReal) :=109 norm_toLp_le_of_ae_norm_bound (V f) p hp hptop (M * ‖f‖)110 (mul_nonneg hM (norm_nonneg f)) (ae_norm_le_mul_of_unit_bound V M hM hunit f)111 (memLp_of_ae_norm_bound (V f) p hp hptop (M * ‖f‖)112 (ae_norm_le_mul_of_unit_bound V M hM hunit f))113114theorem norm_boundedLift_apply_le_of_norm_le_one (f : F) (hf : ‖f‖ ≤ 1) :115 ‖boundedLift V p hp hptop M hM hunit f‖ ≤116 M ^ (1 - 1 / p.toReal) * ‖V f‖ ^ (1 / p.toReal) :=117 norm_toLp_le_of_ae_norm_bound (V f) p hp hptop M hM (hunit f hf)118 (memLp_of_ae_norm_bound (V f) p hp hptop (M * ‖f‖)119 (ae_norm_le_mul_of_unit_bound V M hM hunit f))120121theorem norm_boundedLift_le : ‖boundedLift V p hp hptop M hM hunit‖ ≤ M + ‖V‖ :=122 ContinuousLinearMap.opNorm_le_bound _ (add_nonneg hM (norm_nonneg V))123 (norm_boundedLiftFun_le V p hp hptop M hM hunit)124125end PL1.LpInterpolation126127namespace PL1.OperatorDomination128129variable {𝕜 Ω : Type*} [RCLike 𝕜] [MeasurableSpace Ω] (μ : Measure Ω)130variable (B : IntervalL1 𝕜 →L[𝕜] Lp 𝕜 1 μ)131 (G : Ω → ℝ) (hG : Measurable G)132 (hdom : ∀ f : Lp 𝕜 ∞ intervalMeasure, ‖f‖ ≤ 1 →133 ∀ᵐ x ∂μ, ‖restriction μ B f x‖ ≤ G x)134 (p : ℝ≥0∞) (hp : 1 ≤ p) (hptop : p ≠ ∞) [Fact (1 ≤ p)]135 (M : ℝ) (hM : 0 ≤ M)136137def maskedRestriction : Lp 𝕜 ∞ intervalMeasure →L[𝕜] Lp 𝕜 1 μ :=138 (L1Masks.mask μ {x | G x ≤ M} (measurableSet_le hG measurable_const)).comp (restriction μ B)139140include hdom hM in141omit [Fact (1 ≤ p)] in142theorem maskedRestriction_unit_bound (f : Lp 𝕜 ∞ intervalMeasure) (hf : ‖f‖ ≤ 1) :143 ∀ᵐ x ∂μ, ‖maskedRestriction μ B G hG M f x‖ ≤ M := by144 filter_upwards [hdom f hf, L1Masks.coeFn_mask μ {x | G x ≤ M}145 (measurableSet_le hG measurable_const) (restriction μ B f)] with x hx hm146 change ‖L1Masks.mask μ {x | G x ≤ M} (measurableSet_le hG measurable_const)147 (restriction μ B f) x‖ ≤ M148 rw [hm]149 by_cases h : G x ≤ M150 · simpa only [Set.indicator_of_mem (show x ∈ {x | G x ≤ M} from h)] using hx.trans h151 · simpa only [Set.indicator_of_notMem (show x ∉ {x | G x ≤ M} from h), norm_zero] using hM152153/-- The measurable target cutoff lifts the restricted operator genuinely to154Lp. The source is L-infinity, as required by the domination theorem. -/155def maskedRestrictionLp : Lp 𝕜 ∞ intervalMeasure →L[𝕜] Lp 𝕜 p μ :=156 LpInterpolation.boundedLift (maskedRestriction μ B G hG M) p hp hptop M hM157 (maskedRestriction_unit_bound μ B G hG hdom M hM)158159theorem coeFn_maskedRestrictionLp (f : Lp 𝕜 ∞ intervalMeasure) :160 maskedRestrictionLp μ B G hG hdom p hp hptop M hM f =ᵐ[μ]161 maskedRestriction μ B G hG M f :=162 LpInterpolation.coeFn_boundedLift _ _ _ _ _ _ _ f163164theorem norm_maskedRestrictionLp_apply_le (f : Lp 𝕜 ∞ intervalMeasure) (hf : ‖f‖ ≤ 1) :165 ‖maskedRestrictionLp μ B G hG hdom p hp hptop M hM f‖ ≤166 M ^ (1 - 1 / p.toReal) * ‖maskedRestriction μ B G hG M f‖ ^ (1 / p.toReal) :=167 LpInterpolation.norm_boundedLift_apply_le_of_norm_le_one _ _ _ _ _ _ _ f hf168169end PL1.OperatorDomination170