Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.distribution_eq_zero_iff

Carleson.ToMathlib.Distribution · Carleson/ToMathlib/Distribution.lean:344 to 355

Mathematical statement

Exact Lean statement

lemma distribution_eq_zero_iff {ε} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {f : α → ε} :
    distribution f t μ = 0 ↔ eLpNormEssSup f μ ≤ t

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma distribution_eq_zero_iff {ε} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {f : α → ε} :    distribution f t μ = 0 ↔ eLpNormEssSup f μ ≤ t := by  rw [distribution, eLpNormEssSup]  rw [← compl_compl {x | t < ‖f x‖ₑ}, ← mem_ae_iff, compl_def]  simp only [mem_setOf_eq, not_lt]  constructor  · intro h    apply essSup_le_of_ae_le _    filter_upwards [h] using by simp  · rw [essSup]    intro h    filter_upwards [ENNReal.eventually_le_limsup ..] with x hx using hx.trans h