English
If a set of events is conditionally independent, then their indicator-valued random variables are conditionally independent.
Русский
Если множество событий условно независимо, то соответствующие индикаторные переменные независимы условно.
LaTeX
$$$\text{IndepSets}(\cdot, \{T\}) \Rightarrow\; \text{IndepFun } (1_{T})$$$
Lean4
/-- If a nonzero function belongs to `ℒ^p` and is independent of another function, then
the space is a probability space. -/
theorem isProbabilityMeasure_of_indepFun (f : Ω → E) (g : Ω → F) {p : ℝ≥0∞} (hp : p ≠ 0) (hp' : p ≠ ∞)
(hℒp : MemLp f p μ) (h'f : ¬(∀ᵐ ω ∂μ, f ω = 0)) (hindep : IndepFun f g μ) : IsProbabilityMeasure μ :=
by
obtain ⟨c, c_pos, hc⟩ : ∃ (c : ℝ≥0), 0 < c ∧ 0 < μ {ω | c ≤ ‖f ω‖₊} :=
by
contrapose! h'f
have A (c : ℝ≥0) (hc : 0 < c) : ∀ᵐ ω ∂μ, ‖f ω‖₊ < c := by simpa [ae_iff] using h'f c hc
obtain ⟨u, -, u_pos, u_lim⟩ : ∃ u, StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (𝓝 0) :=
exists_seq_strictAnti_tendsto (0 : ℝ≥0)
filter_upwards [ae_all_iff.2 (fun n ↦ A (u n) (u_pos n))] with ω hω
simpa using ge_of_tendsto' u_lim (fun i ↦ (hω i).le)
have h'c : μ {ω | c ≤ ‖f ω‖₊} < ∞ := hℒp.meas_ge_lt_top hp hp' c_pos.ne'
have :=
hindep.measure_inter_preimage_eq_mul {x | c ≤ ‖x‖₊} Set.univ
(isClosed_le continuous_const continuous_nnnorm).measurableSet MeasurableSet.univ
simp only [Set.preimage_setOf_eq, Set.preimage_univ, Set.inter_univ] at this
exact ⟨(ENNReal.mul_eq_left hc.ne' h'c.ne).1 this.symm⟩
