Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.distribution_le_of_eLpNorm_le

Carleson.ToMathlib.Distribution · Carleson/ToMathlib/Distribution.lean:492 to 507

Mathematical statement

Exact Lean statement

lemma distribution_le_of_eLpNorm_le {ε' : Type*} [TopologicalSpace ε'] [ContinuousENorm ε']
  {δ ε p : NNReal} (δpos : 0 < δ) (p_pos : 0 < p) {f : α → ε'} (meas_f : AEStronglyMeasurable f μ)
  (hf : eLpNorm f p μ ≤ C_distribution_le_of_eLpNorm_le δ ε p) :
    distribution f δ μ ≤ ε

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma distribution_le_of_eLpNorm_le {ε' : Type*} [TopologicalSpace ε'] [ContinuousENorm ε']  {δ ε p : NNReal} (δpos : 0 < δ) (p_pos : 0 < p) {f : α → ε'} (meas_f : AEStronglyMeasurable f μ)  (hf : eLpNorm f p μ ≤ C_distribution_le_of_eLpNorm_le δ ε p) :    distribution f δ μ ≤ ε := by  apply (distribution_le_mul_pow_eLpNorm_enorm (p := p) (by simp [p_pos.ne']) (by simp) meas_f    (by simp [δpos.ne']) (by simp)).trans  calc _    _ ≤ (↑δ)⁻¹ ^ p.toReal * ENNReal.ofNNReal (C_distribution_le_of_eLpNorm_le δ ε p) ^ p.toReal := by      simp only [ENNReal.coe_toReal]      gcongr    _ ≤ ε := by      unfold C_distribution_le_of_eLpNorm_le      push_cast      rw [← ENNReal.mul_rpow_of_nonneg _ _ (by simp), ← mul_assoc,        ENNReal.inv_mul_cancel (by simp [δpos.ne']) (by simp), one_mul,        ENNReal.coe_rpow_of_nonneg _ (by simp), ENNReal.rpow_inv_rpow (by simp [p_pos.ne'])]