measure_le_tsum_of_absolutelyContinuous

English

If ρ ≪ μ, then ρ(s) ≤ ∑' p∈h.index ρ(h.covering p).

Русский

Если ρ эквивалентна μ, то ρ(s) не превышает суммирование по покрывающим.

LaTeX

$$$\\rho\\ll\\mu\\quad\\Rightarrow\\quad \\rho(s)\\le \\sum' p\\in h.index,\\rho(h.covering(p)).$$$

Lean4

theorem measure_le_tsum_of_absolutelyContinuous [SecondCountableTopology X] {ρ : Measure X} (hρ : ρ ≪ μ) :
    ρ s ≤ ∑' p : h.index, ρ (h.covering p) :=
  calc
    ρ s ≤ ρ ((s \ ⋃ p ∈ h.index, h.covering p) ∪ ⋃ p ∈ h.index, h.covering p) :=
      measure_mono (by simp only [subset_union_left, diff_union_self])
    _ ≤ ρ (s \ ⋃ p ∈ h.index, h.covering p) + ρ (⋃ p ∈ h.index, h.covering p) := (measure_union_le _ _)
    _ = ∑' p : h.index, ρ (h.covering p) := by
      rw [hρ h.measure_diff_biUnion, zero_add,
        measure_biUnion h.index_countable h.covering_disjoint fun x hx => h.measurableSet_u hx]

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