PL1/LpInterpolation.lean
All source files · Download exact source
SHA-256: 72b863322fbec8b800b74733bcfa6aa17f434627094ce61356c277da11ac09a0
1import PL1.Definitions23/-! # Elementary L1–L-infinity interpolation45The estimate follows pointwise from t^p ≤ M^(p-1) t. It applies to arbitrary6measures and every finite exponent p ≥ 1.7-/89noncomputable section10open MeasureTheory11open scoped ENNReal1213namespace PL1.LpInterpolation1415variable {Ω E : Type*} [MeasurableSpace Ω] [NormedAddCommGroup E]16 {μ : Measure Ω}1718theorem eLpNorm_le_of_ae_bound (f : Ω → E) (hf : AEStronglyMeasurable f μ)19 (p : ℝ≥0∞) (hp : 1 ≤ p) (hptop : p ≠ ∞) (M b : ℝ≥0∞)20 (hM : ∀ᵐ x ∂μ, ‖f x‖ₑ ≤ M) (hb : eLpNorm f 1 μ ≤ b) :21 eLpNorm f p μ ≤ M ^ (1 - 1 / p.toReal) * b ^ (1 / p.toReal) := by22 have hpR : (1 : ℝ) ≤ p.toReal := by simpa using ENNReal.toReal_mono hptop hp23 have hp0 : 0 < p.toReal := lt_of_lt_of_le zero_lt_one hpR24 have hpne : p ≠ 0 := ne_of_gt (lt_of_lt_of_le zero_lt_one hp)25 have hpow : ∀ᵐ x ∂μ, ‖f x‖ₑ ^ p.toReal ≤ M ^ (p.toReal - 1) * ‖f x‖ₑ := by26 filter_upwards [hM] with x hx27 calc28 ‖f x‖ₑ ^ p.toReal = ‖f x‖ₑ ^ ((p.toReal - 1) + 1) := by rw [sub_add_cancel]29 _ = ‖f x‖ₑ ^ (p.toReal - 1) * ‖f x‖ₑ := by30 rw [ENNReal.rpow_add_of_nonneg _ _ (sub_nonneg.mpr hpR) zero_le_one, ENNReal.rpow_one]31 _ ≤ M ^ (p.toReal - 1) * ‖f x‖ₑ :=32 mul_le_mul_of_nonneg_right (ENNReal.rpow_le_rpow hx (sub_nonneg.mpr hpR)) bot_le33 have hint : (∫⁻ x, ‖f x‖ₑ ^ p.toReal ∂μ) ≤ M ^ (p.toReal - 1) * b := by34 calc35 _ ≤ ∫⁻ x, M ^ (p.toReal - 1) * ‖f x‖ₑ ∂μ := lintegral_mono_ae hpow36 _ = M ^ (p.toReal - 1) * eLpNorm f 1 μ := by37 rw [lintegral_const_mul'' _ hf.enorm, eLpNorm_one_eq_lintegral_enorm]38 _ ≤ M ^ (p.toReal - 1) * b := mul_le_mul_of_nonneg_left hb bot_le39 rw [eLpNorm_eq_lintegral_rpow_enorm_toReal hpne hptop]40 calc41 _ ≤ (M ^ (p.toReal - 1) * b) ^ (1 / p.toReal) :=42 ENNReal.rpow_le_rpow hint (by positivity)43 _ = M ^ (1 - 1 / p.toReal) * b ^ (1 / p.toReal) := by44 rw [ENNReal.mul_rpow_of_nonneg _ _ (by positivity), ← ENNReal.rpow_mul]45 congr 246 field_simp4748theorem eLpNorm_le_of_ae_norm_bound (f : Lp E 1 μ)49 (p : ℝ≥0∞) (hp : 1 ≤ p) (hptop : p ≠ ∞)50 (M : ℝ) (hM : ∀ᵐ x ∂μ, ‖f x‖ ≤ M) :51 eLpNorm f p μ ≤ (ENNReal.ofReal M) ^ (1 - 1 / p.toReal) *52 (ENNReal.ofReal ‖f‖) ^ (1 / p.toReal) := by53 apply eLpNorm_le_of_ae_bound f (Lp.aestronglyMeasurable f) p hp hptop54 · filter_upwards [hM] with x hx55 simpa only [ofReal_norm] using ENNReal.ofReal_le_ofReal hx56 · simp only [ofReal_norm, Lp.enorm_def, le_refl]5758private theorem interpolation_bound_ne_top (p : ℝ≥0∞) (hp : 1 ≤ p) (hptop : p ≠ ∞)59 (M b : ℝ) :60 (ENNReal.ofReal M) ^ (1 - 1 / p.toReal) *61 (ENNReal.ofReal b) ^ (1 / p.toReal) ≠ ∞ := by62 have hpR : (1 : ℝ) ≤ p.toReal := by simpa using ENNReal.toReal_mono hptop hp63 have hp0 : 0 < p.toReal := lt_of_lt_of_le zero_lt_one hpR64 apply ENNReal.mul_ne_top65 · apply ENNReal.rpow_ne_top_of_nonneg _ ENNReal.ofReal_ne_top66 exact sub_nonneg.mpr ((div_le_one hp0).mpr hpR)67 · exact ENNReal.rpow_ne_top_of_nonneg (by positivity) ENNReal.ofReal_ne_top6869/-- Every bounded L1 function belongs to every finite Lp space with p ≥ 1. -/70theorem memLp_of_ae_norm_bound (f : Lp E 1 μ)71 (p : ℝ≥0∞) (hp : 1 ≤ p) (hptop : p ≠ ∞)72 (M : ℝ) (hM : ∀ᵐ x ∂μ, ‖f x‖ ≤ M) : MemLp (fun x => f x) p μ :=73 ⟨Lp.aestronglyMeasurable f,74 (eLpNorm_le_of_ae_norm_bound f p hp hptop M hM).trans_lt75 (lt_top_iff_ne_top.mpr (interpolation_bound_ne_top p hp hptop M ‖f‖))⟩7677/-- The concrete Lp vector obtained from a bounded L1 function has the usual78interpolation norm estimate. -/79theorem norm_toLp_le_of_ae_norm_bound (f : Lp E 1 μ)80 (p : ℝ≥0∞) (hp : 1 ≤ p) (hptop : p ≠ ∞) [Fact (1 ≤ p)]81 (M : ℝ) (hMnonneg : 0 ≤ M) (hM : ∀ᵐ x ∂μ, ‖f x‖ ≤ M)82 (hf : MemLp (fun x => f x) p μ) :83 ‖hf.toLp (fun x => f x)‖ ≤ M ^ (1 - 1 / p.toReal) * ‖f‖ ^ (1 / p.toReal) := by84 rw [Lp.norm_toLp]85 have h := ENNReal.toReal_mono (interpolation_bound_ne_top p hp hptop M ‖f‖)86 (eLpNorm_le_of_ae_norm_bound f p hp hptop M hM)87 simpa only [ENNReal.toReal_mul, ← ENNReal.toReal_rpow,88 ENNReal.toReal_ofReal hMnonneg, ENNReal.toReal_ofReal (norm_nonneg f)] using h8990end PL1.LpInterpolation91