English
If κ a.e. is μ-a.e. perpendicular to η a with respect to μ, then μ ⊗ₘ κ ⟂ μ ⊗ₘ η for every ν (i.e., μ ⊗ κ is mutually singular with ν ⊗ η).
Русский
Если κ(a) и η(a) взаимно слабо пересекаются μ-почти для μ-обычных a, тогда μ ⊗ₘ κ и ν ⊗ₘ η взаимно-селективны для любого ν.
LaTeX
$$$\\bigl(\\forall^{\\text{ae}} a \\partial μ,\\ κ(a) \\perp_m η(a)\\bigr) \\Rightarrow μ \\otimes_m κ \\perp_m ν \\otimes_m η.$$$
Lean4
theorem compProd_of_right (μ ν : Measure α) (hκη : ∀ᵐ a ∂μ, κ a ⟂ₘ η a) : μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ η :=
by
by_cases hμ : SFinite μ
swap; · rw [compProd_of_not_sfinite _ _ hμ]; simp
by_cases hν : SFinite ν
swap; · rw [compProd_of_not_sfinite _ _ hν]; simp
let s := κ.mutuallySingularSet η
have hs : MeasurableSet s := Kernel.measurableSet_mutuallySingularSet κ η
symm
refine ⟨s, hs, ?_⟩
rw [compProd_apply hs, compProd_apply hs.compl]
have h_eq a : Prod.mk a ⁻¹' s = Kernel.mutuallySingularSetSlice κ η a := rfl
have h1 a : η a (Prod.mk a ⁻¹' s) = 0 := by rw [h_eq, Kernel.measure_mutuallySingularSetSlice]
have h2 : ∀ᵐ a ∂μ, κ a (Prod.mk a ⁻¹' s)ᶜ = 0 :=
by
filter_upwards [hκη] with a ha
rwa [h_eq, ← Kernel.withDensity_rnDeriv_eq_zero_iff_measure_eq_zero κ η a,
Kernel.withDensity_rnDeriv_eq_zero_iff_mutuallySingular]
simp [h1, lintegral_congr_ae h2]
