congr_ae — Mathlib

English

If two measures μ and ν have the same a.e. sets, then a conservative property is equivalent under both measures.

Русский

Если множества с почти полной мерой совпадают для двух мер, консервативность сохраняется между ними.

LaTeX

$$$\mathrm{Conservative}(f,\mu) \Rightarrow \mathrm{ae}\,\mu = \mathrm{ae}\,\nu \Rightarrow \mathrm{Conservative}(f,\nu);$ также обратное направление.$$

Lean4

theorem congr_ae {ν : Measure α} (hf : Conservative f μ) (h : ae μ = ae ν) : Conservative f ν :=
  .of_absolutelyContinuous hf h.ge.absolutelyContinuous_of_ae <|
    hf.toQuasiMeasurePreserving.mono h.ge.absolutelyContinuous_of_ae h.le.absolutelyContinuous_of_ae

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