isProper_iff_restrict_eq_indicator_smul

English

If the a.e. posterior condition κ ω ≪ κ ∘ₘ μ holds, then for μ-almost every x, the posterior κ†μ at x equals μ with density κ.rnDeriv(κ ∘ μ) ω x.

Русский

Если верно почти наверняка κ ω ≪ κ ∘ μ, то для μ-почти каждого x постериор κ†μ при x равен μ с плотностью κ.rnDeriv(κ ∘ μ) ω x.

LaTeX

$$$$ (κ†μ) x = μ.withDensity (λ ω ↦ κ.rnDeriv (Kernel.const _ (κ ∘ₘ μ)) ω x). $$$$

Lean4

theorem isProper_iff_restrict_eq_indicator_smul (h𝓑𝓧 : 𝓑 ≤ 𝓧) :
    IsProper π ↔
      ∀ ⦃B : Set X⦄ (hB : MeasurableSet[𝓑] B) (x : X),
        π.restrict (h𝓑𝓧 _ hB) x = B.indicator (fun _ ↦ (1 : ℝ≥0∞)) x • π x :=
  by refine ⟨fun ⟨h⟩ ↦ ?_, fun h ↦ ⟨?_⟩⟩ <;> simpa only [inf_eq_left.2 h𝓑𝓧] using h

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