English
If i<j and independence holds, then conditional expectation with respect to natural filtration equals expectation a.e. of f_j.
Русский
Если i<j и выполняются условия независимости, то условное ожидание по естественной фильтрации совпадает почти наверняка с обычным ожиданием f_j.
LaTeX
$$$$\text{Theorem condExp_natural_ae_eq_of_lt: } \mu[f_j|\Filtration.natural f hf i] =^{ae}_{\mu} \mu[f_j].$$$$
Lean4
/-- **The second Borel-Cantelli lemma**: Given a sequence of independent sets `(sₙ)` such that
`∑ n, μ sₙ = ∞`, `limsup sₙ` has measure 1. -/
theorem measure_limsup_eq_one {s : ℕ → Set Ω} (hsm : ∀ n, MeasurableSet (s n)) (hs : iIndepSet s μ)
(hs' : (∑' n, μ (s n)) = ∞) : μ (limsup s atTop) = 1 :=
by
have : IsProbabilityMeasure μ := hs.isProbabilityMeasure
rw [measure_congr
(eventuallyEq_set.2 (ae_mem_limsup_atTop_iff μ <| measurableSet_filtrationOfSet' hsm) :
(limsup s atTop : Set Ω) =ᵐ[μ]
{ω |
Tendsto (fun n => ∑ k ∈ Finset.range n, (μ[(s (k + 1)).indicator (1 : Ω → ℝ)|filtrationOfSet hsm k]) ω)
atTop atTop})]
suffices
{ω |
Tendsto (fun n => ∑ k ∈ Finset.range n, (μ[(s (k + 1)).indicator (1 : Ω → ℝ)|filtrationOfSet hsm k]) ω) atTop
atTop} =ᵐ[μ]
Set.univ
by rw [measure_congr this, measure_univ]
have : ∀ᵐ ω ∂μ, ∀ n, (μ[(s (n + 1)).indicator (1 : Ω → ℝ)|filtrationOfSet hsm n]) ω = _ :=
ae_all_iff.2 fun n => hs.condExp_indicator_filtrationOfSet_ae_eq hsm n.lt_succ_self
filter_upwards [this] with ω hω
refine eq_true (?_ : Tendsto _ _ _)
simp_rw [hω]
have htends : Tendsto (fun n => ∑ k ∈ Finset.range n, μ (s (k + 1))) atTop (𝓝 ∞) :=
by
rw [← ENNReal.tsum_add_one_eq_top hs' (measure_ne_top _ _)]
exact ENNReal.tendsto_nat_tsum _
rw [ENNReal.tendsto_nhds_top_iff_nnreal] at htends
refine tendsto_atTop_atTop_of_monotone' ?_ ?_
· refine monotone_nat_of_le_succ fun n => ?_
rw [← sub_nonneg, Finset.sum_range_succ_sub_sum]
exact ENNReal.toReal_nonneg
· rintro ⟨B, hB⟩
refine not_eventually.2 (Frequently.of_forall fun n => ?_) (htends B.toNNReal)
rw [mem_upperBounds] at hB
specialize hB (∑ k ∈ Finset.range n, μ (s (k + 1))).toReal _
· refine ⟨n, ?_⟩
rw [ENNReal.toReal_sum (by finiteness)]
rfl
· rwa [not_lt, ENNReal.ofNNReal_toNNReal, ENNReal.le_ofReal_iff_toReal_le]
· simp
· exact le_trans (by positivity) hB
