of_measure_le — Mathlib

English

Equivalence between FinMeasAdditive for μ and for c•μ when c ≠ 0, ∞.

Русский

Эквивалентность FinMeasAdditive для μ и для c•μ при c ≠ 0, ∞.

LaTeX

$$FinMeasAdditive (c•μ) T ↔ FinMeasAdditive μ T$$

Lean4

theorem of_measure_le {μ' : Measure α} (h : μ ≤ μ') (hT : DominatedFinMeasAdditive μ T C) (hC : 0 ≤ C) :
    DominatedFinMeasAdditive μ' T C :=
  by
  have h' : ∀ s, μ s = ∞ → μ' s = ∞ := fun s hs ↦ top_unique <| hs.symm.trans_le (h _)
  refine ⟨hT.1.of_eq_top_imp_eq_top fun s _ ↦ h' s, fun s hs hμ's ↦ ?_⟩
  have hμs : μ s < ∞ := (h s).trans_lt hμ's
  calc
    ‖T s‖ ≤ C * μ.real s := hT.2 s hs hμs
    _ ≤ C * μ'.real s := by
      simp only [measureReal_def]
      gcongr
      exacts [hμ's.ne, h s]

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