prod — Mathlib

English

Let μ, μ′ be measures on α and ν, ν′ be measures on β with μ ≪ μ′ and ν ≪ ν′ (ν′ σ-finite). Then the product measure μ × ν is absolutely continuous with respect to μ′ × ν′.

Русский

Пусть μ, μ′ — меры на α, ν, ν′ — меры на β, причем μ ≪ μ′ и ν ≪ ν′ (ν′ — σ–конечная). Тогда произведениеMeasures μ × ν относительно μ′ × ν′.

LaTeX

$$$ (\mu \ll \mu') \land (\nu \ll \nu') \Rightarrow \mu \otimes \nu \ll \mu' \otimes \nu' $$$

Lean4

theorem prod [SFinite ν'] (h1 : μ ≪ μ') (h2 : ν ≪ ν') : μ.prod ν ≪ μ'.prod ν' :=
  by
  refine AbsolutelyContinuous.mk fun s hs h2s => ?_
  apply measure_prod_null_of_ae_null hs
  rw [measure_prod_null hs] at h2s
  exact (h2s.filter_mono h1.ae_le).mono fun _ h => h2 h

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