memLp_add_of_disjoint — Mathlib

English

If two measurable sets have equal indicatorConstLp values for all nonzero c, then the sets are μ-a.e. equal.

Русский

Если для всех ненулевых c значения indicatorConstLp одинаковы, множества равны μ-эквивалентно.

LaTeX

$$indicatorConstLp(p, hs, hμs, c) = indicatorConstLp(p, ht, hμt, c) for all c ≠ 0 ⇒ s =ᵐ μ t.$$

Lean4

theorem memLp_add_of_disjoint {f g : α → E} (h : Disjoint (support f) (support g)) (hf : StronglyMeasurable f)
    (hg : StronglyMeasurable g) : MemLp (f + g) p μ ↔ MemLp f p μ ∧ MemLp g p μ :=
  by
  borelize E
  refine ⟨fun hfg => ⟨?_, ?_⟩, fun h => h.1.add h.2⟩
  · rw [← Set.indicator_add_eq_left h]; exact hfg.indicator (measurableSet_support hf.measurable)
  · rw [← Set.indicator_add_eq_right h]; exact hfg.indicator (measurableSet_support hg.measurable)

Похожие утверждения