restrict_compl_sigmaFiniteSetWRT — Mathlib

English

For measurable s, the measure equality in the WRT' framework holds, linking ν s and μ s with sigma-finite restrictions.

Русский

Для измеримого s выполняется равенство по отношению ν s и μ s в рамках WRT', связывающее сигма-финитность ограничений μ|s.

LaTeX

$$$$\text{If } s\text{ is measurable},\ ν(s)\neq 0 \Rightarrow μ(s)=∞ \text{ under the} \text{WRT' framework}.$$$

Lean4

theorem restrict_compl_sigmaFiniteSetWRT [SFinite ν] (hμν : μ ≪ ν) :
    μ.restrict (μ.sigmaFiniteSetWRT ν)ᶜ = ∞ • ν.restrict (μ.sigmaFiniteSetWRT ν)ᶜ :=
  by
  ext s
  rw [Measure.restrict_apply' measurableSet_sigmaFiniteSetWRT.compl, Measure.smul_apply, smul_eq_mul,
    Measure.restrict_apply' measurableSet_sigmaFiniteSetWRT.compl]
  by_cases hνs : ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = 0
  · rw [hνs, mul_zero]
    exact hμν hνs
  · rw [ENNReal.top_mul hνs, measure_eq_top_of_subset_compl_sigmaFiniteSetWRT Set.inter_subset_right hνs]

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