integral_congr_ae₂ — Mathlib

English

If almost everywhere with respect to κ, f and g are equal pointwise, then the iterated integrals ∫ a ∫ b f a b dκ a dμ and ∫ a ∫ b g a b dκ a dμ are equal.

Русский

Если почти везде относительно κ функции f и g равны, то вложенные интегралы по a и b равны.

LaTeX

$$$\\forall {f,g}, (∀^* a\\,∂μ, f(a,·)= g(a,·)\\,\\text{a.e. w.r.t. } κ a) \\Rightarrow \\\\ ∫ a ∫ b f(a,b) dκ a dμ = ∫ a ∫ b g(a,b) dκ a dμ$$$

Lean4

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

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