isProper_iff_inter_eq_indicator_mul

English

A proper kernel π satisfies that its value on an intersection A ∩ B equals B.indicator(1) times its value on A, i.e., a decomposition into a conditional density over B.

Русский

Правильное ядро π удовлетворяет разложению π(x,A∩B) = 1_B(x) π(x,A).

LaTeX

$$$$ π(x, A \cap B) = \mathbf{1}_B(x) \cdot π(x,A). $$$$

Lean4

theorem isProper_iff_inter_eq_indicator_mul (h𝓑𝓧 : 𝓑 ≤ 𝓧) :
    IsProper π ↔
      ∀ ⦃A : Set X⦄ (_hA : MeasurableSet[𝓧] A) ⦃B : Set X⦄ (_hB : MeasurableSet[𝓑] B) (x : X),
        π x (A ∩ B) = B.indicator 1 x * π x A :=
  by
  calc
    _ ↔
        ∀ ⦃A : Set X⦄ (_hA : MeasurableSet[𝓧] A) ⦃B : Set X⦄ (hB : MeasurableSet[𝓑] B) (x : X),
          π.restrict (h𝓑𝓧 _ hB) x A = B.indicator 1 x * π x A :=
      by simp [isProper_iff_restrict_eq_indicator_smul h𝓑𝓧, Measure.ext_iff]; aesop
    _ ↔ _ := by congr! 5 with A hA B hB x; rw [restrict_apply, Measure.restrict_apply hA]

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