Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.distribution_add

Carleson.ToMathlib.Distribution · Carleson/ToMathlib/Distribution.lean:362 to 390

Mathematical statement

Exact Lean statement

lemma distribution_add {ε} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {f g : α → ε}
  (h : Disjoint (Function.support f) (Function.support g)) (hg : AEStronglyMeasurable g μ) :
    distribution (f + g) t μ = distribution f t μ + distribution g t μ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma distribution_add {ε} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {f g : α → ε}  (h : Disjoint (Function.support f) (Function.support g)) (hg : AEStronglyMeasurable g μ) :    distribution (f + g) t μ = distribution f t μ + distribution g t μ := by  unfold distribution  rw [← measure_union₀]  · congr 1    ext x    simp only [Pi.add_apply, mem_setOf_eq, mem_union]    by_cases hxf : x ∈ support f    · have := disjoint_left.mp h hxf      simp_all    · simp_all  · apply nullMeasurableSet_lt aemeasurable_const hg.enorm  · apply Disjoint.aedisjoint    apply disjoint_of_subset _ _ h    · intro x      simp only [mem_setOf_eq, mem_support, ne_eq]      intro h'      have := LT.lt.ne_bot h'      rw [ENNReal.bot_eq_zero] at this      contrapose! this      rw [this, enorm_zero]    · intro x      simp only [mem_setOf_eq, mem_support, ne_eq]      intro h'      have := LT.lt.ne_bot h'      rw [ENNReal.bot_eq_zero] at this      contrapose! this      rw [this, enorm_zero]