mutuallySingular_compProd_left_iff

English

Under finiteness hypotheses, μ ⊗ κ ⟂ ν ⊗ κ iff μ ⟂ ν.

Русский

При конечных предпосылках μ ⊗ κ ⟂ ν ⊗ κ тогда и только тогда μ ⟂ ν.

LaTeX

$$$[SFinite μ][SigmaFinite ν][IsSFiniteKernel κ] : (μ ⊗ₘ κ) ⟂ₘ (ν ⊗ₘ κ) \\iff μ ⟂ₘ ν$$$

Lean4

theorem mutuallySingular_compProd_left_iff [SFinite μ] [SigmaFinite ν] [IsSFiniteKernel κ] [hκ : ∀ x, NeZero (κ x)] :
    μ ⊗ₘ κ ⟂ₘ ν ⊗ₘ κ ↔ μ ⟂ₘ ν := by
  refine ⟨fun h ↦ ?_, fun h ↦ h.compProd_of_left _ _⟩
  rw [← withDensity_rnDeriv_eq_zero]
  have hh := mutuallySingular_of_mutuallySingular_compProd h ?_ ?_ (ξ := ν.withDensity (μ.rnDeriv ν))
  rotate_left
  · exact absolutelyContinuous_of_le (μ.withDensity_rnDeriv_le ν)
  · exact withDensity_absolutelyContinuous _ _
  simp_rw [MutuallySingular.self_iff, (hκ _).ne] at hh
  exact ae_eq_bot.mp (Filter.eventually_false_iff_eq_bot.mp hh)

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