integral_congr_ae₂ — Mathlib

English

If almost every point respects an almost-everywhere equality for a second family, the iterated integrals are equal.

Русский

Если почти во всех точках выполняется почти везде равенство для второй семьи функций, то образованные по очереди интегралы равны.

LaTeX

$$$\text{ae}\,\mu \Rightarrow \int a, \int b, f(a,b) \partial\nu \partial\mu = \int a, \int b, g(a,b) \partial\nu \partial\mu$$$

Lean4

theorem integral_congr_ae₂ {β : Type*} {_ : MeasurableSpace β} {ν : Measure β} {f g : α → β → G}
    (h : ∀ᵐ a ∂μ, f a =ᵐ[ν] g a) : ∫ a, ∫ b, f a b ∂ν ∂μ = ∫ a, ∫ b, g a b ∂ν ∂μ :=
  by
  apply integral_congr_ae
  filter_upwards [h] with _ ha
  apply integral_congr_ae
  filter_upwards [ha] with _ hb using hb

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