tilted_congr — Mathlib

English

If f and g are equal almost everywhere with respect to μ, tilting by f yields the same as tilting by g: f =ᵐμ g ⇒ μ.tilted f = μ.tilted g.

Русский

Если функции f и g равны почти всюду относительно μ, то тильтование по f даёт ту же меру, что и по g: f =ᵐμ g ⇒ μ.tilted f = μ.tilted g.

LaTeX

$$$$f =_{\\mu,\\mathrm{ae}} g \\implies \\mu^{\\mathrm{tilted}}(f) = \\mu^{\\mathrm{tilted}}(g).$$$$

Lean4

theorem tilted_congr {g : α → ℝ} (hfg : f =ᵐ[μ] g) : μ.tilted f = μ.tilted g :=
  by
  have h_int_eq : ∫ x, exp (f x) ∂μ = ∫ x, exp (g x) ∂μ :=
    by
    refine integral_congr_ae ?_
    filter_upwards [hfg] with x hx
    rw [hx]
  refine withDensity_congr_ae ?_
  filter_upwards [hfg] with x hx
  rw [h_int_eq, hx]

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