mutuallySingular_of_mutuallySingular_compProd

English

If μ ⟂ ν and ξ ≪ μ, ξ ≪ ν, then κ x ⟂ η x for μ-a.e. x.

Русский

Если μ ⟂ ν и ξ ≪ μ, ξ ≪ ν, тогда κ(x) ⟂ η(x) для μ- почти всех x.

LaTeX

$$$(ξ: Measure α):\\; ξ ⪯ μ, ξ ⪯ ν \\Rightarrow ∀^* x, κ(x) ⟂ η(x)$$$

Lean4

theorem mutuallySingular_of_mutuallySingular_compProd {ξ : Measure α} [SFinite μ] [SFinite ν] [IsSFiniteKernel κ]
    [IsSFiniteKernel η] (h : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η) (hμ : ξ ≪ μ) (hν : ξ ≪ ν) : ∀ᵐ x ∂ξ, κ x ⟂ₘ η x :=
  by
  have hs : MeasurableSet h.nullSet := h.measurableSet_nullSet
  have hμ_zero : (μ ⊗ₘ κ) h.nullSet = 0 := h.measure_nullSet
  have hν_zero : (ν ⊗ₘ η) h.nullSetᶜ = 0 := h.measure_compl_nullSet
  rw [compProd_apply, lintegral_eq_zero_iff'] at hμ_zero hν_zero
  · filter_upwards [hμ hμ_zero, hν hν_zero] with x hxμ hxν
    exact ⟨Prod.mk x ⁻¹' h.nullSet, measurable_prodMk_left hs, ⟨hxμ, hxν⟩⟩
  · exact (Kernel.measurable_kernel_prodMk_left hs.compl).aemeasurable
  · exact (Kernel.measurable_kernel_prodMk_left hs).aemeasurable
  · exact hs.compl
  · exact hs

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