Stat.Limit
Convergence concepts: convergence in probability and distribution, continuous mapping, and Slutsky-style composition rules.
Convergence 7 core · 8 supporting Defines scalar convergence in probability, L² convergence, convergence in distribution, and stochastic-order notation used by the estimation layer. ★ tightness★ const_mul_tendsto_zero
Defines scalar convergence in probability, L² convergence, convergence in distribution, and stochastic-order notation used by the estimation layer.
The core predicates are Tendsto_inProb, Tendsto_L2, Tendsto_dist,
IsBigOp, and IsLittleOp. The main theorem set includes deterministic-scalar
Slutsky for distributional convergence (Tendsto_dist.const_mul_tendsto),
tightness from convergence in distribution (Tendsto_dist.tightness),
degenerate Slutsky (IsBigOp.const_mul_tendsto_zero), and stochastic-order
arithmetic such as IsLittleOp.add_eventually_nonneg_rate,
IsLittleOp.mul_isBigOp, IsBigOp.add, and
IsBigOp.mul_isLittleOp_one_isLittleOp.
def Tendsto_inProb reviewed
⚑ flagged
Causalean.Stat
A sequence of real random variables converges in probability to a limit when, for every positive tolerance, the probability that the absolute error exceeds that tolerance tends to zero.
Definition (Lean source)
def Tendsto_inProb (Xn : ℕ → Ω → ℝ) (X : Ω → ℝ) (μ : Measure Ω) : Prop :=
TendstoInMeasure μ Xn atTop X
def Tendsto_L2 reviewed
⚑ flagged
Causalean.Stat
Tendsto_L2 Xn X μ is convergence in L²(μ) of Xn to X.
Definition (Lean source)
def Tendsto_L2 (Xn : ℕ → Ω → ℝ) (X : Ω → ℝ) (μ : Measure Ω) : Prop :=
Tendsto (fun n => eLpNorm (fun ω => Xn n ω - X ω) 2 μ) atTop (𝓝 0)
def Tendsto_dist reviewed
⚑ flagged
Causalean.Stat
Convergence in distribution means that the laws of the random variables converge weakly to a specified probability law on the real line.
Definition (Lean source)
def Tendsto_dist (Xn : ℕ → Ω → ℝ) (Q : Measure ℝ) (μ : Measure Ω)
[IsProbabilityMeasure μ] [IsProbabilityMeasure Q]
(hXn : ∀ n, AEMeasurable (Xn n) μ) : Prop :=
Tendsto (β := ProbabilityMeasure ℝ)
(fun n =>
⟨μ.map (Xn n), Measure.isProbabilityMeasure_map (hXn n)⟩) atTop
(𝓝 ⟨Q, ‹IsProbabilityMeasure Q›⟩)
def IsBigOp reviewed
⚑ flagged
Causalean.Stat
IsBigOp Xn rn μ: the sequence Xn is bounded in probability at rate rn under μ. Matches def:est-stoch-order(1):
def IsLittleOp reviewed
⚑ flagged
Causalean.Stat
IsLittleOp Xn rn μ: the sequence Xn is o_p(rn) under μ. Matches def:est-stoch-order(2):
Definition (Lean source)
def IsLittleOp (Xn : ℕ → Ω → ℝ) (rn : ℕ → ℝ) (μ : Measure Ω) : Prop :=
∀ ε : ℝ, 0 < ε →
Tendsto (fun n => μ {ω | ε * rn n < |Xn n ω|}) atTop (𝓝 0)
theorem tightness reviewed
⚑ flagged
Causalean.Stat.Tendsto_dist
Tightness from convergence in distribution. Suppose a real-valued sequence Xn is measurable at every sample size and it converges in distribution under μ to a probability measure Q on ℝ. Then Xn is bounded in probability, O_p(1). Standard fact: any single tight limit gives a tight sequence (Prokhorov).
Formal statement
hypotheses
conclusion
IsBigOp Xn (fun _ => (1 : ℝ)) μ
Proof (Lean source)
theorem Tendsto_dist.tightness
{Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
{Xn : ℕ → Ω → ℝ} {Q : Measure ℝ} [IsProbabilityMeasure Q]
(hXn : ∀ n, AEMeasurable (Xn n) μ)
(hX : Tendsto_dist Xn Q μ hXn) :
IsBigOp Xn (fun _ => (1 : ℝ)) μ := by
intro ε hε
let s : ℕ → Set ℝ := fun n => {x | (n : ℝ) ≤ |x|}
have hQtail : Tendsto (fun n => Q (s n)) atTop (𝓝 0) := by
have hs : ∀ n, NullMeasurableSet (s n) Q := by
intro n
exact (isClosed_le continuous_const continuous_abs).measurableSet.nullMeasurableSet
have hm : Antitone s := by
intro i j hij x hx
dsimp [s] at hx ⊢
exact le_trans (Nat.cast_le.mpr hij) hx
have hf : ∃ n, Q (s n) ≠ ⊤ := ⟨0, measure_ne_top Q _⟩
have hinter : (⋂ n, s n) = ∅ := by
ext x
constructor
· intro hx
obtain ⟨n, hn⟩ := exists_nat_gt |x|
exact (not_lt_of_ge (Set.mem_iInter.mp hx n)) hn
· intro hx
cases hx
have ht := tendsto_measure_iInter_atTop hs hm hf
simpa [Function.comp_def, hinter] using ht
have hεtail_pos : 0 < ofReal (ε / 2) := by
exact ENNReal.ofReal_pos.mpr (by linarith)
have hQevent := (ENNReal.tendsto_nhds_zero.mp hQtail) (ofReal (ε / 2)) hεtail_pos
obtain ⟨N, hN⟩ := hQevent.exists
refine ⟨(N : ℝ), ?_⟩
let F : Set ℝ := s N
have hFclosed : IsClosed F := by
exact isClosed_le continuous_const continuous_abs
unfold Tendsto_dist at hX
let νs : ℕ → ProbabilityMeasure ℝ := fun n =>
⟨μ.map (Xn n), Measure.isProbabilityMeasure_map (hXn n)⟩
let ν : ProbabilityMeasure ℝ := ⟨Q, inferInstance⟩
have hpm : limsup (fun n => ((νs n : ProbabilityMeasure ℝ) : Measure ℝ) F) atTop
≤ (ν : Measure ℝ) F := by
exact ProbabilityMeasure.limsup_measure_closed_le_of_tendsto (μs := νs) (μ := ν) hX hFclosed
have hhalf_le : ofReal (ε / 2) ≤ ofReal ε := by
gcongr
linarith
have hpoint : ∀ n, μ {ω | (N : ℝ) * (fun _ => (1 : ℝ)) n < |Xn n ω|}
≤ ((νs n : ProbabilityMeasure ℝ) : Measure ℝ) F := by
intro n
change μ {ω | (N : ℝ) * (fun _ => (1 : ℝ)) n < |Xn n ω|} ≤ (μ.map (Xn n)) F
rw [Measure.map_apply_of_aemeasurable (hXn n) hFclosed.measurableSet]
apply measure_mono
intro ω hω
dsimp [F, s]
have hω' : (N : ℝ) < |Xn n ω| := by
simpa using hω
exact le_of_lt hω'
calc
limsup (fun n => μ {ω | (N : ℝ) * (fun _ => (1 : ℝ)) n < |Xn n ω|}) atTop
≤ limsup (fun n => ((νs n : ProbabilityMeasure ℝ) : Measure ℝ) F) atTop := by
exact Filter.limsup_le_limsup (Eventually.of_forall hpoint)
_ ≤ (ν : Measure ℝ) F := hpm
_ = Q F := rfl
_ ≤ ofReal (ε / 2) := by
simpa [F] using hN
_ ≤ ofReal ε := hhalf_le
theorem const_mul_tendsto_zero reviewed
⚑ flagged
Causalean.Stat.IsBigOp
Degenerate Slutsky. If a real-valued sequence Xn is bounded in probability, O_p(1), under μ, and a deterministic scalar sequence a converges to 0, then the product sequence a n · Xn is o_p(1). Concretely: the product of a sequence converging to 0 with a tight sequence is o_p(1).
Formal statement
hypotheses
conclusion
IsLittleOp (fun n ω => a n * Xn n ω) (fun _ => (1 : ℝ)) μ
Proof (Lean source)
theorem IsBigOp.const_mul_tendsto_zero
{Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω}
{Xn : ℕ → Ω → ℝ} {a : ℕ → ℝ}
(hX : IsBigOp Xn (fun _ => (1 : ℝ)) μ)
(ha : Tendsto a atTop (𝓝 0)) :
IsLittleOp (fun n ω => a n * Xn n ω) (fun _ => (1 : ℝ)) μ := by
intro ε hε
rw [ENNReal.tendsto_nhds_zero]
intro δ hδ
by_cases hδtop : δ = ⊤
· filter_upwards with n
simp [hδtop]
have hδpos : 0 < δ.toReal := ENNReal.toReal_pos (ne_of_gt hδ) hδtop
let α : ℝ := δ.toReal / 2
have hαpos : 0 < α := by
dsimp [α]
linarith
rcases hX α hαpos with ⟨M0, hM0⟩
let M : ℝ := max M0 1
have hMpos : 0 < M := by
dsimp [M]
exact lt_of_lt_of_le zero_lt_one (le_max_right M0 1)
have hM0le : M0 ≤ M := by
dsimp [M]
exact le_max_left M0 1
let A : ℕ → Set Ω := fun n => {ω | M < |Xn n ω|}
let C : ℕ → Set Ω := fun n => {ω | ε < |a n * Xn n ω|}
have hlimA : limsup (fun n => μ (A n)) atTop ≤ ofReal α := by
refine le_trans (Filter.limsup_le_limsup (Eventually.of_forall ?_)) hM0
intro n
apply measure_mono
intro ω hω
dsimp [A] at hω ⊢
linarith
have hα_lt_delta : ofReal α < δ := by
rw [ENNReal.ofReal_lt_iff_lt_toReal]
· dsimp [α]
linarith
· dsimp [α]
linarith [le_of_lt hδpos]
· exact hδtop
have hAevent := Filter.eventually_lt_of_limsup_lt (lt_of_le_of_lt hlimA hα_lt_delta)
have haevent : ∀ᶠ n in atTop, |a n| < ε / M := by
have ht := (Metric.tendsto_nhds.mp ha) (ε / M) (div_pos hε hMpos)
simpa [Real.dist_eq] using ht
filter_upwards [hAevent, haevent] with n hAn han
have hsubset : C n ⊆ A n := by
intro ω hω
by_contra hnot
have hXle : |Xn n ω| ≤ M := le_of_not_gt hnot
have hprod_lt : |a n * Xn n ω| < ε := by
calc
|a n * Xn n ω| = |a n| * |Xn n ω| := abs_mul (a n) (Xn n ω)
_ ≤ |a n| * M := mul_le_mul_of_nonneg_left hXle (abs_nonneg (a n))
_ < (ε / M) * M := mul_lt_mul_of_pos_right han hMpos
_ = ε := by
field_simp [hMpos.ne']
exact (not_lt_of_ge (le_of_lt hprod_lt)) hω
have heq : {ω | ε * (fun _ => (1 : ℝ)) n < |a n * Xn n ω|} = C n := by
ext ω; simp [C]
rw [heq]
exact le_of_lt (lt_of_le_of_lt (measure_mono hsubset) hAn)
8 supporting declarations (lemmas, instances)
-
const_mul_tendstotheorem — Deterministic-scalar Slutsky for the project's measure-level Tendsto_dist wrapper.hypothesesΩ :Xn :ℕ → Ω → ℝQ :a :ℕ → ℝa₀ :ℝhXn :∀ n, AEMeasurable (Xn n) μhX :Tendsto_dist Xn Q μ hXnconclusionTendsto (β := ProbabilityMeasure ℝ) (fun n => ⟨μ.map (fun ω => a n * Xn n ω), Measure.isProbabilityMeasure_map ((measurable_const.mul measurable_id).aemeasurable.comp_aemeasurable (hXn n))⟩) atTop (𝓝 ⟨Q.map (fun x : ℝ => a₀ * x), Measure.isProbabilityMeasure_map (measurable_const.mul measurable_id).aemeasurable⟩)Proof (Lean source)
theorem Tendsto_dist.const_mul_tendsto {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] {Xn : ℕ → Ω → ℝ} {Q : Measure ℝ} [IsProbabilityMeasure Q] {a : ℕ → ℝ} {a₀ : ℝ} (hXn : ∀ n, AEMeasurable (Xn n) μ) (hX : Tendsto_dist Xn Q μ hXn) (ha : Tendsto a atTop (𝓝 a₀)) : Tendsto (β := ProbabilityMeasure ℝ) (fun n => ⟨μ.map (fun ω => a n * Xn n ω), Measure.isProbabilityMeasure_map ((measurable_const.mul measurable_id).aemeasurable.comp_aemeasurable (hXn n))⟩) atTop (𝓝 ⟨Q.map (fun x : ℝ => a₀ * x), Measure.isProbabilityMeasure_map (measurable_const.mul measurable_id).aemeasurable⟩) := by have hScaled : ∀ n, AEMeasurable (fun ω => a n * Xn n ω) μ := fun n => (measurable_const.mul measurable_id).aemeasurable.comp_aemeasurable (hXn n) letI : IsProbabilityMeasure (Q.map (fun x : ℝ => a₀ * x)) := Measure.isProbabilityMeasure_map (measurable_const.mul measurable_id).aemeasurable change Tendsto_dist (fun n ω => a n * Xn n ω) (Q.map (fun x : ℝ => a₀ * x)) μ hScaled unfold Tendsto_dist at hX ⊢ have hpm := tendsto_map_mul_of_tendsto hX ha refine hpm.congr' ?_ filter_upwards with n apply Subtype.ext change Measure.map (fun x : ℝ => a n * x) (μ.map (Xn n)) = μ.map (fun ω => a n * Xn n ω) rw [AEMeasurable.map_map_of_aemeasurable] · rfl · exact (measurable_const.mul measurable_id).aemeasurable · exact hXn n -
add_eventually_nonneg_ratetheorem — The sum of two stochastic little-o terms is stochastic little-o for an eventually nonnegative rate.hypothesesconclusionIsLittleOp (fun n ω => Xn n ω + Yn n ω) rn μProof (Lean source)
theorem IsLittleOp.add_eventually_nonneg_rate (hrn_nonneg : ∀ᶠ n : ℕ in atTop, 0 ≤ rn n) (hX : IsLittleOp Xn rn μ) (hY : IsLittleOp Yn rn μ) : IsLittleOp (fun n ω => Xn n ω + Yn n ω) rn μ := by intro ε hε rw [ENNReal.tendsto_nhds_zero] intro δ hδ by_cases hδtop : δ = ⊤ · filter_upwards with n simp [hδtop] have hδpos : 0 < δ.toReal := ENNReal.toReal_pos (ne_of_gt hδ) hδtop let α : ℝ := δ.toReal / 4 have hαpos : 0 < α := by dsimp [α] linarith let A : ℕ → Set Ω := fun n => {ω | (ε / 2) * rn n < |Xn n ω|} let B : ℕ → Set Ω := fun n => {ω | (ε / 2) * rn n < |Yn n ω|} let C : ℕ → Set Ω := fun n => {ω | ε * rn n < |Xn n ω + Yn n ω|} have hXevent_le := (ENNReal.tendsto_nhds_zero.mp (hX (ε / 2) (by linarith))) (ofReal α) (ENNReal.ofReal_pos.mpr hαpos) have hYevent_le := (ENNReal.tendsto_nhds_zero.mp (hY (ε / 2) (by linarith))) (ofReal α) (ENNReal.ofReal_pos.mpr hαpos) have htwo_alpha_lt_delta : ofReal (2 * α) < δ := by rw [ENNReal.ofReal_lt_iff_lt_toReal] · dsimp [α] linarith · dsimp [α] linarith [le_of_lt hδpos] · exact hδtop filter_upwards [hrn_nonneg, hXevent_le, hYevent_le] with n hrn hXA hYB have hsubset : C n ⊆ A n ∪ B n := by intro ω hω by_contra hnot have hnotA : ¬ (ε / 2) * rn n < |Xn n ω| := by intro hx exact hnot (inl hx) have hnotB : ¬ (ε / 2) * rn n < |Yn n ω| := by intro hy exact hnot (inr hy) have hXle : |Xn n ω| ≤ (ε / 2) * rn n := le_of_not_gt hnotA have hYle : |Yn n ω| ≤ (ε / 2) * rn n := le_of_not_gt hnotB have hsum : |Xn n ω + Yn n ω| ≤ ε * rn n := by calc |Xn n ω + Yn n ω| ≤ |Xn n ω| + |Yn n ω| := abs_add_le (Xn n ω) (Yn n ω) _ ≤ (ε / 2) * rn n + (ε / 2) * rn n := add_le_add hXle hYle _ = ε * rn n := by ring exact not_lt_of_ge hsum hω exact le_of_lt <| calc μ {ω | ε * rn n < |Xn n ω + Yn n ω|} = μ (C n) := by simp [C] _ ≤ μ (A n ∪ B n) := measure_mono hsubset _ ≤ μ (A n) + μ (B n) := MeasureTheory.measure_union_le (A n) (B n) _ ≤ ofReal α + ofReal α := add_le_add hXA hYB _ = ofReal (2 * α) := by rw [← ENNReal.ofReal_add] · congr 1 ring · linarith · linarith _ < δ := htwo_alpha_lt_delta -
of_abs_le_const_multheorem — Domination by a positive constant times a stochastic little-o term preserves the stochastic little-o rate.hypothesesconclusionIsLittleOp Xn rn μProof (Lean source)
theorem IsLittleOp.of_abs_le_const_mul {C : ℝ} (hC : 0 < C) (hY : IsLittleOp Yn rn μ) (hbound : ∀ n ω, |Xn n ω| ≤ C * |Yn n ω|) : IsLittleOp Xn rn μ := by intro ε hε rw [ENNReal.tendsto_nhds_zero] intro δ hδ have hYevent := (ENNReal.tendsto_nhds_zero.mp (hY (ε / C) (div_pos hε hC))) δ hδ filter_upwards [hYevent] with n hn refine (measure_mono ?_).trans hn intro ω hω by_contra hnot have hYle : |Yn n ω| ≤ (ε / C) * rn n := le_of_not_gt hnot have hprod : C * |Yn n ω| ≤ ε * rn n := by calc C * |Yn n ω| ≤ C * ((ε / C) * rn n) := mul_le_mul_of_nonneg_left hYle hC.le _ = ε * rn n := by field_simp [hC.ne'] exact not_lt_of_ge ((hbound n ω).trans hprod) hω -
add_onetheorem — The sum of two o_p(1) sequences is o_p(1).hypotheseshX :IsLittleOp Xn (fun _ => (1 : ℝ)) μhY :IsLittleOp Yn (fun _ => (1 : ℝ)) μconclusionIsLittleOp (fun n ω => Xn n ω + Yn n ω) (fun _ => (1 : ℝ)) μProof (Lean source)
theorem IsLittleOp.add_one (hX : IsLittleOp Xn (fun _ => (1 : ℝ)) μ) (hY : IsLittleOp Yn (fun _ => (1 : ℝ)) μ) : IsLittleOp (fun n ω => Xn n ω + Yn n ω) (fun _ => (1 : ℝ)) μ := IsLittleOp.add_eventually_nonneg_rate (Eventually.of_forall (fun _ => zero_le_one)) hX hY -
of_abs_le_const_mul_onetheorem — Domination by a positive constant times an o_p(1) sequence preserves o_p(1).hypothesesconclusionIsLittleOp Xn (fun _ => (1 : ℝ)) μProof (Lean source)
theorem IsLittleOp.of_abs_le_const_mul_one {C : ℝ} (hC : 0 < C) (hY : IsLittleOp Yn (fun _ => (1 : ℝ)) μ) (hbound : ∀ n ω, |Xn n ω| ≤ C * |Yn n ω|) : IsLittleOp Xn (fun _ => (1 : ℝ)) μ := IsLittleOp.of_abs_le_const_mul (rn := fun _ => (1 : ℝ)) hC hY hbound -
mul_isBigOptheorem — o_p(rn) · O_p(sn) = o_p(rn · sn), assuming positive rates.hypothesesconclusionIsLittleOp (fun n ω => Xn n ω * Yn n ω) (fun n => rn n * sn n) μProof (Lean source)
theorem IsLittleOp.mul_isBigOp (hrn : ∀ n, 0 < rn n) (hsn : ∀ n, 0 < sn n) (hX : IsLittleOp Xn rn μ) (hY : IsBigOp Yn sn μ) : IsLittleOp (fun n ω => Xn n ω * Yn n ω) (fun n => rn n * sn n) μ := by intro ε hε rw [ENNReal.tendsto_nhds_zero] intro δ hδ by_cases hδtop : δ = ⊤ · filter_upwards with n simp [hδtop] have hδpos : 0 < δ.toReal := ENNReal.toReal_pos (ne_of_gt hδ) hδtop let α : ℝ := δ.toReal / 8 have hαpos : 0 < α := by dsimp [α] linarith rcases hY α hαpos with ⟨M0, hM0⟩ let M : ℝ := max M0 1 have hMpos : 0 < M := by dsimp [M] exact lt_of_lt_of_le zero_lt_one (le_max_right M0 1) have hM0le : M0 ≤ M := by dsimp [M] exact le_max_left M0 1 let A : ℕ → Set Ω := fun n => {ω | (ε / M) * rn n < |Xn n ω|} let B : ℕ → Set Ω := fun n => {ω | M * sn n < |Yn n ω|} let C : ℕ → Set Ω := fun n => {ω | ε * (rn n * sn n) < |Xn n ω * Yn n ω|} have hlimB : limsup (fun n => μ (B n)) atTop ≤ ofReal α := by refine le_trans (Filter.limsup_le_limsup (Eventually.of_forall ?_)) hM0 intro n apply measure_mono intro ω hω dsimp [B] at hω ⊢ nlinarith [mul_le_mul_of_nonneg_right hM0le (le_of_lt (hsn n))] have hpoint : ∀ n, μ (C n) ≤ μ (A n) + μ (B n) := by intro n have hsubset : C n ⊆ A n ∪ B n := by intro ω hω by_contra hnot have hnotA : ¬ (ε / M) * rn n < |Xn n ω| := by intro hx exact hnot (inl hx) have hnotB : ¬ M * sn n < |Yn n ω| := by intro hy exact hnot (inr hy) have hXle : |Xn n ω| ≤ (ε / M) * rn n := le_of_not_gt hnotA have hYle : |Yn n ω| ≤ M * sn n := le_of_not_gt hnotB have hXbound_nonneg : 0 ≤ (ε / M) * rn n := le_of_lt (mul_pos (div_pos hε hMpos) (hrn n)) have hprod : |Xn n ω * Yn n ω| ≤ ε * (rn n * sn n) := by calc |Xn n ω * Yn n ω| = |Xn n ω| * |Yn n ω| := abs_mul (Xn n ω) (Yn n ω) _ ≤ ((ε / M) * rn n) * (M * sn n) := mul_le_mul hXle hYle (abs_nonneg _) hXbound_nonneg _ = ε * (rn n * sn n) := by field_simp [hMpos.ne'] exact not_lt_of_ge hprod hω calc μ (C n) ≤ μ (A n ∪ B n) := measure_mono hsubset _ ≤ μ (A n) + μ (B n) := MeasureTheory.measure_union_le (A n) (B n) have halpha_two : ofReal α < ofReal (2 * α) := by rw [ENNReal.ofReal_lt_ofReal_iff] · linarith · linarith have hBevent := Filter.eventually_lt_of_limsup_lt (lt_of_le_of_lt hlimB halpha_two) have hXt : Tendsto (fun n => μ (A n)) atTop (𝓝 0) := by simpa [A] using hX (ε / M) (div_pos hε hMpos) have hAevent_le := (ENNReal.tendsto_nhds_zero.mp hXt) (ofReal α) (by exact ENNReal.ofReal_pos.mpr hαpos) have hAevent : ∀ᶠ n in atTop, μ (A n) < ofReal (2 * α) := by filter_upwards [hAevent_le] with n hn exact lt_of_le_of_lt hn halpha_two have hfour_lt_delta : ofReal (4 * α) < δ := by rw [ENNReal.ofReal_lt_iff_lt_toReal] · dsimp [α] linarith · dsimp [α] linarith [le_of_lt hδpos] · exact hδtop filter_upwards [hAevent, hBevent] with n hAn hBn exact le_of_lt <| calc μ {ω | ε * (fun n => rn n * sn n) n < |Xn n ω * Yn n ω|} = μ (C n) := by simp [C] _ ≤ μ (A n) + μ (B n) := hpoint n _ < ofReal (2 * α) + ofReal (2 * α) := ENNReal.add_lt_add hAn hBn _ = ofReal (4 * α) := by rw [← ENNReal.ofReal_add] · congr 1; ring · linarith · linarith _ < δ := hfour_lt_delta -
addtheorem — O_p(rn) + O_p(rn) = O_p(rn).hypothesesconclusionIsBigOp (fun n ω => Xn n ω + Yn n ω) rn μProof (Lean source)
theorem IsBigOp.add (hX : IsBigOp Xn rn μ) (hY : IsBigOp Yn rn μ) : IsBigOp (fun n ω => Xn n ω + Yn n ω) rn μ := by intro ε hε rcases hX (ε / 4) (by linarith) with ⟨MX, hMX⟩ rcases hY (ε / 4) (by linarith) with ⟨MY, hMY⟩ refine ⟨MX + MY, ?_⟩ let A : ℕ → Set Ω := fun n => {ω | MX * rn n < |Xn n ω|} let B : ℕ → Set Ω := fun n => {ω | MY * rn n < |Yn n ω|} let C : ℕ → Set Ω := fun n => {ω | (MX + MY) * rn n < |Xn n ω + Yn n ω|} have hpoint : ∀ n, μ (C n) ≤ μ (A n) + μ (B n) := by intro n have hsubset : C n ⊆ A n ∪ B n := by intro ω hω by_contra hnot have hnotA : ¬ MX * rn n < |Xn n ω| := by intro hx exact hnot (inl hx) have hnotB : ¬ MY * rn n < |Yn n ω| := by intro hy exact hnot (inr hy) have hXle : |Xn n ω| ≤ MX * rn n := le_of_not_gt hnotA have hYle : |Yn n ω| ≤ MY * rn n := le_of_not_gt hnotB have hsum : |Xn n ω + Yn n ω| ≤ (MX + MY) * rn n := by calc |Xn n ω + Yn n ω| ≤ |Xn n ω| + |Yn n ω| := abs_add_le (Xn n ω) (Yn n ω) _ ≤ MX * rn n + MY * rn n := add_le_add hXle hYle _ = (MX + MY) * rn n := by ring exact not_lt_of_ge hsum hω calc μ (C n) ≤ μ (A n ∪ B n) := measure_mono hsubset _ ≤ μ (A n) + μ (B n) := MeasureTheory.measure_union_le (A n) (B n) rw [Filter.limsup_le_iff] intro y hy have hquarter_half : ofReal (ε / 4) < ofReal (ε / 2) := by rw [ENNReal.ofReal_lt_ofReal_iff] · linarith · linarith have hAevent := Filter.eventually_lt_of_limsup_lt (lt_of_le_of_lt hMX hquarter_half) have hBevent := Filter.eventually_lt_of_limsup_lt (lt_of_le_of_lt hMY hquarter_half) filter_upwards [hAevent, hBevent] with n hAn hBn calc μ (C n) ≤ μ (A n) + μ (B n) := hpoint n _ < ofReal (ε / 2) + ofReal (ε / 2) := ENNReal.add_lt_add hAn hBn _ = ofReal ε := by rw [← ENNReal.ofReal_add] · congr 1; ring · linarith · linarith _ < y := hy -
mul_isLittleOp_one_isLittleOptheorem — Slutsky-style product: Xn = O_p(1) and Yn = o_p(1) imply Xn · Yn = o_p(1).hypotheseshX :IsBigOp Xn (fun _ => (1 : ℝ)) μhY :IsLittleOp Yn (fun _ => (1 : ℝ)) μconclusionIsLittleOp (fun n ω => Xn n ω * Yn n ω) (fun _ => (1 : ℝ)) μProof (Lean source)
theorem IsBigOp.mul_isLittleOp_one_isLittleOp (hX : IsBigOp Xn (fun _ => (1 : ℝ)) μ) (hY : IsLittleOp Yn (fun _ => (1 : ℝ)) μ) : IsLittleOp (fun n ω => Xn n ω * Yn n ω) (fun _ => (1 : ℝ)) μ := by intro ε hε rw [ENNReal.tendsto_nhds_zero] intro δ hδ by_cases hδtop : δ = ⊤ · filter_upwards with n simp [hδtop] have hδpos : 0 < δ.toReal := ENNReal.toReal_pos (ne_of_gt hδ) hδtop let α : ℝ := δ.toReal / 8 have hαpos : 0 < α := by dsimp [α] linarith rcases hX α hαpos with ⟨M0, hM0⟩ let M : ℝ := max M0 1 have hMpos : 0 < M := by dsimp [M] exact lt_of_lt_of_le zero_lt_one (le_max_right M0 1) have hM0le : M0 ≤ M := by dsimp [M] exact le_max_left M0 1 let A : ℕ → Set Ω := fun n => {ω | M < |Xn n ω|} let B : ℕ → Set Ω := fun n => {ω | ε / M < |Yn n ω|} let C : ℕ → Set Ω := fun n => {ω | ε < |Xn n ω * Yn n ω|} have hlimA : limsup (fun n => μ (A n)) atTop ≤ ofReal α := by refine le_trans (Filter.limsup_le_limsup (Eventually.of_forall ?_)) hM0 intro n apply measure_mono intro ω hω dsimp [A] at hω ⊢ nlinarith have hpoint : ∀ n, μ (C n) ≤ μ (A n) + μ (B n) := by intro n have hsubset : C n ⊆ A n ∪ B n := by intro ω hω by_contra hnot have hnotA : ¬ M < |Xn n ω| := by intro hx exact hnot (inl hx) have hnotB : ¬ ε / M < |Yn n ω| := by intro hy exact hnot (inr hy) have hXle : |Xn n ω| ≤ M := le_of_not_gt hnotA have hYle : |Yn n ω| ≤ ε / M := le_of_not_gt hnotB have hprod : |Xn n ω * Yn n ω| ≤ ε := by calc |Xn n ω * Yn n ω| = |Xn n ω| * |Yn n ω| := abs_mul (Xn n ω) (Yn n ω) _ ≤ M * (ε / M) := mul_le_mul hXle hYle (abs_nonneg _) (le_of_lt hMpos) _ = ε := by field_simp [hMpos.ne'] exact not_lt_of_ge hprod hω calc μ (C n) ≤ μ (A n ∪ B n) := measure_mono hsubset _ ≤ μ (A n) + μ (B n) := MeasureTheory.measure_union_le (A n) (B n) have halpha_two : ofReal α < ofReal (2 * α) := by rw [ENNReal.ofReal_lt_ofReal_iff] · linarith · linarith have hAevent := Filter.eventually_lt_of_limsup_lt (lt_of_le_of_lt hlimA halpha_two) have hYt : Tendsto (fun n => μ (B n)) atTop (𝓝 0) := by simpa [B, mul_comm] using hY (ε / M) (div_pos hε hMpos) have hBevent_le := (ENNReal.tendsto_nhds_zero.mp hYt) (ofReal α) (by exact ENNReal.ofReal_pos.mpr hαpos) have hBevent : ∀ᶠ n in atTop, μ (B n) < ofReal (2 * α) := by filter_upwards [hBevent_le] with n hn exact lt_of_le_of_lt hn halpha_two have hfour_lt_delta : ofReal (4 * α) < δ := by rw [ENNReal.ofReal_lt_iff_lt_toReal] · dsimp [α] linarith · dsimp [α] linarith [le_of_lt hδpos] · exact hδtop filter_upwards [hAevent, hBevent] with n hAn hBn exact le_of_lt <| calc μ {ω | ε * (fun _ => (1 : ℝ)) n < |Xn n ω * Yn n ω|} = μ (C n) := by simp [C] _ ≤ μ (A n) + μ (B n) := hpoint n _ < ofReal (2 * α) + ofReal (2 * α) := ENNReal.add_lt_add hAn hBn _ = ofReal (4 * α) := by rw [← ENNReal.ofReal_add] · congr 1; ring · linarith · linarith _ < δ := hfour_lt_delta
ContinuousMapping 1 core · 7 supporting This file provides continuous-mapping and Slutsky-style primitives for convergence in probability. ★ comp_continuousAt
Continuous Mapping
This file provides continuous-mapping and Slutsky-style primitives for convergence in probability. The lemmas cover composition with a function continuous at the probability limit, reciprocals at nonzero limits, centering by a constant, and small-order bookkeeping.
The main scalar tools are Tendsto_inProb.comp_continuousAt,
Tendsto_inProb.inv, Tendsto_inProb.sub_const, Tendsto_inProb.sub,
Tendsto_inProb.isLittleOp_one, and Tendsto_inProb.isBigOp_one. The file
also provides finite-dimensional continuous mapping principles
Tendsto_inProb.pi_comp_continuousAt and
Tendsto_inProb.matrix_comp_continuousAt, which lift entrywise convergence in
probability to continuous functionals of vectors and square matrices.
theorem comp_continuousAt reviewed
⚑ flagged
Causalean.Stat.Tendsto_inProb
Continuous mapping for convergence in probability at a point. If a real-valued sequence Yn converges in probability to a point c under μ, and a function g is continuous at c, then the composed sequence g ∘ Yn converges in probability to g c. Generalizes Tendsto_inProb.inv (the case g = fun x => 1/x at a nonzero c).
Formal statement
hypotheses
conclusion
Tendsto_inProb (fun n ω => g (Yn n ω)) (fun _ => g c) μ
Proof (Lean source)
theorem Tendsto_inProb.comp_continuousAt
{Ω : Type*} [MeasurableSpace Ω] {Yn : ℕ → Ω → ℝ} {c : ℝ} {μ : Measure Ω}
{g : ℝ → ℝ} (hg : ContinuousAt g c)
(h : Tendsto_inProb Yn (fun _ => c) μ) :
Tendsto_inProb (fun n ω => g (Yn n ω)) (fun _ => g c) μ := by
unfold Tendsto_inProb at h ⊢
rw [tendstoInMeasure_iff_dist] at h ⊢
intro ε hε
have hev : ∀ᶠ y in 𝓝 c, dist (g y) (g c) < ε :=
(Metric.tendsto_nhds.mp hg) ε hε
rcases Metric.eventually_nhds_iff.mp hev with ⟨η, hηpos, hη⟩
have ht := h η hηpos
refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds ht
(fun _ => zero_le) ?_
intro n
apply measure_mono
intro ω hω
-- `ε ≤ dist (g (Yn n ω)) (g c)` forces `Yn n ω` outside the η-ball at `c`.
exact le_of_not_gt fun hd => not_le_of_gt (hη hd) hω
7 supporting declarations (lemmas, instances)
-
invtheorem — Reciprocal continuity for convergence in probability at a nonzero constant: if Yn →_p Y₀ with Y₀ ≠ 0, then 1 / Yn →_p 1 / Y₀.hypothesesconclusionTendsto_inProb (fun n ω => 1 / Yn n ω) (fun _ => 1 / Y₀) μProof (Lean source)
theorem Tendsto_inProb.inv {Ω : Type*} [MeasurableSpace Ω] {Yn : ℕ → Ω → ℝ} {Y₀ : ℝ} {μ : Measure Ω} (h : Tendsto_inProb Yn (fun _ => Y₀) μ) (hY₀ : Y₀ ≠ 0) : Tendsto_inProb (fun n ω => 1 / Yn n ω) (fun _ => 1 / Y₀) μ := by unfold Tendsto_inProb at h ⊢ rw [tendstoInMeasure_iff_dist] at h ⊢ intro ε hε have hcont : ContinuousAt (fun x : ℝ => x⁻¹) Y₀ := continuousAt_inv₀ hY₀ have hev : ∀ᶠ y in 𝓝 Y₀, dist (y⁻¹) (Y₀⁻¹) < ε := (Metric.tendsto_nhds.mp hcont) ε hε rcases Metric.eventually_nhds_iff.mp hev with ⟨η, hηpos, hη⟩ have ht := h η hηpos refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds ht (fun _ => zero_le) ?_ intro n apply measure_mono intro ω hω have hω' : ε ≤ dist (Yn n ω)⁻¹ Y₀⁻¹ := by simpa [one_div] using hω exact le_of_not_gt fun hd => not_le_of_gt (hη hd) hω' -
sub_consttheorem — Center a convergence-in-probability statement around a constant limit: if Yn →_p Y₀, then Yn - Y₀ →_p 0.hypothesesconclusionTendsto_inProb (fun n ω => Yn n ω - Y₀) (fun _ => 0) μProof (Lean source)
theorem Tendsto_inProb.sub_const {Ω : Type*} [MeasurableSpace Ω] {Yn : ℕ → Ω → ℝ} {Y₀ : ℝ} {μ : Measure Ω} (h : Tendsto_inProb Yn (fun _ => Y₀) μ) : Tendsto_inProb (fun n ω => Yn n ω - Y₀) (fun _ => 0) μ := by unfold Tendsto_inProb at h ⊢ rw [tendstoInMeasure_iff_norm] at h ⊢ intro ε hε simpa [Pi.sub_apply, sub_eq_add_neg, add_comm, add_left_comm, add_assoc] using h ε hε -
subtheorem — Difference of convergent-in-probability sequences. If Xn →_p a and Yn →_p b (both to constant limits), then Xn − Yn →_p a − b. Standard ε/2-union-bound argument; the analogue of TendstoInMeasure.sub, which Mathlib does not currently provide for the constant-limit case.hypothesesΩ :a b :ℝμ :Measure ΩhX :Tendsto_inProb Xn (fun _ => a) μhY :Tendsto_inProb Yn (fun _ => b) μconclusionTendsto_inProb (fun n ω => Xn n ω - Yn n ω) (fun _ => a - b) μProof (Lean source)
theorem Tendsto_inProb.sub {Ω : Type*} [MeasurableSpace Ω] {Xn Yn : ℕ → Ω → ℝ} {a b : ℝ} {μ : Measure Ω} (hX : Tendsto_inProb Xn (fun _ => a) μ) (hY : Tendsto_inProb Yn (fun _ => b) μ) : Tendsto_inProb (fun n ω => Xn n ω - Yn n ω) (fun _ => a - b) μ := by unfold Tendsto_inProb at hX hY ⊢ rw [tendstoInMeasure_iff_norm] at hX hY ⊢ intro ε hε have hhalf : 0 < ε / 2 := by positivity have hupper : Tendsto (fun n => μ {ω | ε / 2 ≤ ‖Xn n ω - a‖} + μ {ω | ε / 2 ≤ ‖Yn n ω - b‖}) atTop (𝓝 0) := by simpa using (hX (ε / 2) hhalf).add (hY (ε / 2) hhalf) refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hupper (fun _ => zero_le) ?_ intro n refine le_trans (measure_mono ?_) (measure_union_le _ _) intro ω hω simp only [Set.mem_setOf_eq, Real.norm_eq_abs] at hω have heq : Xn n ω - Yn n ω - (a - b) = (Xn n ω - a) - (Yn n ω - b) := by ring rw [heq] at hω rcases le_or_gt (ε / 2) |Xn n ω - a| with h1 | h1 · exact inl (by simpa [Set.mem_setOf_eq, Real.norm_eq_abs] using h1) · refine inr ?_ simp only [Set.mem_setOf_eq, Real.norm_eq_abs] by_contra h2 push_neg at h2 have htri : |(Xn n ω - a) - (Yn n ω - b)| < ε := by calc |(Xn n ω - a) - (Yn n ω - b)| ≤ |Xn n ω - a| + |Yn n ω - b| := abs_sub _ _ _ < ε / 2 + ε / 2 := add_lt_add h1 h2 _ = ε := by ring linarith -
isLittleOp_onetheorem — Convergence in probability to zero implies o_p(1): if Yn →_p 0, then Yn is IsLittleOp of the constant-one rate.Proof (Lean source)
theorem Tendsto_inProb.isLittleOp_one {Ω : Type*} [MeasurableSpace Ω] {Yn : ℕ → Ω → ℝ} {μ : Measure Ω} (h : Tendsto_inProb Yn (fun _ => 0) μ) : IsLittleOp Yn (fun _ => (1 : ℝ)) μ := by intro ε hε unfold Tendsto_inProb at h rw [tendstoInMeasure_iff_norm] at h have ht := h ε hε refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds ht (fun _ => zero_le) ?_ intro n apply measure_mono intro ω hω have hle : ε ≤ |Yn n ω| := le_of_lt (by simpa using hω) simpa [Real.norm_eq_abs] using hle -
isBigOp_onetheorem — In-probability tightness. A sequence converging in probability to a constant is bounded in probability: Xₙ →ₚ c ⟹ Xₙ = O_p(1).hypothesesconclusionIsBigOp Xn (fun _ => (1 : ℝ)) μProof (Lean source)
theorem Tendsto_inProb.isBigOp_one {Ω : Type*} [MeasurableSpace Ω] {Xn : ℕ → Ω → ℝ} {c : ℝ} {μ : Measure Ω} (h : Tendsto_inProb Xn (fun _ => c) μ) : IsBigOp Xn (fun _ => (1 : ℝ)) μ := by intro ε hε refine ⟨|c| + 1, ?_⟩ unfold Tendsto_inProb at h rw [tendstoInMeasure_iff_norm] at h have ht := h 1 one_pos have hlim : limsup (fun n => μ {ω | (1 : ℝ) ≤ ‖Xn n ω - c‖}) atTop = 0 := ht.limsup_eq calc limsup (fun n => μ {ω | (|c| + 1) * (fun _ => (1 : ℝ)) n < |Xn n ω|}) atTop ≤ limsup (fun n => μ {ω | (1 : ℝ) ≤ ‖Xn n ω - c‖}) atTop := by refine Filter.limsup_le_limsup (Filter.Eventually.of_forall ?_) intro n apply measure_mono intro ω hω simp only [Set.mem_setOf_eq, mul_one] at hω ⊢ rw [Real.norm_eq_abs] have htri := abs_sub_abs_le_abs_sub (Xn n ω) c linarith _ = 0 := hlim _ ≤ ofReal ε := zero_le -
pi_comp_continuousAttheorem — Finite-Pi continuous mapping in probability. If every coordinate of a finite-dimensional random vector converges in probability to the corresponding constant coordinate, and g is continuous at the limiting vector, then g(Yₙ) →ₚ g(c).hypothesesconclusionTendsto_inProb (fun n ω => g (Yn n ω)) (fun _ => g c) μProof (Lean source)
theorem Tendsto_inProb.pi_comp_continuousAt {Ω ι : Type*} [MeasurableSpace Ω] [Fintype ι] {μ : Measure Ω} {Yn : ℕ → Ω → (ι → ℝ)} {c : ι → ℝ} {g : (ι → ℝ) → ℝ} (hg : ContinuousAt g c) (h : ∀ i, Tendsto_inProb (fun n ω => Yn n ω i) (fun _ => c i) μ) : Tendsto_inProb (fun n ω => g (Yn n ω)) (fun _ => g c) μ := by classical unfold Tendsto_inProb rw [tendstoInMeasure_iff_dist] intro ε hε have hev := (Metric.tendsto_nhds.mp hg) ε hε rcases Metric.eventually_nhds_iff.mp hev with ⟨η, hηpos, hη⟩ let δ : ℝ := η / 2 have hδpos : 0 < δ := by dsimp [δ]; linarith have hδ_nonneg : 0 ≤ δ := le_of_lt hδpos have hδ_lt_eta : δ < η := by dsimp [δ]; linarith let Bad : ℕ → ι → Set Ω := fun n i => {ω | δ ≤ |Yn n ω i - c i|} have hentry : ∀ i, Tendsto (fun n => μ (Bad n i)) atTop (nhds 0) := by intro i have hi := h i unfold Tendsto_inProb at hi rw [tendstoInMeasure_iff_norm] at hi have ht := hi δ hδpos simpa [Bad, Real.norm_eq_abs] using ht have hupper : Tendsto (fun n => ∑ i, μ (Bad n i)) atTop (nhds 0) := by simpa using (tendsto_finset_sum (M := ENNReal) (s := (Finset.univ : Finset ι)) (f := fun i n => μ (Bad n i)) (x := atTop) (a := fun _ => (0 : ENNReal)) (fun i _ => hentry i)) have hsubset : ∀ n, {ω | ε ≤ dist (g (Yn n ω)) (g c)} ⊆ ⋃ i, Bad n i := by intro n ω hω by_contra hωU have hcoord : ∀ i, |Yn n ω i - c i| < δ := by intro i have hnot : ¬ δ ≤ |Yn n ω i - c i| := by intro hb exact hωU (Set.mem_iUnion.2 ⟨i, hb⟩) exact not_le.mp hnot have hdist_le : dist (Yn n ω) c ≤ δ := by refine (dist_pi_le_iff hδ_nonneg).2 ?_ intro i simpa [Real.dist_eq] using le_of_lt (hcoord i) have hdist : dist (Yn n ω) c < η := lt_of_le_of_lt hdist_le hδ_lt_eta exact not_le_of_gt (hη hdist) hω have hmeasure_union : ∀ n, μ (⋃ i, Bad n i) ≤ ∑ i, μ (Bad n i) := by intro n exact MeasureTheory.measure_iUnion_fintype_le μ (fun i => Bad n i) refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hupper (fun _ => zero_le) ?_ intro n calc μ {ω | ε ≤ dist (g (Yn n ω)) (g c)} ≤ μ (⋃ i, Bad n i) := measure_mono (hsubset n) _ ≤ ∑ i, μ (Bad n i) := hmeasure_union n -
matrix_comp_continuousAttheorem — Matrix continuous mapping in probability. If every entry of the random matrix Mₙ converges in probability to the corresponding entry of M₀, and g is continuous at M₀, then g(Mₙ) →ₚ g(M₀).hypotheseshg :ContinuousAt g M₀h :∀ i j, Tendsto_inProb (fun n ω => Mn n ω i j) (fun _ => M₀ i j) μconclusionTendsto_inProb (fun n ω => g (Mn n ω)) (fun _ => g M₀) μProof (Lean source)
theorem Tendsto_inProb.matrix_comp_continuousAt {Ω K : Type*} [MeasurableSpace Ω] [Fintype K] {μ : Measure Ω} {Mn : ℕ → Ω → Matrix K K ℝ} {M₀ : Matrix K K ℝ} {g : Matrix K K ℝ → ℝ} (hg : ContinuousAt g M₀) (h : ∀ i j, Tendsto_inProb (fun n ω => Mn n ω i j) (fun _ => M₀ i j) μ) : Tendsto_inProb (fun n ω => g (Mn n ω)) (fun _ => g M₀) μ := by classical let reindex : ((K × K) → ℝ) → Matrix K K ℝ := fun y => of fun i j => y (i, j) have hreindex_cont : Continuous reindex := by dsimp [reindex] exact continuous_pi fun i => continuous_pi fun j => continuous_apply (i, j) have hpoint : reindex (fun p : K × K => M₀ p.1 p.2) = M₀ := by ext i j simp [reindex] have hg' : ContinuousAt (fun y : (K × K) → ℝ => g (reindex y)) (fun p : K × K => M₀ p.1 p.2) := by have hg_at : ContinuousAt g (reindex (fun p : K × K => M₀ p.1 p.2)) := by simpa [hpoint] using hg exact hg_at.comp' hreindex_cont.continuousAt have hpi := Tendsto_inProb.pi_comp_continuousAt (Ω := Ω) (ι := K × K) (μ := μ) (Yn := fun n ω p => Mn n ω p.1 p.2) (c := fun p => M₀ p.1 p.2) (g := fun y : (K × K) → ℝ => g (reindex y)) hg' (fun p => h p.1 p.2) exact hpi
ConvergenceVec 3 core · 1 supporting This module extends the scalar convergence-in-distribution interface to metric-space-valued random variables. ★ add_isLittleOp_one★ map_continuous
Vector convergence in distribution
This module extends the scalar convergence-in-distribution interface to
metric-space-valued random variables. The definition Tendsto_dist_vec
formulates weak convergence through pushforward probability measures, while
Tendsto_dist_vec.add_isLittleOp_one, Tendsto_dist_vec.congr_ae, and
Tendsto_dist_vec.map_continuous provide the vector Slutsky, a.e.-congruence,
and continuous-mapping rules used by multivariate CLT and delta-method
arguments.
def Tendsto_dist_vec reviewed
⚑ flagged
Causalean.Stat
Tendsto_dist_vec Xn Q μ hXn is convergence in distribution of an E-valued sequence Xn : ℕ → Ω → E to a probability measure Q : Measure E, formulated as weak convergence of pushforward measures.
Definition (Lean source)
def Tendsto_dist_vec {Ω E : Type*} [MeasurableSpace Ω] [PseudoMetricSpace E]
[MeasurableSpace E] [OpensMeasurableSpace E]
(Xn : ℕ → Ω → E) (Q : Measure E) (μ : Measure Ω)
[IsProbabilityMeasure μ] [IsProbabilityMeasure Q]
(hXn : ∀ n, AEMeasurable (Xn n) μ) : Prop :=
Tendsto (β := ProbabilityMeasure E)
(fun n =>
⟨μ.map (Xn n), Measure.isProbabilityMeasure_map (hXn n)⟩) atTop
(𝓝 ⟨Q, ‹IsProbabilityMeasure Q›⟩)
theorem add_isLittleOp_one reviewed
⚑ flagged
Causalean.Stat.Tendsto_dist_vec
Vector Slutsky absorption. Suppose Xn and Yn are E-valued sequences that are each measurable at every sample size, Xn converges in distribution to a probability measure Q on E, and the norm of the perturbation ‖Yn − Xn‖ is o_p(1). Then Yn also converges in distribution to Q.
Formal statement
hypotheses
Ω E :
Xn Yn :
ℕ → Ω → E
Q :
hXn :
∀ n, AEMeasurable (Xn n) μ
hYn :
∀ n, AEMeasurable (Yn n) μ
hX :
Tendsto_dist_vec Xn Q μ hXn
hRem :
IsLittleOp (fun n ω => ‖Yn n ω - Xn n ω‖) (fun _ => (1 : ℝ)) μ
conclusion
Tendsto_dist_vec Yn Q μ hYn
Proof (Lean source)
theorem Tendsto_dist_vec.add_isLittleOp_one
{Ω E : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
[NormedAddCommGroup E] [MeasurableSpace E] [OpensMeasurableSpace E]
{Xn Yn : ℕ → Ω → E} {Q : Measure E} [IsProbabilityMeasure Q]
(hXn : ∀ n, AEMeasurable (Xn n) μ)
(hYn : ∀ n, AEMeasurable (Yn n) μ)
(hX : Tendsto_dist_vec Xn Q μ hXn)
(hRem : IsLittleOp (fun n ω => ‖Yn n ω - Xn n ω‖) (fun _ => (1 : ℝ)) μ) :
Tendsto_dist_vec Yn Q μ hYn := by
have hXY : TendstoInMeasure μ (fun n ω => Yn n ω - Xn n ω) atTop (0 : Ω → E) := by
rw [tendstoInMeasure_iff_norm]
intro ε hε
have hhalf : 0 < ε / 2 := by positivity
have hrem : Tendsto (fun n => μ {ω | ε / 2 < ‖Yn n ω - Xn n ω‖}) atTop (𝓝 0) := by
have hrem' := hRem (ε / 2) hhalf
simpa [abs_of_nonneg] using hrem'
rw [ENNReal.tendsto_nhds_zero] at hrem ⊢
intro δ hδ
filter_upwards [hrem δ hδ] with n hn
have hsubset :
{x | ε ≤ ‖Yn n x - Xn n x - (0 : Ω → E) x‖}
⊆ {ω | ε / 2 < ‖Yn n ω - Xn n ω‖} := by
intro ω hω
have hω' : ε ≤ ‖Yn n ω - Xn n ω‖ := by
simpa using hω
exact lt_of_lt_of_le (by linarith) hω'
exact le_trans (measure_mono hsubset) hn
suffices ∀ (F : E → ℝ) (hF_bounded : ∃ (C : ℝ), ∀ x y, dist (F x) (F y) ≤ C)
(hF_lip : ∃ L, LipschitzWith L F),
Tendsto (fun n ↦ ∫ y, F y ∂(μ.map (Yn n))) atTop (𝓝 (∫ y, F y ∂Q)) by
exact tendsto_iff_forall_lipschitz_integral_tendsto.mpr this
rintro F ⟨M, hF_bounded⟩ ⟨L, hF_lip⟩
have hF_cont : Continuous F := hF_lip.continuous
have hM_nonneg : 0 ≤ M := by
simpa using hF_bounded (0 : E) (0 : E)
obtain rfl | hL := eq_zero_or_pos L
· simp only [LipschitzWith.zero_iff] at hF_lip
specialize hF_lip (0 : E)
simp only [← hF_lip, integral_const, smul_eq_mul]
have h_prob n : IsProbabilityMeasure (μ.map (Yn n)) := Measure.isProbabilityMeasure_map (hYn n)
simp
simp_rw [Metric.tendsto_nhds, Real.dist_eq]
suffices ∀ ε > 0, ∀ᶠ n in atTop, |∫ y, F y ∂(μ.map (Yn n)) - ∫ y, F y ∂Q| < L * ε by
intro ε hε
convert this (ε / L) (by positivity)
field_simp
intro ε hε
have h_le n : |∫ y, F y ∂(μ.map (Yn n)) - ∫ y, F y ∂Q|
≤ L * (ε / 2) + M * μ.real {ω | ε / 2 ≤ ‖Yn n ω - Xn n ω‖}
+ |∫ y, F y ∂(μ.map (Xn n)) - ∫ y, F y ∂Q| := by
refine (abs_sub_le (∫ y, F y ∂(μ.map (Yn n))) (∫ y, F y ∂(μ.map (Xn n)))
(∫ y, F y ∂Q)).trans ?_
gcongr
have hFY_meas : AEStronglyMeasurable (fun x ↦ F (Yn n x)) μ :=
(hF_cont.measurable.comp_aemeasurable (hYn n)).aestronglyMeasurable
have hFX_meas : AEStronglyMeasurable (fun x ↦ F (Xn n x)) μ :=
(hF_cont.measurable.comp_aemeasurable (hXn n)).aestronglyMeasurable
have h_int_Y : Integrable (fun x ↦ F (Yn n x)) μ := by
refine Integrable.of_bound hFY_meas (‖F (0 : E)‖ + M) (ae_of_all _ fun a ↦ ?_)
specialize hF_bounded (Yn n a) 0
rw [← sub_le_iff_le_add']
exact (abs_sub_abs_le_abs_sub (F (Yn n a)) (F 0)).trans hF_bounded
have h_int_X : Integrable (fun x ↦ F (Xn n x)) μ := by
refine Integrable.of_bound hFX_meas (‖F (0 : E)‖ + M) (ae_of_all _ fun a ↦ ?_)
specialize hF_bounded (Xn n a) 0
rw [← sub_le_iff_le_add']
exact (abs_sub_abs_le_abs_sub (F (Xn n a)) (F 0)).trans hF_bounded
have h_int_sub : Integrable (fun a ↦ ‖F (Yn n a) - F (Xn n a)‖) μ :=
(h_int_Y.sub h_int_X).norm
have hD_aemeas : AEMeasurable (fun a ↦ ‖F (Yn n a) - F (Xn n a)‖) μ :=
h_int_sub.aemeasurable
rw [integral_map (hYn n) hF_cont.aestronglyMeasurable,
integral_map (hXn n) hF_cont.aestronglyMeasurable,
← integral_sub h_int_Y h_int_X, ← Real.norm_eq_abs]
calc ‖∫ a, F (Yn n a) - F (Xn n a) ∂μ‖
_ ≤ ∫ a, ‖F (Yn n a) - F (Xn n a)‖ ∂μ := norm_integral_le_integral_norm _
_ = ∫ a in {x | ‖F (Yn n x) - F (Xn n x)‖ < L * (ε / 2)},
‖F (Yn n a) - F (Xn n a)‖ ∂μ
+ ∫ a in {x | L * (ε / 2) ≤ ‖F (Yn n x) - F (Xn n x)‖},
‖F (Yn n a) - F (Xn n a)‖ ∂μ := by
symm
simp_rw [← not_lt]
refine integral_add_compl₀ ?_ h_int_sub
exact nullMeasurableSet_lt hD_aemeas aemeasurable_const
_ ≤ ∫ a in {x | ‖F (Yn n x) - F (Xn n x)‖ < L * (ε / 2)}, L * (ε / 2) ∂μ
+ ∫ a in {x | L * (ε / 2) ≤ ‖F (Yn n x) - F (Xn n x)‖}, M ∂μ := by
gcongr ?_ + ?_
· refine setIntegral_mono_on₀ h_int_sub.integrableOn integrableOn_const ?_ ?_
· exact nullMeasurableSet_lt hD_aemeas aemeasurable_const
· exact fun x hx ↦ hx.le
· refine setIntegral_mono h_int_sub.integrableOn integrableOn_const fun a ↦ ?_
rw [← dist_eq_norm]
convert hF_bounded _ _
_ = L * (ε / 2) * μ.real {x | ‖F (Yn n x) - F (Xn n x)‖ < L * (ε / 2)}
+ M * μ.real {ω | L * (ε / 2) ≤ ‖F (Yn n ω) - F (Xn n ω)‖} := by
simp only [integral_const, MeasurableSet.univ, measureReal_restrict_apply, Set.univ_inter,
smul_eq_mul]
ring
_ ≤ L * (ε / 2) + M * μ.real {ω | ε / 2 ≤ ‖Yn n ω - Xn n ω‖} := by
have hD_subset :
{ω | L * (ε / 2) ≤ ‖F (Yn n ω) - F (Xn n ω)‖}
⊆ {ω | ε / 2 ≤ ‖Yn n ω - Xn n ω‖} := by
intro ω hω
have hLip : ‖F (Yn n ω) - F (Xn n ω)‖ ≤ L * ‖Yn n ω - Xn n ω‖ := by
simpa [dist_eq_norm] using hF_lip.dist_le_mul (Yn n ω) (Xn n ω)
have hmul : (L : ℝ) * (ε / 2) ≤ (L : ℝ) * ‖Yn n ω - Xn n ω‖ :=
hω.trans hLip
exact le_of_mul_le_mul_left hmul (by exact_mod_cast hL)
apply add_le_add
· calc
L * (ε / 2) * μ.real {x | ‖F (Yn n x) - F (Xn n x)‖ < L * (ε / 2)}
≤ L * (ε / 2) * 1 := by
gcongr
exact measureReal_le_one
_ = L * (ε / 2) := by ring
· exact mul_le_mul_of_nonneg_left
(measureReal_mono hD_subset (measure_ne_top μ _)) hM_nonneg
have h_tendsto :
Tendsto (fun n ↦ L * (ε / 2) + M * μ.real {ω | ε / 2 ≤ ‖Yn n ω - Xn n ω‖}
+ |∫ y, F y ∂(μ.map (Xn n)) - ∫ y, F y ∂Q|) atTop (𝓝 (L * ε / 2)) := by
suffices Tendsto (fun n ↦ L * (ε / 2) + M * μ.real {ω | ε / 2 ≤ ‖Yn n ω - Xn n ω‖}
+ |∫ y, F y ∂(μ.map (Xn n)) - ∫ y, F y ∂Q|) atTop (𝓝 (L * ε / 2 + M * 0 + 0)) by
simpa
refine (Tendsto.add ?_ (Tendsto.const_mul _ ?_)).add ?_
· rw [mul_div_assoc]
exact tendsto_const_nhds
· simp only [tendstoInMeasure_iff_measureReal_norm, Pi.zero_apply, sub_zero] at hXY
exact hXY (ε / 2) (by positivity)
· have hXF : Tendsto (fun n ↦ ∫ y, F y ∂(μ.map (Xn n))) atTop (𝓝 (∫ y, F y ∂Q)) :=
tendsto_iff_forall_lipschitz_integral_tendsto.mp hX F ⟨M, hF_bounded⟩ ⟨L, hF_lip⟩
rw [tendsto_iff_dist_tendsto_zero] at hXF
simpa only [Real.dist_eq] using hXF
have h_lt : L * ε / 2 < L * ε := half_lt_self (by positivity)
filter_upwards [h_tendsto.eventually_lt_const h_lt] with n hn using (h_le n).trans_lt hn
theorem map_continuous reviewed
⚑ flagged
Causalean.Stat.Tendsto_dist_vec
Pushforward of Tendsto_dist_vec under a continuous map. Suppose Xn is an E-valued sequence, measurable at every sample size, converging in distribution to a probability measure Q on E, and g : E → F is continuous. Then the composed sequence g ∘ Xn converges in distribution to the pushforward measure Q.map g.
Formal statement
hypotheses
Ω E F :
Xn :
ℕ → Ω → E
Q :
g :
E → F
hg :
hXn :
∀ n, AEMeasurable (Xn n) μ
hX :
Tendsto_dist_vec Xn Q μ hXn
conclusion
Tendsto (β := ProbabilityMeasure F) (fun n => ⟨μ.map (fun ω => g (Xn n ω)), Measure.isProbabilityMeasure_map (hg.measurable.aemeasurable.comp_aemeasurable (hXn n))⟩) atTop (𝓝 ⟨Q.map g, Measure.isProbabilityMeasure_map hg.measurable.aemeasurable⟩)
Proof (Lean source)
theorem Tendsto_dist_vec.map_continuous
{Ω E F : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
[PseudoMetricSpace E] [MeasurableSpace E] [OpensMeasurableSpace E]
[PseudoMetricSpace F] [MeasurableSpace F] [BorelSpace F]
{Xn : ℕ → Ω → E} {Q : Measure E} [IsProbabilityMeasure Q]
{g : E → F} (hg : Continuous g)
(hXn : ∀ n, AEMeasurable (Xn n) μ)
(hX : Tendsto_dist_vec Xn Q μ hXn) :
Tendsto (β := ProbabilityMeasure F)
(fun n =>
⟨μ.map (fun ω => g (Xn n ω)),
Measure.isProbabilityMeasure_map
(hg.measurable.aemeasurable.comp_aemeasurable (hXn n))⟩)
atTop
(𝓝 ⟨Q.map g, Measure.isProbabilityMeasure_map hg.measurable.aemeasurable⟩) := by
have hgXn : ∀ n, AEMeasurable (fun ω => g (Xn n ω)) μ := fun n =>
hg.measurable.aemeasurable.comp_aemeasurable (hXn n)
letI : IsProbabilityMeasure (Q.map g) :=
Measure.isProbabilityMeasure_map hg.measurable.aemeasurable
change Tendsto_dist_vec (fun n ω => g (Xn n ω)) (Q.map g) μ hgXn
unfold Tendsto_dist_vec at hX ⊢
have hpm := MeasureTheory.ProbabilityMeasure.tendsto_map_of_tendsto_of_continuous
(fun n => ⟨μ.map (Xn n), Measure.isProbabilityMeasure_map (hXn n)⟩)
⟨Q, ‹IsProbabilityMeasure Q›⟩ hX hg
refine hpm.congr' ?_
filter_upwards with n
apply Subtype.ext
change Measure.map g (μ.map (Xn n)) = μ.map (fun ω => g (Xn n ω))
rw [AEMeasurable.map_map_of_aemeasurable hg.measurable.aemeasurable (hXn n)]
rfl
1 supporting declaration (lemmas, instances)
-
congr_aetheorem — Vector convergence in distribution is invariant under eventual a.e. equality of the random variables. Vector analogue of Tendsto_dist.congr_ae.hypothesesΩ E :Xn Yn :ℕ → Ω → EQ :hXn :∀ n, AEMeasurable (Xn n) μhYn :∀ n, AEMeasurable (Yn n) μhX :Tendsto_dist_vec Xn Q μ hXnhXY :∀ᶠ n in atTop, Xn n =ᵐ[μ] Yn nconclusionTendsto_dist_vec Yn Q μ hYnProof (Lean source)
theorem Tendsto_dist_vec.congr_ae {Ω E : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] [PseudoMetricSpace E] [MeasurableSpace E] [OpensMeasurableSpace E] {Xn Yn : ℕ → Ω → E} {Q : Measure E} [IsProbabilityMeasure Q] (hXn : ∀ n, AEMeasurable (Xn n) μ) (hYn : ∀ n, AEMeasurable (Yn n) μ) (hX : Tendsto_dist_vec Xn Q μ hXn) (hXY : ∀ᶠ n in atTop, Xn n =ᵐ[μ] Yn n) : Tendsto_dist_vec Yn Q μ hYn := by unfold Tendsto_dist_vec at hX ⊢ refine hX.congr' ?_ filter_upwards [hXY] with n hn apply Subtype.ext exact Measure.map_congr hn
SequentialCumulativeRisk 1 core · 4 supporting This file isolates the purely real-analytic core of the Ω(log T) minimax lower bound for cumulative Neyman regret of an adaptive two-arm Horvitz–Thompson estimator. ★ sequential_cumulative_risk_regret
Sequential-experiment cumulative-risk engine
This file isolates the purely real-analytic core of the Ω(log T) minimax lower
bound for cumulative Neyman regret of an adaptive two-arm Horvitz–Thompson
estimator. In words: suppose a nonnegative "per-round mean-squared-error"
sequence b₁, b₂, … (with running totals Bₙ = b₁ + ⋯ + bₙ) obeys the
predictable van Trees / Bayes–Cramér–Rao recursion
bₜ ≥ (d²/4) / (Iq + (5J/4)·t + L·√(t·B_{t-1}))
for every round t ≥ 1, where J > 0 is the per-round Fisher information scale,
d ≠ 0 the oracle-sensitivity, L ≥ 0 a fixed feedback constant, and Iq ≥ 0
the prior information. Then the cumulative total is forced to grow at least
logarithmically: there is a threshold T₀ beyond which B_T ≥ (d²/(32 J))·log T.
This is the "self-bounding + harmonic-sum" argument that converts a per-round
information bound into a cumulative one — the crux of the lower bound — with the
measure-theoretic van Trees inequality and the Neyman-gap quadratic conversion
taken as clean hypotheses so the engine is self-contained and reusable.
The main engine is cumulative_risk_engine. It is assembled into the regret
form sequential_cumulative_risk_regret, the radius-monotone lemma
lem:local-neighborhood-cumulative-risk of the Neyman-regret writeup, by
combining it with the two assumed inputs: the Neyman-gap quadratic conversion
R^B_T ≥ 2 S² B_T and sup regret ≥ R^B_T. A standalone harmonic-tail bound
harmonic_sum_ge_log_sub_log is proved on the way and is independently reusable.
theorem sequential_cumulative_risk_regret reviewed
⚑ flagged
Causalean.Stat
Radius-monotone cumulative Neyman-regret lower bound (lem:local-neighborhood-cumulative-risk). Fix a per-round Fisher information scale J > 0, an oracle-sensitivity d ≠ 0, a nonnegative feedback constant L, and a nonnegative prior information Iq. Let b be a per-round mean-squared-error sequence with running totals B defined by B n = ∑_{t≤n} b t, satisfying the predictable van Trees / Bayes–Cramér–Rao recursion b t ≥ (d²/4) / (Iq + (5J/4)·t + L·√(t·B(t-1))) for every round t ≥ 1. Suppose further the Neyman-gap quadratic conversion 2S²·B T ≤ RB T for every T (the Bayes-average cumulative regret RB dominates twice the scaled cumulative Bayes MSE) and the worst-case cumulative regret Rsup dominates the Bayes average, RB T ≤ Rsup T for every T. Then there is a threshold T₀ beyond which the worst-case cumulative regret grows at least logarithmically: Rsup T ≥ (S² d² / (16J)) · log T for all T ≥ T₀, with universal constant 1/16.
Formal statement
hypotheses
S J d L Iq :
ℝ
hJ :
0 < J
hd :
d ≠ 0
hL :
0 ≤ L
hIq :
0 ≤ Iq
b B RB Rsup :
ℕ → ℝ
hB :
∀ n, B n = ∑ t ∈ Icc 1 n, b t
hrec :
∀ t : ℕ
if
1 ≤ t
then
(d ^ 2 / 4) / (Iq + (5 * J / 4) * (t : ℝ) + L * sqrt ((t : ℝ) * B (t - 1))) ≤ b t
hconv :
∀ T : ℕ, 2 * S ^ 2 * B T ≤ RB T
hsup :
∀ T : ℕ, RB T ≤ Rsup T
conclusion
∃ T₀ : ℕ, ∀ T : ℕ, T₀ ≤ T → (S ^ 2 * d ^ 2 / (16 * J)) * log (T : ℝ) ≤ Rsup T
Proof (Lean source)
theorem sequential_cumulative_risk_regret
(S J d L Iq : ℝ) (hJ : 0 < J) (hd : d ≠ 0)
(hL : 0 ≤ L) (hIq : 0 ≤ Iq)
(b B RB Rsup : ℕ → ℝ) (hB : ∀ n, B n = ∑ t ∈ Icc 1 n, b t)
(hrec : ∀ t : ℕ, 1 ≤ t →
(d ^ 2 / 4) / (Iq + (5 * J / 4) * (t : ℝ) + L * sqrt ((t : ℝ) * B (t - 1)))
≤ b t)
(hconv : ∀ T : ℕ, 2 * S ^ 2 * B T ≤ RB T)
(hsup : ∀ T : ℕ, RB T ≤ Rsup T) :
∃ T₀ : ℕ, ∀ T : ℕ, T₀ ≤ T →
(S ^ 2 * d ^ 2 / (16 * J)) * log (T : ℝ) ≤ Rsup T := by
rcases cumulative_risk_engine J d L Iq hJ hd hL hIq b B hB hrec with ⟨T₀, hBT⟩
refine ⟨T₀, ?_⟩
intro T hT
have hbase := hBT T hT
have hscale_nonneg : 0 ≤ 2 * S ^ 2 := by positivity
have hscaled :
2 * S ^ 2 * ((d ^ 2 / (32 * J)) * log (T : ℝ)) ≤
2 * S ^ 2 * B T :=
mul_le_mul_of_nonneg_left hbase hscale_nonneg
have hchain :
2 * S ^ 2 * ((d ^ 2 / (32 * J)) * log (T : ℝ)) ≤ Rsup T :=
hscaled.trans ((hconv T).trans (hsup T))
convert hchain using 1
field_simp [ne_of_gt hJ]
ring
4 supporting declarations (lemmas, instances)
-
log_add_one_sub_log_le_invlemma — Elementary per-term bound log(x+1) - log x ≤ 1/x for x > 0, i.e. log(1 + 1/x) ≤ 1/x. This is the pointwise ingredient of the harmonic-tail lower bound.Proof (Lean source)
lemma log_add_one_sub_log_le_inv {x : ℝ} (hx : 0 < x) : log (x + 1) - log x ≤ 1 / x := by have hx_ne : x ≠ 0 := ne_of_gt hx have hx1_pos : 0 < x + 1 := by linarith calc log (x + 1) - log x = log ((x + 1) / x) := by rw [Real.log_div hx1_pos.ne' hx_ne] _ ≤ (x + 1) / x - 1 := Real.log_le_sub_one_of_pos (div_pos hx1_pos hx) _ = 1 / x := by field_simp [hx_ne] ring -
harmonic_sum_ge_log_sub_loglemma — Harmonic-tail lower bound: for natural numbers with 1 ≤ m, ∑_{t=m}^{n} 1/t ≥ log(n+1) - log m. Proof by telescoping the pointwise bound 1/t ≥ log(t+1) - log t.hypothesesm n :ℕhm :1 ≤ mProof (Lean source)
lemma harmonic_sum_ge_log_sub_log (m n : ℕ) (hm : 1 ≤ m) : log ((n : ℝ) + 1) - log (m : ℝ) ≤ ∑ t ∈ Icc m n, (1 : ℝ) / (t : ℝ) := by by_cases hmn : m ≤ n · induction n with | zero => have : m = 0 := Nat.eq_zero_of_le_zero hmn omega | succ n ih => by_cases hmn' : m ≤ n · have hstep : log (((n : ℝ) + 1) + 1) - log ((n : ℝ) + 1) ≤ (1 : ℝ) / ((n : ℝ) + 1) := by exact log_add_one_sub_log_le_inv (by positivity) have htel : log (((n + 1 : ℕ) : ℝ) + 1) - log (m : ℝ) = (log ((n : ℝ) + 1) - log (m : ℝ)) + (log (((n : ℝ) + 1) + 1) - log ((n : ℝ) + 1)) := by norm_num rw [Finset.sum_Icc_succ_top hmn] rw [htel] simpa [Nat.cast_add, cast_one, add_assoc] using add_le_add (ih hmn') hstep · have hm_eq : m = n + 1 := by omega subst hm_eq simp only [Finset.Icc_self, Finset.sum_singleton] exact log_add_one_sub_log_le_inv (by positivity : 0 < ((n + 1 : ℕ) : ℝ)) · have hlt : n < m := lt_of_not_ge hmn have hle : (n : ℝ) + 1 ≤ (m : ℝ) := by exact_mod_cast Nat.succ_le_of_lt hlt have hlog : log ((n : ℝ) + 1) ≤ log (m : ℝ) := by exact Real.log_le_log (by positivity) hle rw [Finset.Icc_eq_empty hmn, Finset.sum_empty] linarith -
log_lin_log_le_half_loglemma — Sub-logarithmic growth of log (c·log T + 1): for any c > 0 there is a threshold N beyond which log (c · log T + 1) ≤ (1/2) · log T. This is the log log T = o(log T) book-keeping that lets the harmonic tail dominate the t_* = Θ(log T) cutoff. (Route: c·log T + 1 ≤ (log T)²/16 ≤ exp((log T)/2) for large T, then take log.)hypothesesc :ℝhc :0 < cProof (Lean source)
lemma log_lin_log_le_half_log {c : ℝ} (hc : 0 < c) : ∃ N : ℕ, ∀ T : ℕ, N ≤ T → log (c * log (T : ℝ) + 1) ≤ (1 / 2) * log (T : ℝ) := by have htend : Tendsto (fun T : ℕ => log (T : ℝ)) atTop atTop := by simpa [Function.comp_def] using Real.tendsto_log_atTop.comp (tendsto_natCast_atTop_atTop (R := ℝ)) obtain ⟨N, hN⟩ := Filter.eventually_atTop.mp (htend.eventually_ge_atTop (16 * c + 16)) exact ⟨N, fun T hT => log_lin_log_le_half_log_of_log_ge hc (hN T hT)⟩ -
cumulative_risk_enginetheorem — Sequential-experiment cumulative-risk engine.hypothesesJ d L Iq :ℝhJ :0 < Jhd :d ≠ 0hL :0 ≤ LhIq :0 ≤ Iqb :ℕ → ℝB :ℕ → ℝhB :∀ n, B n = ∑ t ∈ Icc 1 n, b threc :∀ t : ℕif1 ≤ tthen(d ^ 2 / 4) / (Iq + (5 * J / 4) * (t : ℝ) + L * sqrt ((t : ℝ) * B (t - 1))) ≤ b tconclusion∃ T₀ : ℕ, ∀ T : ℕ, T₀ ≤ T → (d ^ 2 / (32 * J)) * log (T : ℝ) ≤ B TProof (Lean source)
theorem cumulative_risk_engine (J d L Iq : ℝ) (hJ : 0 < J) (hd : d ≠ 0) (hL : 0 ≤ L) (hIq : 0 ≤ Iq) (b : ℕ → ℝ) (B : ℕ → ℝ) (hB : ∀ n, B n = ∑ t ∈ Icc 1 n, b t) (hrec : ∀ t : ℕ, 1 ≤ t → (d ^ 2 / 4) / (Iq + (5 * J / 4) * (t : ℝ) + L * sqrt ((t : ℝ) * B (t - 1))) ≤ b t) : ∃ T₀ : ℕ, ∀ T : ℕ, T₀ ≤ T → (d ^ 2 / (32 * J)) * log (T : ℝ) ≤ B T := by classical have hd2 : 0 < d ^ 2 := sq_pos_of_ne_zero hd have hJ_ne : J ≠ 0 := ne_of_gt hJ have hden_pos : ∀ t : ℕ, 1 ≤ t → 0 < Iq + (5 * J / 4) * (t : ℝ) + L * sqrt ((t : ℝ) * B (t - 1)) := by intro t ht have htpos : 0 < (t : ℝ) := by exact_mod_cast ht have hmain : 0 < (5 * J / 4) * (t : ℝ) := by positivity have hsqrt_nonneg : 0 ≤ L * sqrt ((t : ℝ) * B (t - 1)) := by positivity nlinarith have hb_nonneg : ∀ t : ℕ, 1 ≤ t → 0 ≤ b t := by intro t ht have hnum_pos : 0 < d ^ 2 / 4 := by positivity have hfrac_pos : 0 < (d ^ 2 / 4) / (Iq + (5 * J / 4) * (t : ℝ) + L * sqrt ((t : ℝ) * B (t - 1))) := by positivity exact (hfrac_pos.le.trans (hrec t ht)) have hB_nonneg : ∀ n : ℕ, 0 ≤ B n := by intro n rw [hB n] exact sum_nonneg fun t ht => hb_nonneg t ((Finset.mem_Icc.mp ht).1) have hB_mono : Monotone B := by intro n n' hnn' rw [hB n, hB n'] exact Finset.sum_le_sum_of_subset_of_nonneg (by intro t ht exact Finset.mem_Icc.mpr ⟨(Finset.mem_Icc.mp ht).1, (Finset.mem_Icc.mp ht).2.trans hnn'⟩) (by intro t ht' ht exact hb_nonneg t ((Finset.mem_Icc.mp ht').1)) let C₁ : ℝ := L ^ 2 * d ^ 2 / (8 * J ^ 3) + 1 have hC₁_pos : 0 < C₁ := by have hden : 0 < 8 * J ^ 3 := by positivity have hfrac_nonneg : 0 ≤ L ^ 2 * d ^ 2 / (8 * J ^ 3) := by positivity dsimp [C₁] nlinarith obtain ⟨Nlog, hNlog⟩ := log_lin_log_le_half_log hC₁_pos have htend : Tendsto (fun T : ℕ => log (T : ℝ)) atTop atTop := by simpa [Function.comp_def] using Real.tendsto_log_atTop.comp (tendsto_natCast_atTop_atTop (R := ℝ)) obtain ⟨NIq, hNIq⟩ := Filter.eventually_atTop.mp (htend.eventually_ge_atTop (4 * Iq / (J * C₁))) refine ⟨Nlog ⊔ NIq ⊔ 3, ?_⟩ intro T hT have hTlog : Nlog ≤ T := le_trans (le_trans (Nat.le_max_left _ _) (Nat.le_max_left _ _)) hT have hTIq : NIq ≤ T := le_trans (le_trans (Nat.le_max_right _ _) (Nat.le_max_left _ _)) hT have hT3 : 3 ≤ T := le_trans (Nat.le_max_right _ _) hT let LT : ℝ := log (T : ℝ) have hTpos_nat : 0 < T := by omega have hTpos : 0 < (T : ℝ) := by exact_mod_cast hTpos_nat have hTone : 1 ≤ (T : ℝ) := by exact_mod_cast (by omega : 1 ≤ T) have hLT_nonneg : 0 ≤ LT := by simpa [LT] using Real.log_nonneg hTone have hLT_pos : 0 < LT := by have hTgt1 : (1 : ℝ) < T := by exact_mod_cast (by omega : 1 < T) simpa [LT] using Real.log_pos hTgt1 have hlog_bound : log (C₁ * LT + 1) ≤ (1 / 2) * LT := by simpa [LT] using hNlog T hTlog have hIq_log : 4 * Iq / (J * C₁) ≤ LT := by simpa [LT] using hNIq T hTIq by_contra hgoal have hBTlt : B T < (d ^ 2 / (32 * J)) * LT := by exact not_le.mp hgoal let M : ℝ := (d ^ 2 / (32 * J)) * LT let tstar : ℕ := ceil (C₁ * LT) have hcut_pos : 0 < C₁ * LT := mul_pos hC₁_pos hLT_pos have hcut_nonneg : 0 ≤ C₁ * LT := hcut_pos.le have htstar_one : 1 ≤ tstar := by simpa [tstar] using (Nat.one_le_ceil_iff.mpr hcut_pos) have htstar_lower : C₁ * LT ≤ (tstar : ℝ) := by simpa [tstar] using (Nat.le_ceil (C₁ * LT)) have harg_pos : 0 < C₁ * LT + 1 := by positivity have harg_le_T : C₁ * LT + 1 ≤ (T : ℝ) := by have harg_le_exp : C₁ * LT + 1 ≤ exp ((1 / 2) * LT) := by exact (Real.log_le_iff_le_exp harg_pos).mp hlog_bound have hexp_le_T : exp ((1 / 2) * LT) ≤ (T : ℝ) := by calc exp ((1 / 2) * LT) ≤ exp LT := Real.exp_le_exp.mpr (by nlinarith) _ = (T : ℝ) := by simpa [LT] using Real.exp_log hTpos exact harg_le_exp.trans hexp_le_T have htstar_upper : (tstar : ℝ) ≤ C₁ * LT + 1 := by simpa [tstar] using (Nat.ceil_lt_add_one hcut_nonneg).le have htstar_le_T : tstar ≤ T := by rw [Nat.ceil_le] exact (le_add_of_nonneg_right zero_le_one).trans harg_le_T have hclaim : ∀ t : ℕ, tstar ≤ t → t ≤ T → d ^ 2 / (8 * J) * ((1 : ℝ) / (t : ℝ)) ≤ b t := by intro t htt htT have ht1 : 1 ≤ t := le_trans htstar_one htt have htpos : 0 < (t : ℝ) := by exact_mod_cast ht1 have ht_nonneg : 0 ≤ (t : ℝ) := htpos.le have ht_lower : C₁ * LT ≤ (t : ℝ) := by exact htstar_lower.trans (by exact_mod_cast htt) have hBt_le : B (t - 1) ≤ B T := hB_mono (by omega) have hBt_lt : B (t - 1) < M := by exact hBt_le.trans_lt (by simpa [M] using hBTlt) have hM_nonneg : 0 ≤ M := by dsimp [M] positivity have hBtM : B (t - 1) ≤ M := hBt_lt.le have hfeedback : L * sqrt ((t : ℝ) * B (t - 1)) ≤ (J / 2) * (t : ℝ) := by by_cases hL0 : L = 0 · rw [hL0] simp only [zero_mul] exact mul_nonneg (div_nonneg hJ.le (by norm_num)) ht_nonneg · have hLpos : 0 < L := lt_of_le_of_ne hL (Ne.symm hL0) have hM_le : M ≤ (J ^ 2 / (4 * L ^ 2)) * (t : ℝ) := by have hpart : (L ^ 2 * d ^ 2 / (8 * J ^ 3)) * LT ≤ (t : ℝ) := by dsimp [C₁] at ht_lower nlinarith [ht_lower, hLT_nonneg] calc M = (J ^ 2 / (4 * L ^ 2)) * ((L ^ 2 * d ^ 2 / (8 * J ^ 3)) * LT) := by dsimp [M] field_simp [ne_of_gt hJ, ne_of_gt hLpos] ring _ ≤ (J ^ 2 / (4 * L ^ 2)) * (t : ℝ) := mul_le_mul_of_nonneg_left hpart (by positivity) have hprod_le : (t : ℝ) * B (t - 1) ≤ ((J / (2 * L)) * (t : ℝ)) ^ 2 := by calc (t : ℝ) * B (t - 1) ≤ (t : ℝ) * M := mul_le_mul_of_nonneg_left hBtM ht_nonneg _ ≤ (t : ℝ) * ((J ^ 2 / (4 * L ^ 2)) * (t : ℝ)) := mul_le_mul_of_nonneg_left hM_le ht_nonneg _ = ((J / (2 * L)) * (t : ℝ)) ^ 2 := by field_simp [ne_of_gt hLpos] ring have hy_nonneg : 0 ≤ (J / (2 * L)) * (t : ℝ) := by positivity have hsqrt_le : sqrt ((t : ℝ) * B (t - 1)) ≤ (J / (2 * L)) * (t : ℝ) := by exact (Real.sqrt_le_iff).mpr ⟨hy_nonneg, hprod_le⟩ calc L * sqrt ((t : ℝ) * B (t - 1)) ≤ L * ((J / (2 * L)) * (t : ℝ)) := mul_le_mul_of_nonneg_left hsqrt_le hL _ = (J / 2) * (t : ℝ) := by field_simp [ne_of_gt hLpos] have hIq_le : Iq ≤ (J / 4) * (t : ℝ) := by have haux : Iq ≤ J / 4 * (C₁ * LT) := by field_simp [ne_of_gt hJ, ne_of_gt hC₁_pos] at hIq_log ⊢ nlinarith have hcoef : 0 ≤ J / 4 := by positivity exact haux.trans (mul_le_mul_of_nonneg_left ht_lower hcoef) let D : ℝ := Iq + (5 * J / 4) * (t : ℝ) + L * sqrt ((t : ℝ) * B (t - 1)) have hD_pos : 0 < D := by simpa [D] using hden_pos t ht1 have hD_le : D ≤ 2 * J * (t : ℝ) := by dsimp [D] nlinarith [hIq_le, hfeedback] have hright_pos : 0 < 2 * J * (t : ℝ) := by positivity have hnum_nonneg : 0 ≤ d ^ 2 / 4 := by positivity have hfrac : d ^ 2 / (8 * J) * ((1 : ℝ) / (t : ℝ)) ≤ (d ^ 2 / 4) / D := by calc d ^ 2 / (8 * J) * ((1 : ℝ) / (t : ℝ)) = (d ^ 2 / 4) / (2 * J * (t : ℝ)) := by field_simp [hJ_ne, ne_of_gt htpos] ring _ ≤ (d ^ 2 / 4) / D := div_le_div_of_nonneg_left hnum_nonneg hD_pos hD_le exact hfrac.trans (by simpa [D] using hrec t ht1) have htail_subset : Icc tstar T ⊆ Icc 1 T := by intro t ht exact Finset.mem_Icc.mpr ⟨le_trans htstar_one (Finset.mem_Icc.mp ht).1, (Finset.mem_Icc.mp ht).2⟩ have htail_le_B : ∑ t ∈ Icc tstar T, b t ≤ B T := by rw [hB T] exact Finset.sum_le_sum_of_subset_of_nonneg htail_subset (by intro t htBig htSmall exact hb_nonneg t ((Finset.mem_Icc.mp htBig).1)) have hscaled_tail : (d ^ 2 / (8 * J)) * (∑ t ∈ Icc tstar T, (1 : ℝ) / (t : ℝ)) ≤ ∑ t ∈ Icc tstar T, b t := by rw [Finset.mul_sum] exact Finset.sum_le_sum fun t ht => hclaim t (Finset.mem_Icc.mp ht).1 (Finset.mem_Icc.mp ht).2 have hharm := harmonic_sum_ge_log_sub_log tstar T htstar_one have hcoef_nonneg : 0 ≤ d ^ 2 / (8 * J) := by positivity have hlog_tail : (d ^ 2 / (8 * J)) * (log ((T : ℝ) + 1) - log (tstar : ℝ)) ≤ (d ^ 2 / (8 * J)) * (∑ t ∈ Icc tstar T, (1 : ℝ) / (t : ℝ)) := mul_le_mul_of_nonneg_left hharm hcoef_nonneg have hLT_le_log_succ : LT ≤ log ((T : ℝ) + 1) := by exact Real.log_le_log hTpos (by nlinarith) have htstar_pos_real : 0 < (tstar : ℝ) := by exact_mod_cast htstar_one have hlog_tstar_le : log (tstar : ℝ) ≤ log (C₁ * LT + 1) := by exact Real.log_le_log htstar_pos_real htstar_upper have hlog_tstar_half : log (tstar : ℝ) ≤ (1 / 2) * LT := hlog_tstar_le.trans hlog_bound have htail_lower : (d ^ 2 / (8 * J)) * ((1 / 2) * LT) ≤ B T := by have hdiff : (1 / 2) * LT ≤ log ((T : ℝ) + 1) - log (tstar : ℝ) := by nlinarith exact (mul_le_mul_of_nonneg_left hdiff hcoef_nonneg).trans (hlog_tail.trans (hscaled_tail.trans htail_le_B)) have hstrong : (d ^ 2 / (16 * J)) * LT ≤ B T := by convert htail_lower using 1 field_simp [hJ_ne] ring have hcontr : (d ^ 2 / (32 * J)) * LT < (d ^ 2 / (16 * J)) * LT := by have hposcoef : 0 < d ^ 2 / (32 * J) := by positivity have htwice : d ^ 2 / (16 * J) = 2 * (d ^ 2 / (32 * J)) := by field_simp [hJ_ne] ring calc (d ^ 2 / (32 * J)) * LT < 2 * ((d ^ 2 / (32 * J)) * LT) := by nlinarith [mul_pos hposcoef hLT_pos] _ = (d ^ 2 / (16 * J)) * LT := by rw [htwice] ring exact (lt_irrefl _ (hstrong.trans_lt (hBTlt.trans hcontr))).elim
VanTreesInequality 1 core · 0 supporting This file states and proves the classical single-parameter van Trees inequality van_trees_inequality: a Bayesian analogue of the Cramer-Rao lower bound for the mean-squared error of estimating a smooth functional of a ra ★ van_trees_inequality
The van Trees inequality (Bayesian Cramer-Rao bound)
This file states and proves the classical single-parameter van Trees
inequality van_trees_inequality: a Bayesian analogue of the Cramer-Rao lower bound for the
mean-squared error of estimating a smooth functional of a random parameter.
Setup (an econometrician's reading). A scalar parameter h is drawn from a
prior with a continuously differentiable density q supported on [a, b] that
vanishes at both endpoints (q a = q b = 0); its prior Fisher information is
I_q = ∫ q'(h)² / q(h) dh. Given h, data Z are drawn from a law P h with
score function S h (mean zero under P h) and Fisher information
I(h) = E_h[S h ²]. For any estimator δ(Z) of a differentiable scalar target
ψ(h), the average (Bayes) mean-squared error is bounded below by
(∫ ψ'(h) q(h) dh)² / (I_q + ∫ I(h) q(h) dh).
The denominator adds the prior information I_q to the average experimental
information ∫ I(h) q(h) dh; the numerator is the squared average sensitivity of
the target. Because the prior information appears additively, the bound stays
finite even where the frequentist Cramer-Rao bound degenerates, which is why the
van Trees inequality is the standard device for proving minimax lower bounds.
The differentiation-in-quadratic-mean regularity is imposed in the standard
regularity form: the score has mean zero (hscore_mean), its second moment is
the Fisher information (hfisher), and the posterior mean of the estimator is
differentiable with derivative equal to its covariance with the score
(hDQM — the DQM/"differentiate under the integral" identity). The genuine
content proved here is the integration-by-parts assembly of the numerator, the
variance decomposition of the total score, and the Cauchy–Schwarz step.
theorem van_trees_inequality reviewed
⚑ flagged
Causalean.Stat.Limit
van Trees inequality (Bayesian Cramér–Rao bound), single parameter. Let a scalar parameter h range over an interval [a, b], drawn from a prior density q that is continuously differentiable on [a, b], nonnegative, positive on the open interior, and vanishing at both endpoints. Given h, data are drawn from a law P h whose score function S h has conditional mean zero and second moment equal to the Fisher information I h; let δ be an estimator of a target ψ that is differentiable with derivative dψ, whose posterior mean is differentiable with derivative equal to its covariance with the score. Assume also that δ, S, and their pointwise products are integrable, that the three quadratic building blocks (δ-ψ)², (δ-ψ)(S+dq/q), (S+dq/q)² are integrable under P h, that the posterior-mean derivative, dψ, dq, and their combination are interval-integrable, that ψ·dq, dq²/q, and I·q are interval-integrable, and that the three h-indexed second-moment integrands are interval-integrable — the standard integrability side conditions for the Bochner/interval-integral manipulations. Assume finally that the total information — prior information plus average experimental information — is positive. Then the Bayes mean-squared error ∫ E_h[(δ − ψ h)²] q(h) dh is at least (∫ ψ'(h) q(h) dh)² / (I_q + ∫ I(h) q(h) dh), where I_q = ∫ q'(h)²/q(h) dh.
Formal statement
hypotheses
Z :
Type*
a b :
ℝ
hab :
a ≤ b
P :
ℝ → Measure Z
∀ h, IsProbabilityMeasure (P h)
δ :
Z → ℝ
ψ dψ q dq I :
ℝ → ℝ
S :
ℝ → Z → ℝ
prior regularity: `q` is `C¹` on `[a,b]`, nonnegative, positive in the interior, vanishing at the endpoints
hq_deriv :
∀ h ∈ Icc a b, HasDerivAt q (dq h) h
hq_nonneg :
∀ h ∈ Icc a b, 0 ≤ q h
hq_pos :
∀ h ∈ Ioo a b, 0 < q h
hq_a :
q a = 0
hq_b :
q b = 0
target regularity: `ψ` differentiable with derivative `dψ`
hψ_deriv :
∀ h ∈ Icc a b, HasDerivAt ψ (dψ h) h
score / DQM regularity (the differentiation-in-quadratic-mean form)
hscore_mean :
∀ h ∈ Icc a b, ∫ z, S h z ∂(P h) = 0
hfisher :
∀ h ∈ Icc a b, ∫ z, (S h z) ^ 2 ∂(P h) = I h
hDQM :
∀ h ∈ Icc a b, HasDerivAt (fun h' => ∫ z, δ z ∂(P h')) (∫ z, δ z * S h z ∂(P h)) h
integrability side conditions for Bochner/interval integral linearity
hδ_int :
∀ h ∈ Icc a b, Integrable δ (P h)
hS_int :
∀ h ∈ Icc a b, Integrable (S h) (P h)
hδS_int :
∀ h ∈ Icc a b, Integrable (fun z => δ z * S h z) (P h)
hSS_int :
∀ h ∈ Icc a b, Integrable (fun z => S h z * S h z) (P h)
hEE_inner_int :
∀ h ∈ Icc a b, Integrable (fun z => (δ z - ψ h) * (δ z - ψ h)) (P h)
hEPsi_inner_int :
∀ h ∈ Icc a b, Integrable (fun z => (δ z - ψ h) * (S h z + dq h / q h)) (P h)
hPsiPsi_inner_int :
∀ h ∈ Icc a b, Integrable (fun z => (S h z + dq h / q h) * (S h z + dq h / q h)) (P h)
hmprime_int :
IntervalIntegrable (fun h => ∫ z, δ z * S h z ∂(P h)) volume a b
hdψ_int :
IntervalIntegrable dψ volume a b
hdq_int :
IntervalIntegrable dq volume a b
hmprod_deriv_int :
IntervalIntegrable (fun h => (∫ z, δ z * S h z ∂(P h)) * q h + (∫ z, δ z ∂(P h)) * dq h) volume a b
hψdq_int :
IntervalIntegrable (fun h => ψ h * dq h) volume a b
hdq2q_int :
IntervalIntegrable (fun h => (dq h) ^ 2 / q h) volume a b
hIq_int :
IntervalIntegrable (fun h => I h * q h) volume a b
hEE_int :
IntervalIntegrable (fun h => (∫ z, (δ z - ψ h) * (δ z - ψ h) ∂(P h)) * q h) volume a b
hEPsi_int :
IntervalIntegrable (fun h => (∫ z, (δ z - ψ h) * (S h z + dq h / q h) ∂(P h)) * q h) volume a b
hPsiPsi_int :
IntervalIntegrable (fun h => (∫ z, (S h z + dq h / q h) * (S h z + dq h / q h) ∂(P h)) * q h) volume a b
positivity of the total information (prior + average experimental)
hJ :
0 < (∫ h in a..b, (dq h) ^ 2 / q h) + (∫ h in a..b, I h * q h)
conclusion
((∫ h in a..b, dψ h * q h)) ^ 2 / ((∫ h in a..b, (dq h) ^ 2 / q h) + (∫ h in a..b, I h * q h))
≤ ∫ h in a..b, (∫ z, (δ z - ψ h) ^ 2 ∂(P h)) * q h
Proof (Lean source)
theorem van_trees_inequality
{Z : Type*} [MeasurableSpace Z]
{a b : ℝ} (hab : a ≤ b)
(P : ℝ → Measure Z) [∀ h, IsProbabilityMeasure (P h)]
(δ : Z → ℝ) (ψ dψ q dq I : ℝ → ℝ) (S : ℝ → Z → ℝ)
-- prior regularity: `q` is `C¹` on `[a,b]`, nonnegative, positive in the
-- interior, vanishing at the endpoints
(hq_deriv : ∀ h ∈ Icc a b, HasDerivAt q (dq h) h)
(hq_nonneg : ∀ h ∈ Icc a b, 0 ≤ q h)
(hq_pos : ∀ h ∈ Ioo a b, 0 < q h)
(hq_a : q a = 0) (hq_b : q b = 0)
-- target regularity: `ψ` differentiable with derivative `dψ`
(hψ_deriv : ∀ h ∈ Icc a b, HasDerivAt ψ (dψ h) h)
-- score / DQM regularity (the differentiation-in-quadratic-mean form)
(hscore_mean : ∀ h ∈ Icc a b, ∫ z, S h z ∂(P h) = 0)
(hfisher : ∀ h ∈ Icc a b, ∫ z, (S h z) ^ 2 ∂(P h) = I h)
(hDQM : ∀ h ∈ Icc a b,
HasDerivAt (fun h' => ∫ z, δ z ∂(P h')) (∫ z, δ z * S h z ∂(P h)) h)
-- integrability side conditions for Bochner/interval integral linearity
(hδ_int : ∀ h ∈ Icc a b, Integrable δ (P h))
(hS_int : ∀ h ∈ Icc a b, Integrable (S h) (P h))
(hδS_int : ∀ h ∈ Icc a b, Integrable (fun z => δ z * S h z) (P h))
(hSS_int : ∀ h ∈ Icc a b, Integrable (fun z => S h z * S h z) (P h))
(hEE_inner_int : ∀ h ∈ Icc a b,
Integrable (fun z => (δ z - ψ h) * (δ z - ψ h)) (P h))
(hEPsi_inner_int : ∀ h ∈ Icc a b,
Integrable (fun z => (δ z - ψ h) * (S h z + dq h / q h)) (P h))
(hPsiPsi_inner_int : ∀ h ∈ Icc a b,
Integrable (fun z => (S h z + dq h / q h) * (S h z + dq h / q h)) (P h))
(hmprime_int : IntervalIntegrable
(fun h => ∫ z, δ z * S h z ∂(P h)) volume a b)
(hdψ_int : IntervalIntegrable dψ volume a b)
(hdq_int : IntervalIntegrable dq volume a b)
(hmprod_deriv_int : IntervalIntegrable
(fun h => (∫ z, δ z * S h z ∂(P h)) * q h
+ (∫ z, δ z ∂(P h)) * dq h) volume a b)
(hψdq_int : IntervalIntegrable (fun h => ψ h * dq h) volume a b)
(hdq2q_int : IntervalIntegrable (fun h => (dq h) ^ 2 / q h) volume a b)
(hIq_int : IntervalIntegrable (fun h => I h * q h) volume a b)
(hEE_int : IntervalIntegrable
(fun h => (∫ z, (δ z - ψ h) * (δ z - ψ h) ∂(P h)) * q h) volume a b)
(hEPsi_int : IntervalIntegrable
(fun h => (∫ z, (δ z - ψ h) * (S h z + dq h / q h) ∂(P h)) * q h) volume a b)
(hPsiPsi_int : IntervalIntegrable
(fun h => (∫ z, (S h z + dq h / q h) * (S h z + dq h / q h) ∂(P h)) * q h)
volume a b)
-- positivity of the total information (prior + average experimental)
(hJ : 0 < (∫ h in a..b, (dq h) ^ 2 / q h) + (∫ h in a..b, I h * q h)) :
((∫ h in a..b, dψ h * q h)) ^ 2
/ ((∫ h in a..b, (dq h) ^ 2 / q h) + (∫ h in a..b, I h * q h))
≤ ∫ h in a..b, (∫ z, (δ z - ψ h) ^ 2 ∂(P h)) * q h := by
-- Abbreviations for the numerator (`A`), the total information (`J`) and the
-- Bayes risk (`R`).
set A : ℝ := ∫ h in a..b, dψ h * q h with hAdef
set J : ℝ := (∫ h in a..b, (dq h) ^ 2 / q h) + (∫ h in a..b, I h * q h) with hJdef
set R : ℝ := ∫ h in a..b, (∫ z, (δ z - ψ h) ^ 2 ∂(P h)) * q h with hRdef
-- The weighted `L²(P h ⊗ q)` bilinear form, the error `e` and total score `Ψ`.
set Bform : (ℝ → Z → ℝ) → (ℝ → Z → ℝ) → ℝ :=
fun f g => ∫ h in a..b, (∫ z, f h z * g h z ∂(P h)) * q h with hBdef
set e : ℝ → Z → ℝ := fun h z => δ z - ψ h with hedef
set Ψ : ℝ → Z → ℝ := fun h z => S h z + dq h / q h with hΨdef
-- === The five genuine analytic obligations (van Trees content) ===
-- (0) The bilinear form on the error reproduces the Bayes risk.
have hExx : Bform e e = R := by
simp [hBdef, hRdef, hedef, pow_two]
-- (1) NUMERATOR: integration by parts against the prior (`q a = q b = 0`),
-- using `hDQM` (posterior-mean derivative = covariance with the score)
-- and `hscore_mean` (mean-zero score).
have hExPsi : Bform e Ψ = A := by
let m : ℝ → ℝ := fun h => ∫ z, δ z ∂(P h)
let mp : ℝ → ℝ := fun h => ∫ z, δ z * S h z ∂(P h)
have hb_ae : ∀ᵐ h : ℝ ∂volume, h ≠ b := by
rw [MeasureTheory.ae_iff]
simp
have h_integrand :
(∫ h in a..b, (∫ z, e h z * Ψ h z ∂(P h)) * q h)
= ∫ h in a..b, (mp h * q h + m h * dq h) - ψ h * dq h := by
apply intervalIntegral.integral_congr_ae
filter_upwards [hb_ae] with h hne_b
intro hh
have hhIoc : h ∈ Ioc a b := by
simpa [uIoc, min_eq_left hab, max_eq_right hab] using hh
have hhIoo : h ∈ Ioo a b :=
⟨hhIoc.1, lt_of_le_of_ne hhIoc.2 hne_b⟩
have hhIcc : h ∈ Icc a b := ⟨le_of_lt hhIoc.1, hhIoc.2⟩
let c : ℝ := dq h / q h
have hq_ne : q h ≠ 0 := ne_of_gt (hq_pos h hhIoo)
have hinner :
(∫ z, e h z * Ψ h z ∂(P h))
= mp h + c * m h - ψ h * c := by
calc
(∫ z, e h z * Ψ h z ∂(P h))
= ∫ z, (δ z * S h z + c * δ z) - (ψ h * S h z + ψ h * c) ∂(P h) := by
apply MeasureTheory.integral_congr_ae
filter_upwards with z
simp [hedef, hΨdef, c]
ring
_ = (∫ z, δ z * S h z + c * δ z ∂(P h))
- ∫ z, ψ h * S h z + ψ h * c ∂(P h) := by
have hsplit_sub := MeasureTheory.integral_sub
((hδS_int h hhIcc).add ((hδ_int h hhIcc).const_mul c))
(((hS_int h hhIcc).const_mul (ψ h)).add (integrable_const (ψ h * c)))
simpa [Pi.add_apply] using hsplit_sub
_ = ((∫ z, δ z * S h z ∂(P h)) + ∫ z, c * δ z ∂(P h))
- ((∫ z, ψ h * S h z ∂(P h)) + ∫ z, ψ h * c ∂(P h)) := by
rw [MeasureTheory.integral_add
(hδS_int h hhIcc) ((hδ_int h hhIcc).const_mul c)]
rw [MeasureTheory.integral_add
((hS_int h hhIcc).const_mul (ψ h)) (integrable_const (ψ h * c))]
_ = mp h + c * m h - ψ h * c := by
rw [MeasureTheory.integral_const_mul]
rw [MeasureTheory.integral_const_mul]
rw [hscore_mean h hhIcc]
simp [m, mp]
calc
(∫ z, e h z * Ψ h z ∂(P h)) * q h
= (mp h + c * m h - ψ h * c) * q h := by
rw [hinner]
_ = (mp h * q h + m h * dq h) - ψ h * dq h := by
rw [show c = dq h / q h by rfl]
field_simp [hq_ne]
have hm_ftc :
(∫ h in a..b, mp h * q h + m h * dq h) = 0 := by
have hderiv_mq :
(∫ h in a..b, mp h * q h + m h * dq h)
= m b * q b - m a * q a := by
apply intervalIntegral.integral_deriv_mul_eq_sub
· intro h hh
have hhIcc : h ∈ Icc a b := by
simpa [Set.uIcc_of_le hab] using hh
exact hDQM h hhIcc
· intro h hh
have hhIcc : h ∈ Icc a b := by
simpa [Set.uIcc_of_le hab] using hh
exact hq_deriv h hhIcc
· exact hmprime_int
· exact hdq_int
rw [hderiv_mq, hq_a, hq_b]
ring
have hψdq_eq :
(∫ h in a..b, ψ h * dq h) = -A := by
have hibp :
(∫ h in a..b, ψ h * dq h)
= ψ b * q b - ψ a * q a - ∫ h in a..b, dψ h * q h := by
apply intervalIntegral.integral_mul_deriv_eq_deriv_mul
· intro h hh
have hhIcc : h ∈ Icc a b := by
simpa [Set.uIcc_of_le hab] using hh
exact hψ_deriv h hhIcc
· intro h hh
have hhIcc : h ∈ Icc a b := by
simpa [Set.uIcc_of_le hab] using hh
exact hq_deriv h hhIcc
· exact hdψ_int
· exact hdq_int
rw [hibp, hq_a, hq_b, hAdef]
ring
calc
Bform e Ψ
= ∫ h in a..b, (mp h * q h + m h * dq h) - ψ h * dq h := by
simpa [hBdef] using h_integrand
_ = (∫ h in a..b, mp h * q h + m h * dq h)
- ∫ h in a..b, ψ h * dq h := by
rw [intervalIntegral.integral_sub hmprod_deriv_int hψdq_int]
_ = A := by
rw [hm_ftc, hψdq_eq]
ring
-- (2) DENOMINATOR: variance decomposition of the total score, using
-- `hfisher` (`E_h[S²] = I h`) and `hscore_mean`.
have hPsiPsi : Bform Ψ Ψ = J := by
have h_int :
(∫ h in a..b, (∫ z, Ψ h z * Ψ h z ∂(P h)) * q h)
= ∫ h in a..b, (I h * q h + (dq h) ^ 2 / q h) := by
apply intervalIntegral.integral_congr
intro h hh
have hhi : h ∈ Icc a b := by
simpa [Set.uIcc_of_le hab] using hh
let c : ℝ := dq h / q h
have hinner :
(∫ z, Ψ h z * Ψ h z ∂(P h)) = I h + c ^ 2 := by
calc
(∫ z, Ψ h z * Ψ h z ∂(P h))
= ∫ z, ((S h z * S h z) + (2 * c) * S h z + c * c) ∂(P h) := by
apply MeasureTheory.integral_congr_ae
filter_upwards with z
simp [hΨdef, c]
ring
_ = (∫ z, S h z * S h z ∂(P h))
+ (∫ z, (2 * c) * S h z ∂(P h))
+ (∫ z, c * c ∂(P h)) := by
have hsplit_outer := MeasureTheory.integral_add
((hSS_int h hhi).add ((hS_int h hhi).const_mul (2 * c)))
(integrable_const (c * c))
have hsplit_inner := MeasureTheory.integral_add
(hSS_int h hhi) ((hS_int h hhi).const_mul (2 * c))
calc
(∫ z, S h z * S h z + (2 * c) * S h z + c * c ∂(P h))
= (∫ z, S h z * S h z + (2 * c) * S h z ∂(P h))
+ ∫ z, c * c ∂(P h) := by
simpa [Pi.add_apply, add_assoc] using hsplit_outer
_ = (∫ z, S h z * S h z ∂(P h))
+ (∫ z, (2 * c) * S h z ∂(P h))
+ ∫ z, c * c ∂(P h) := by
rw [hsplit_inner]
_ = I h + c ^ 2 := by
have hSSval : (∫ z, S h z * S h z ∂(P h)) = I h := by
simpa [sq] using hfisher h hhi
rw [MeasureTheory.integral_const_mul]
rw [hscore_mean h hhi]
rw [hSSval]
simp [sq, c]
calc
(∫ z, Ψ h z * Ψ h z ∂(P h)) * q h
= (I h + (dq h / q h) ^ 2) * q h := by
simpa [c] using congrArg (fun x => x * q h) hinner
_ = I h * q h + (dq h) ^ 2 / q h := by
by_cases hq0 : q h = 0
· simp [hq0]
· field_simp [hq0]
calc
Bform Ψ Ψ = ∫ h in a..b, (I h * q h + (dq h) ^ 2 / q h) := by
simpa [hBdef] using h_int
-- … truncated; follow the source link for the rest …
WLLN 2 core · 1 supporting This module proves weak laws of large numbers for real-valued statistics of IIDSample. ★ sampleMean_tendsto_inProb★ sampleSecondMoment_tendsto_inProb
Weak laws for sample means
This module proves weak laws of large numbers for real-valued statistics of
IIDSample. The measurability helper IIDSample.measurable_sampleMean supports
sample means of measurable functions, IIDSample.sampleMean_tendsto_inProb
converts the strong law into convergence in probability for any integrable
statistic, and IIDSample.sampleSecondMoment_tendsto_inProb records the
second-moment specialization used by variance-estimation arguments.
theorem sampleMean_tendsto_inProb reviewed
⚑ flagged
Causalean.Stat.IIDSample
Generic weak law of large numbers. For an i.i.d. sample S, suppose a real-valued statistic g is measurable and integrable under the population law P. Then the sample mean S.sampleMean g N converges in probability to the population integral ∫ x, g x ∂P as N → ∞.
Formal statement
hypotheses
conclusion
Tendsto_inProb (S.sampleMean g) (fun _ => ∫ x, g x ∂P) μ
Proof (Lean source)
theorem sampleMean_tendsto_inProb
(S : IIDSample Ω X μ P) {g : X → ℝ}
(hg_meas : Measurable g)
(hg_int : Integrable g P) :
Tendsto_inProb (S.sampleMean g) (fun _ => ∫ x, g x ∂P) μ := by
haveI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure
have hg_int_sample : Integrable (fun ω => g (S.Z 0 ω)) μ := by
have hg_int_map : Integrable g (μ.map (S.Z 0)) := by
simpa [S.law] using hg_int
exact hg_int_map.comp_measurable (S.meas 0)
-- i.i.d. family of the transformed sample points
have hindep_iid :
Pairwise (onFun (fun x1 x2 => IndepFun x1 x2 μ)
(fun i ω => g (S.Z i ω))) := by
have hi : iIndepFun (fun i => g ∘ S.Z i) μ :=
S.indep.comp (fun _ => g) (fun _ => hg_meas)
intro i j hij
exact hi.indepFun hij
have hident :
∀ i, IdentDistrib (fun ω => g (S.Z i ω)) (fun ω => g (S.Z 0 ω)) μ μ := by
intro i
exact ((S.identDist i).symm.comp hg_meas)
have hslln := ProbabilityTheory.strong_law_ae_real
(fun i ω => g (S.Z i ω)) hg_int_sample hindep_iid hident
-- transfer the limiting integral through the law of `Z 0`
have hint_eq : (∫ ω, g (S.Z 0 ω) ∂μ) = ∫ x, g x ∂P := by
rw [← integral_map (S.meas 0).aemeasurable hg_meas.aestronglyMeasurable, S.law]
-- a.s. convergence of the sample mean to `∫ x, g x ∂P`
have hae : ∀ᵐ ω ∂μ,
Tendsto (fun N : ℕ => S.sampleMean g N ω) atTop
(𝓝 (∫ x, g x ∂P)) := by
filter_upwards [hslln] with ω hω
unfold IIDSample.sampleMean
simpa [hint_eq, div_eq_mul_inv, mul_comm] using hω
-- a.e. ⟹ in-measure on the finite (probability) space `μ`
unfold Tendsto_inProb
refine tendstoInMeasure_of_tendsto_ae ?_ hae
intro N
exact (S.measurable_sampleMean hg_meas N).aestronglyMeasurable
theorem sampleSecondMoment_tendsto_inProb reviewed
⚑ flagged
Causalean.Stat.IIDSample
Second-moment consistency. For an i.i.d. sample S, suppose a known influence function ψ is measurable and has square-integrable values under the population law P. Then the empirical second moment S.sampleMean (ψ²) N converges in probability to ∫ x, (ψ x)² ∂P. Direct application of the WLLN to g := ψ².
Formal statement
hypotheses
conclusion
Tendsto_inProb (S.sampleMean (fun x => (ψ x) ^ 2)) (fun _ => ∫ x, (ψ x) ^ 2 ∂P) μ
Proof (Lean source)
theorem sampleSecondMoment_tendsto_inProb
(S : IIDSample Ω X μ P) {ψ : X → ℝ}
(hψ_meas : Measurable ψ)
(hψ_sq_int : Integrable (fun x => (ψ x) ^ 2) P) :
Tendsto_inProb (S.sampleMean (fun x => (ψ x) ^ 2))
(fun _ => ∫ x, (ψ x) ^ 2 ∂P) μ :=
S.sampleMean_tendsto_inProb (hψ_meas.pow_const 2) hψ_sq_int
1 supporting declaration (lemmas, instances)
-
measurable_sampleMeantheorem — S.sampleMean g N is measurable for measurable g: it is a finite sum of g ∘ Z i scaled by a constant.hypothesesconclusionMeasurable (S.sampleMean g N)Proof (Lean source)
theorem measurable_sampleMean (S : IIDSample Ω X μ P) {g : X → ℝ} (hg_meas : Measurable g) (N : ℕ) : Measurable (S.sampleMean g N) := by unfold IIDSample.sampleMean exact (measurable_sum _ (fun i _hi => hg_meas.comp (S.meas i))).const_mul _