Stat.Limit
Convergence concepts: convergence in probability and distribution, continuous mapping, and Slutsky-style composition rules.
Modes 5 core · 21 supporting This module gives one vocabulary for stochastic convergence that covers scalar and vector statistics, triangular arrays, and finite-design rows. ★ tendstoInProbability_const_space★ map_tendstoInProbability
Modes of stochastic convergence
This module gives one vocabulary for stochastic convergence that covers scalar and vector
statistics, triangular arrays, and finite-design rows. Unlike Mathlib's fixed-space
MeasureTheory.TendstoInMeasure, TendstoInProbability permits both the probability space and
the limiting random variable to vary with the index. TendstoInLaw exposes a probability law
itself as the distributional target.
Using Mathlib's results
Mathlib's Mathlib.MeasureTheory.Function.ConvergenceInDistribution already supplies
MeasureTheory.TendstoInDistribution.continuous_comp (continuous mapping),
MeasureTheory.TendstoInDistribution.prodMk_of_tendstoInMeasure_const and its additive and
multiplicative Slutsky corollaries, MeasureTheory.tendstoInDistribution_of_tendstoInMeasure_sub
(converging together), and MeasureTheory.TendstoInMeasure.tendstoInDistribution. The fixed-space
almost-sure-to-probability results remain in
Mathlib.MeasureTheory.Function.ConvergenceInMeasure. They are intentionally not restated here.
def TendstoInProbability reviewed
⚑ flagged
Causalean.Stat.Modes
Given a row measure, row random variables, an index filter, and row limiting random variables, convergence in probability means that every positive extended-distance tail has row measure tending to zero along the filter.
Definition (Lean source)
theorem tendstoInProbability_const_space reviewed
⚑ flagged
Causalean.Stat.Modes
For a fixed measure, an indexed family of random variables, a filter, and a fixed limiting random variable, the hub's convergence in probability is exactly Mathlib's convergence in measure.
Formal statement
hypotheses
conclusion
TendstoInProbability (fun _ => μ) X l (fun _ => g) ↔ TendstoInMeasure μ X l g
Proof (Lean source)
theorem tendstoInProbability_const_space {ι Ω E : Type*} [MeasurableSpace Ω] [EDist E]
(μ : Measure Ω) (X : ι → Ω → E) (l : Filter ι) (g : Ω → E) :
TendstoInProbability (fun _ => μ) X l (fun _ => g) ↔ TendstoInMeasure μ X l g :=
Iff.rfl
def TendstoInLaw reviewed
⚑ flagged
Causalean.Stat.Modes
Given row probability measures, row random variables, an index filter, and a target probability law, convergence in law means weak convergence of the row pushforward laws to that supplied law.
Definition (Lean source)
parameters
ι :
Type*
ι → Type*
∀ i, MeasurableSpace (Ω i)
E :
μ :
(i : ι) → Measure (Ω i)
∀ i, IsProbabilityMeasure (μ i)
X :
(i : ι) → Ω i → E
l :
Filter ι
Q :
def
TendstoInLaw μ X l Q :
Prop
given by
TendstoInDistribution X l (id : E → E) μ Q
theorem map_tendstoInProbability reviewed
⚑ flagged
Causalean.Stat.Modes
Given first and second row measures, row coupling measures, proof that each row is a coupling, the two row observables, their constant limits, an index filter, a map continuous at the limiting pair, and the two marginal convergence-in-probability statements, the map applied to the paired observable converges in probability, along the filter and under the row couplings, to the map's value at the limiting pair.
Formal statement
hypotheses
ι :
Type*
ι → Type u
ι → Type v
∀ i, MeasurableSpace (X i)
∀ i, MeasurableSpace (Y i)
E F G :
μ :
(i : ι) → Measure (X i)
ρ :
(i : ι) → Measure (Y i)
ν :
(i : ι) → Measure (X i × Y i)
hν :
∀ i, IsCoupling (ν i) (μ i) (ρ i)
U :
(i : ι) → X i → E
V :
(i : ι) → Y i → F
a :
E
b :
F
l :
Filter ι
f :
E × F → G
hf :
ContinuousAt f (a, b)
hU :
TendstoInProbability μ U l (fun _ _ => a)
hV :
TendstoInProbability ρ V l (fun _ _ => b)
conclusion
TendstoInProbability ν (fun i p => f (U i p.1, V i p.2)) l (fun _ _ => f (a, b))
Proof (Lean source)
theorem map_tendstoInProbability
{ι : Type*} {X : ι → Type u} {Y : ι → Type v}
[∀ i, MeasurableSpace (X i)] [∀ i, MeasurableSpace (Y i)]
{E F G : Type*} [PseudoMetricSpace E] [PseudoMetricSpace F]
[PseudoMetricSpace G]
(μ : (i : ι) → Measure (X i)) (ρ : (i : ι) → Measure (Y i))
(ν : (i : ι) → Measure (X i × Y i))
(hν : ∀ i, IsCoupling (ν i) (μ i) (ρ i))
(U : (i : ι) → X i → E) (V : (i : ι) → Y i → F)
(a : E) (b : F) (l : Filter ι) (f : E × F → G)
(hf : ContinuousAt f (a, b))
(hU : TendstoInProbability μ U l (fun _ _ => a))
(hV : TendstoInProbability ρ V l (fun _ _ => b)) :
TendstoInProbability ν
(fun i p => f (U i p.1, V i p.2)) l (fun _ _ => f (a, b)) := by
have hpair := pair_tendstoInProbability μ ρ ν hν U V a b l hU hV
intro ε hε
obtain ⟨δ, hδ, hcont⟩ := (EMetric.continuousAt_iff.mp hf) ε hε
have hδtail := hpair δ hδ
exact tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hδtail
(fun _ => zero_le) (fun i => by
apply measure_mono
intro p hp
exact le_of_not_gt (fun hlt => not_lt_of_ge hp (hcont hlt)))
def sqrtRatioFallback reviewed
⚑ flagged
Causalean.Stat.Modes
Given a numerator--denominator pair, the total square-root-ratio statistic with a zero fallback is the ordinary square-root ratio for a positive denominator and zero otherwise.
Definition (Lean source)
21 supporting declarations (lemmas, instances)
-
tendstoInProbability_iff_normtheorem — For row measures, seminormed-group-valued row variables, a filter, and row limits, convergence in probability is equivalent to every positive norm-tail probability tending to zero.hypothesesι :Type*ι → Type*∀ i, MeasurableSpace (Ω i)E :Type*μ :(i : ι) → Measure (Ω i)X :(i : ι) → Ω i → El :Filter ιg :(i : ι) → Ω i → EconclusionTendstoInProbability μ X l g↔ ∀ ε : ℝ, 0 < ε → Tendsto (fun i => μ i {ω | ε ≤ ‖X i ω - g i ω‖}) l (𝓝 0)Proof (Lean source)
theorem tendstoInProbability_iff_norm {ι : Type*} {Ω : ι → Type*} [∀ i, MeasurableSpace (Ω i)] {E : Type*} [SeminormedAddCommGroup E] (μ : (i : ι) → Measure (Ω i)) (X : (i : ι) → Ω i → E) (l : Filter ι) (g : (i : ι) → Ω i → E) : TendstoInProbability μ X l g ↔ ∀ ε : ℝ, 0 < ε → Tendsto (fun i => μ i {ω | ε ≤ ‖X i ω - g i ω‖}) l (𝓝 0) := by simpa only [dist_eq_norm_sub] using (tendstoInProbability_iff_dist (μ := μ) (X := X) (l := l) (g := g)) -
tendstoInProbability_iff_measureReal_normtheorem — For finite row measures, seminormed-group-valued row variables, a filter, and row limits, convergence in probability is equivalent to the real-valued measure of every positive norm tail tending to zero.hypothesesι :Type*ι → Type*∀ i, MeasurableSpace (Ω i)E :Type*μ :(i : ι) → Measure (Ω i)∀ i, IsFiniteMeasure (μ i)X :(i : ι) → Ω i → El :Filter ιg :(i : ι) → Ω i → EconclusionTendstoInProbability μ X l gProof (Lean source)
theorem tendstoInProbability_iff_measureReal_norm {ι : Type*} {Ω : ι → Type*} [∀ i, MeasurableSpace (Ω i)] {E : Type*} [SeminormedAddCommGroup E] (μ : (i : ι) → Measure (Ω i)) [∀ i, IsFiniteMeasure (μ i)] (X : (i : ι) → Ω i → E) (l : Filter ι) (g : (i : ι) → Ω i → E) : TendstoInProbability μ X l g ↔ ∀ ε : ℝ, 0 < ε → Tendsto (fun i => (μ i).real {ω | ε ≤ ‖X i ω - g i ω‖}) l (𝓝 0) := by rw [tendstoInProbability_iff_norm] congr! with ε hε simp_rw [measureReal_def, ENNReal.tendsto_toReal_zero_iff (fun i => measure_ne_top (μ i) _)] -
tendstoInLaw_iff_boundedContinuoustheorem — For row probability measures, row random variables, an index filter, and a target probability law, convergence in law is equivalent to row measurability together with convergence of expectations of every bounded continuous real test function.hypothesesι :Type*ι → Type*∀ i, MeasurableSpace (Ω i)E :μ :(i : ι) → Measure (Ω i)∀ i, IsProbabilityMeasure (μ i)X :(i : ι) → Ω i → El :Filter ιQ :conclusionTendstoInLaw μ X l Q ↔ (∀ i, AEMeasurable (X i) (μ i)) ∧∀ f : E →ᵇ ℝ, Tendsto (fun i => ∫ ω, f (X i ω) ∂μ i) l (𝓝 (∫ x, f x ∂Q))Proof (Lean source)
theorem tendstoInLaw_iff_boundedContinuous {ι : Type*} {Ω : ι → Type*} [∀ i, MeasurableSpace (Ω i)] {E : Type*} [MeasurableSpace E] [TopologicalSpace E] [OpensMeasurableSpace E] (μ : (i : ι) → Measure (Ω i)) [∀ i, IsProbabilityMeasure (μ i)] (X : (i : ι) → Ω i → E) (l : Filter ι) (Q : Measure E) [IsProbabilityMeasure Q] : TendstoInLaw μ X l Q ↔ (∀ i, AEMeasurable (X i) (μ i)) ∧ ∀ f : E →ᵇ ℝ, Tendsto (fun i => ∫ ω, f (X i ω) ∂μ i) l (𝓝 (∫ x, f x ∂Q)) := by constructor · intro h refine ⟨h.forall_aemeasurable, fun f => ?_⟩ have ht := ProbabilityMeasure.tendsto_iff_forall_integral_tendsto.mp h.tendsto f simpa only [ProbabilityMeasure.coe_mk, integral_map (h.forall_aemeasurable _) f.continuous.aestronglyMeasurable, integral_map measurable_id.aemeasurable f.continuous.aestronglyMeasurable, Function.comp_apply, id_eq] using ht · rintro ⟨hX, ht⟩ refine ⟨hX, by fun_prop, ?_⟩ apply ProbabilityMeasure.tendsto_iff_forall_integral_tendsto.mpr intro f simpa only [ProbabilityMeasure.coe_mk, integral_map (hX _) f.continuous.aestronglyMeasurable, integral_map measurable_id.aemeasurable f.continuous.aestronglyMeasurable, Function.comp_apply, id_eq] using ht f -
tendstoInProbability_consttheorem — For row probability measures, row random variables, an index filter, and a point defining the target Dirac law, if the variables converge in law to that Dirac law, then they converge in probability to the point.hypothesesι :Type*ι → Type*∀ i, MeasurableSpace (Ω i)E :μ :(i : ι) → Measure (Ω i)∀ i, IsProbabilityMeasure (μ i)X :(i : ι) → Ω i → El :Filter ιc :Eh :TendstoInLaw μ X l (Measure.dirac c)conclusionTendstoInProbability μ X l (fun _ _ => c)Proof (Lean source)
theorem TendstoInLaw.tendstoInProbability_const {ι : Type*} {Ω : ι → Type*} [∀ i, MeasurableSpace (Ω i)] {E : Type*} [MeasurableSpace E] [PseudoEMetricSpace E] [BorelSpace E] (μ : (i : ι) → Measure (Ω i)) [∀ i, IsProbabilityMeasure (μ i)] (X : (i : ι) → Ω i → E) (l : Filter ι) (c : E) (h : TendstoInLaw μ X l (Measure.dirac c)) : TendstoInProbability μ X l (fun _ _ => c) := by intro ε hε let F : Set E := {x | ε ≤ edist x c} have hF : IsClosed F := by exact isClosed_le continuous_const (continuous_edist.comp (continuous_id.prodMk continuous_const)) have hlimsup := ProbabilityMeasure.limsup_measure_closed_le_of_tendsto h.tendsto hF have hcF : (Measure.dirac c).map (id : E → E) F = 0 := by rw [Measure.map_id, Measure.dirac_apply' c hF.measurableSet] simp [F, hε.ne'] have hlimsup_zero : l.limsup (fun i => (μ i).map (X i) F) ≤ 0 := by simpa only [ProbabilityMeasure.coe_mk, hcF] using hlimsup rw [ENNReal.tendsto_nhds_zero] intro δ hδ have hevent : ∀ᶠ i in l, (μ i).map (X i) F < δ := ((Filter.limsup_le_iff (u := fun i => (μ i).map (X i) F) (x := (0 : ℝ≥0∞))).mp hlimsup_zero) δ hδ filter_upwards [hevent] with i hi rw [Measure.map_apply_of_aemeasurable (h.forall_aemeasurable i) hF.measurableSet] at hi exact hi.le -
uniformContinuous_comptheorem — If row random variables converge in probability to row limits and a map is uniformly continuous, then applying that map to both the variables and limits preserves convergence in probability.hypothesesι :Type*ι → Type*∀ i, MeasurableSpace (Ω i)E F :μ :(i : ι) → Measure (Ω i)X g :(i : ι) → Ω i → El :Filter ιf :E → Fh :TendstoInProbability μ X l ghf :conclusionTendstoInProbability μ (fun i ω => f (X i ω)) l (fun i ω => f (g i ω))Proof (Lean source)
theorem TendstoInProbability.uniformContinuous_comp {ι : Type*} {Ω : ι → Type*} [∀ i, MeasurableSpace (Ω i)] {E F : Type*} [PseudoEMetricSpace E] [PseudoEMetricSpace F] {μ : (i : ι) → Measure (Ω i)} {X g : (i : ι) → Ω i → E} {l : Filter ι} {f : E → F} (h : TendstoInProbability μ X l g) (hf : UniformContinuous f) : TendstoInProbability μ (fun i ω => f (X i ω)) l (fun i ω => f (g i ω)) := by intro ε hε obtain ⟨δ, hδ, hmap⟩ := EMetric.uniformContinuous_iff.mp hf ε hε refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds (h δ hδ) (fun _ => zero_le) ?_ intro i refine measure_mono fun ω hω => ?_ by_contra hnot exact (not_lt_of_ge hω) (hmap (lt_of_not_ge hnot)) -
first_preimage_letheorem — Given a coupling with prescribed marginals and a set in the first coordinate space, the first-coordinate pullback has no more mass than that set has under its first marginal.hypothesesX :Type uY :Type vν :Measure (X × Y)μ :Measure Xρ :Measure Yhν :IsCoupling ν μ ρs :Set Xconclusionν (fst ⁻¹' s) ≤ μ sProof (Lean source)
theorem first_preimage_le {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {ν : Measure (X × Y)} {μ : Measure X} {ρ : Measure Y} (hν : IsCoupling ν μ ρ) (s : Set X) : ν (fst ⁻¹' s) ≤ μ s := by simpa only [hν.map_fst] using (Measure.le_map_apply (μ := ν) (f := fst) measurable_fst.aemeasurable s) -
second_preimage_letheorem — Given a coupling with prescribed marginals and a set in the second coordinate space, the second-coordinate pullback has no more mass than that set has under its second marginal.hypothesesX :Type uY :Type vν :Measure (X × Y)μ :Measure Xρ :Measure Yhν :IsCoupling ν μ ρs :Set Yconclusionν (snd ⁻¹' s) ≤ ρ sProof (Lean source)
theorem second_preimage_le {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {ν : Measure (X × Y)} {μ : Measure X} {ρ : Measure Y} (hν : IsCoupling ν μ ρ) (s : Set Y) : ν (snd ⁻¹' s) ≤ ρ s := by simpa only [hν.map_snd] using (Measure.le_map_apply (μ := ν) (f := snd) measurable_snd.aemeasurable s) -
first_preimage_eqtheorem — Given a coupling with prescribed marginals and a measurable set in the first coordinate space, the first-coordinate pullback has exactly the mass assigned by the first marginal.hypothesesX :Type uY :Type vν :Measure (X × Y)μ :Measure Xρ :Measure Yhν :IsCoupling ν μ ρs :Set Xhs :conclusionν (fst ⁻¹' s) = μ sProof (Lean source)
theorem first_preimage_eq {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {ν : Measure (X × Y)} {μ : Measure X} {ρ : Measure Y} (hν : IsCoupling ν μ ρ) {s : Set X} (hs : MeasurableSet s) : ν (fst ⁻¹' s) = μ s := by simpa only [hν.map_fst] using (Measure.map_apply (μ := ν) measurable_fst hs).symm -
second_preimage_eqtheorem — Given a coupling with prescribed marginals and a measurable set in the second coordinate space, the second-coordinate pullback has exactly the mass assigned by the second marginal.hypothesesX :Type uY :Type vν :Measure (X × Y)μ :Measure Xρ :Measure Yhν :IsCoupling ν μ ρs :Set Yhs :conclusionν (snd ⁻¹' s) = ρ sProof (Lean source)
theorem second_preimage_eq {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {ν : Measure (X × Y)} {μ : Measure X} {ρ : Measure Y} (hν : IsCoupling ν μ ρ) {s : Set Y} (hs : MeasurableSet s) : ν (snd ⁻¹' s) = ρ s := by simpa only [hν.map_snd] using (Measure.map_apply (μ := ν) measurable_snd hs).symm -
pair_tail_letheorem — Given a coupling with prescribed marginals, first and second observables, their constant limits, and a deviation threshold, the pair's tail probability is bounded by the sum of the two marginal tail probabilities.hypothesesX :Type uY :Type vE F :ν :Measure (X × Y)μ :Measure Xρ :Measure Yhν :IsCoupling ν μ ρU :X → EV :Y → Fa :Eb :Fε :ℝ≥0∞Proof (Lean source)
theorem pair_tail_le {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] {E F : Type*} [PseudoEMetricSpace E] [PseudoEMetricSpace F] {ν : Measure (X × Y)} {μ : Measure X} {ρ : Measure Y} (hν : IsCoupling ν μ ρ) (U : X → E) (V : Y → F) (a : E) (b : F) (ε : ℝ≥0∞) : ν {p | ε ≤ edist (U p.1, V p.2) (a, b)} ≤ μ {x | ε ≤ edist (U x) a} + ρ {y | ε ≤ edist (V y) b} := by calc ν {p | ε ≤ edist (U p.1, V p.2) (a, b)} ≤ ν ((fst ⁻¹' {x | ε ≤ edist (U x) a}) ∪ (snd ⁻¹' {y | ε ≤ edist (V y) b})) := by apply measure_mono intro p hp simpa only [Set.mem_union, Set.mem_preimage, Set.mem_ofPred_eq, Prod.edist_eq, le_max_iff] using hp _ ≤ ν (fst ⁻¹' {x | ε ≤ edist (U x) a}) + ν (snd ⁻¹' {y | ε ≤ edist (V y) b}) := measure_union_le _ _ _ ≤ μ {x | ε ≤ edist (U x) a} + ρ {y | ε ≤ edist (V y) b} := add_le_add (first_preimage_le hν _) (second_preimage_le hν _) -
pair_tendstoInProbabilitytheorem — Given first and second row measures, row coupling measures, proof that each row is a coupling, the two row observables, their constant limits, an index filter, and their two marginal convergence-in-probability statements, the paired observables converge in probability to the pair of limits under every row coupling.hypothesesι :Type*ι → Type uι → Type v∀ i, MeasurableSpace (X i)∀ i, MeasurableSpace (Y i)E F :μ :(i : ι) → Measure (X i)ρ :(i : ι) → Measure (Y i)ν :(i : ι) → Measure (X i × Y i)hν :∀ i, IsCoupling (ν i) (μ i) (ρ i)U :(i : ι) → X i → EV :(i : ι) → Y i → Fa :Eb :Fl :Filter ιhU :TendstoInProbability μ U l (fun _ _ => a)hV :TendstoInProbability ρ V l (fun _ _ => b)conclusionTendstoInProbability ν (fun i p => (U i p.1, V i p.2)) l (fun _ _ => (a, b))Proof (Lean source)
theorem pair_tendstoInProbability {ι : Type*} {X : ι → Type u} {Y : ι → Type v} [∀ i, MeasurableSpace (X i)] [∀ i, MeasurableSpace (Y i)] {E F : Type*} [PseudoEMetricSpace E] [PseudoEMetricSpace F] (μ : (i : ι) → Measure (X i)) (ρ : (i : ι) → Measure (Y i)) (ν : (i : ι) → Measure (X i × Y i)) (hν : ∀ i, IsCoupling (ν i) (μ i) (ρ i)) (U : (i : ι) → X i → E) (V : (i : ι) → Y i → F) (a : E) (b : F) (l : Filter ι) (hU : TendstoInProbability μ U l (fun _ _ => a)) (hV : TendstoInProbability ρ V l (fun _ _ => b)) : TendstoInProbability ν (fun i p => (U i p.1, V i p.2)) l (fun _ _ => (a, b)) := by intro ε hε have hsum : Tendsto (fun i => μ i {x | ε ≤ edist (U i x) a} + ρ i {y | ε ≤ edist (V i y) b}) l (𝓝 0) := by simpa using (hU ε hε).add (hV ε hε) exact tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hsum (fun _ => zero_le) (fun i => pair_tail_le (hν i) (U i) (V i) a b ε) -
aemeasurable_pairtheorem — Given first and second row measures, row coupling measures, proof that each row is a coupling, the two row observables, and their marginal almost-everywhere measurability, the paired observable is almost-everywhere measurable under every row coupling.hypothesesι :Type*ι → Type uι → Type v∀ i, MeasurableSpace (X i)∀ i, MeasurableSpace (Y i)E F :μ :(i : ι) → Measure (X i)ρ :(i : ι) → Measure (Y i)ν :(i : ι) → Measure (X i × Y i)hν :∀ i, IsCoupling (ν i) (μ i) (ρ i)U :(i : ι) → X i → EV :(i : ι) → Y i → FhU :∀ i, AEMeasurable (U i) (μ i)hV :∀ i, AEMeasurable (V i) (ρ i)i :conclusionAEMeasurable (fun p : X i × Y i => (U i p.1, V i p.2)) (ν i)Proof (Lean source)
theorem aemeasurable_pair {ι : Type*} {X : ι → Type u} {Y : ι → Type v} [∀ i, MeasurableSpace (X i)] [∀ i, MeasurableSpace (Y i)] {E F : Type*} [MeasurableSpace E] [MeasurableSpace F] (μ : (i : ι) → Measure (X i)) (ρ : (i : ι) → Measure (Y i)) (ν : (i : ι) → Measure (X i × Y i)) (hν : ∀ i, IsCoupling (ν i) (μ i) (ρ i)) (U : (i : ι) → X i → E) (V : (i : ι) → Y i → F) (hU : ∀ i, AEMeasurable (U i) (μ i)) (hV : ∀ i, AEMeasurable (V i) (ρ i)) : ∀ i, AEMeasurable (fun p : X i × Y i => (U i p.1, V i p.2)) (ν i) := by intro i have hfirst : AEMeasurable (fun p : X i × Y i => U i p.1) (ν i) := by have h : AEMeasurable (U i) ((ν i).map fst) := by rw [(hν i).map_fst] exact hU i exact h.comp_measurable measurable_fst have hsecond : AEMeasurable (fun p : X i × Y i => V i p.2) (ν i) := by have h : AEMeasurable (V i) ((ν i).map snd) := by rw [(hν i).map_snd] exact hV i exact h.comp_measurable measurable_snd exact hfirst.prodMk hsecond -
aemeasurable_maptheorem — Given first and second row measures, row coupling measures, proof that each row is a coupling, the two row observables, a measurable map, and their marginal almost-everywhere measurability, the mapped paired observable is almost-everywhere measurable under every row coupling.hypothesesι :Type*ι → Type uι → Type v∀ i, MeasurableSpace (X i)∀ i, MeasurableSpace (Y i)E F G :μ :(i : ι) → Measure (X i)ρ :(i : ι) → Measure (Y i)ν :(i : ι) → Measure (X i × Y i)hν :∀ i, IsCoupling (ν i) (μ i) (ρ i)U :(i : ι) → X i → EV :(i : ι) → Y i → Ff :E × F → Ghf :hU :∀ i, AEMeasurable (U i) (μ i)hV :∀ i, AEMeasurable (V i) (ρ i)i :conclusionAEMeasurable (fun p : X i × Y i => f (U i p.1, V i p.2)) (ν i)Proof (Lean source)
theorem aemeasurable_map {ι : Type*} {X : ι → Type u} {Y : ι → Type v} [∀ i, MeasurableSpace (X i)] [∀ i, MeasurableSpace (Y i)] {E F G : Type*} [MeasurableSpace E] [MeasurableSpace F] [MeasurableSpace G] (μ : (i : ι) → Measure (X i)) (ρ : (i : ι) → Measure (Y i)) (ν : (i : ι) → Measure (X i × Y i)) (hν : ∀ i, IsCoupling (ν i) (μ i) (ρ i)) (U : (i : ι) → X i → E) (V : (i : ι) → Y i → F) (f : E × F → G) (hf : Measurable f) (hU : ∀ i, AEMeasurable (U i) (μ i)) (hV : ∀ i, AEMeasurable (V i) (ρ i)) : ∀ i, AEMeasurable (fun p : X i × Y i => f (U i p.1, V i p.2)) (ν i) := by intro i exact hf.comp_aemeasurable (aemeasurable_pair μ ρ ν hν U V hU hV i) -
measurable_map_tendstoInProbabilitytheorem — Given first and second row measures, row coupling measures, proof that each row is a coupling, the two row observables, their constant limits, an index filter, a measurable map continuous at the limiting pair, marginal almost-everywhere measurability, and marginal convergence in probability, the mapped paired observable is almost-everywhere measurable and converges in probability under every row coupling.hypothesesι :Type*ι → Type uι → Type v∀ i, MeasurableSpace (X i)∀ i, MeasurableSpace (Y i)E F G :μ :(i : ι) → Measure (X i)ρ :(i : ι) → Measure (Y i)ν :(i : ι) → Measure (X i × Y i)hν :∀ i, IsCoupling (ν i) (μ i) (ρ i)U :(i : ι) → X i → EV :(i : ι) → Y i → Fa :Eb :Fl :Filter ιf :E × F → Ghf :hfc :ContinuousAt f (a, b)hUae :∀ i, AEMeasurable (U i) (μ i)hVae :∀ i, AEMeasurable (V i) (ρ i)hU :TendstoInProbability μ U l (fun _ _ => a)hV :TendstoInProbability ρ V l (fun _ _ => b)conclusionconclusion 2TendstoInProbability ν (fun i p => f (U i p.1, V i p.2)) l (fun _ _ => f (a, b))Proof (Lean source)
theorem measurable_map_tendstoInProbability {ι : Type*} {X : ι → Type u} {Y : ι → Type v} [∀ i, MeasurableSpace (X i)] [∀ i, MeasurableSpace (Y i)] {E F G : Type*} [PseudoMetricSpace E] [PseudoMetricSpace F] [PseudoMetricSpace G] [MeasurableSpace E] [MeasurableSpace F] [MeasurableSpace G] (μ : (i : ι) → Measure (X i)) (ρ : (i : ι) → Measure (Y i)) (ν : (i : ι) → Measure (X i × Y i)) (hν : ∀ i, IsCoupling (ν i) (μ i) (ρ i)) (U : (i : ι) → X i → E) (V : (i : ι) → Y i → F) (a : E) (b : F) (l : Filter ι) (f : E × F → G) (hf : Measurable f) (hfc : ContinuousAt f (a, b)) (hUae : ∀ i, AEMeasurable (U i) (μ i)) (hVae : ∀ i, AEMeasurable (V i) (ρ i)) (hU : TendstoInProbability μ U l (fun _ _ => a)) (hV : TendstoInProbability ρ V l (fun _ _ => b)) : (∀ i, AEMeasurable (fun p : X i × Y i => f (U i p.1, V i p.2)) (ν i)) ∧ TendstoInProbability ν (fun i p => f (U i p.1, V i p.2)) l (fun _ _ => f (a, b)) := by exact ⟨aemeasurable_map μ ρ ν hν U V f hf hUae hVae, map_tendstoInProbability μ ρ ν hν U V a b l f hfc hU hV⟩ -
measurable_sqrtRatioFallbacktheorem — The total square-root-ratio statistic with a zero fallback is Borel measurable.conclusionProof (Lean source)
theorem measurable_sqrtRatioFallback : Measurable sqrtRatioFallback := by change Measurable (fun p : ℝ × ℝ => if 0 < p.2 then sqrt (p.1 / p.2) else 0) exact Measurable.ite (measurableSet_Ioi.preimage measurable_snd) ((measurable_fst.div measurable_snd).sqrt) measurable_const -
continuousAt_sqrtRatioFallbacktheorem — Given a strictly positive limiting denominator, the total square-root-ratio statistic is continuous at the limiting numerator--denominator pair.Proof (Lean source)
theorem continuousAt_sqrtRatioFallback {a b : ℝ} (hb : 0 < b) : ContinuousAt sqrtRatioFallback (a, b) := by have hc : ContinuousAt (fun p : ℝ × ℝ => sqrt (p.1 / p.2)) (a, b) := Real.continuous_sqrt.continuousAt.comp (continuousAt_fst.div continuousAt_snd (ne_of_gt hb)) apply hc.congr_of_eventuallyEq filter_upwards [continuousAt_snd.eventually (Ioi_mem_nhds hb)] with p hp simp [sqrtRatioFallback, hp] -
sqrtRatioFallback_tendstoInProbabilitytheorem — Given first and second row measures, row coupling measures, proof that each row is a coupling, row numerator and denominator observables, their limits, a positive denominator limit, an index filter, and marginal convergence in probability, the total square-root ratio converges in probability under every row coupling.hypothesesι :Type*ι → Type uι → Type v∀ i, MeasurableSpace (X i)∀ i, MeasurableSpace (Y i)μ :(i : ι) → Measure (X i)ρ :(i : ι) → Measure (Y i)ν :(i : ι) → Measure (X i × Y i)hν :∀ i, IsCoupling (ν i) (μ i) (ρ i)U :(i : ι) → X i → ℝV :(i : ι) → Y i → ℝa b :ℝhb :0 < bl :Filter ιhU :TendstoInProbability μ U l (fun _ _ => a)hV :TendstoInProbability ρ V l (fun _ _ => b)conclusionTendstoInProbability ν (fun i p => sqrtRatioFallback (U i p.1, V i p.2)) l (fun _ _ => sqrt (a / b))Proof (Lean source)
theorem sqrtRatioFallback_tendstoInProbability {ι : Type*} {X : ι → Type u} {Y : ι → Type v} [∀ i, MeasurableSpace (X i)] [∀ i, MeasurableSpace (Y i)] (μ : (i : ι) → Measure (X i)) (ρ : (i : ι) → Measure (Y i)) (ν : (i : ι) → Measure (X i × Y i)) (hν : ∀ i, IsCoupling (ν i) (μ i) (ρ i)) (U : (i : ι) → X i → ℝ) (V : (i : ι) → Y i → ℝ) (a b : ℝ) (hb : 0 < b) (l : Filter ι) (hU : TendstoInProbability μ U l (fun _ _ => a)) (hV : TendstoInProbability ρ V l (fun _ _ => b)) : TendstoInProbability ν (fun i p => sqrtRatioFallback (U i p.1, V i p.2)) l (fun _ _ => sqrt (a / b)) := by simpa [sqrtRatioFallback, hb] using (map_tendstoInProbability μ ρ ν hν U V a b l sqrtRatioFallback (continuousAt_sqrtRatioFallback hb) hU hV) -
sqrtRatioFallback_eq_sqrt_divlemma — Given a numerator and denominator with a nonnegative denominator, the total square-root-ratio statistic equals the ordinary square-root ratio.Proof (Lean source)
lemma sqrtRatioFallback_eq_sqrt_div {a b : ℝ} (hb : 0 ≤ b) : sqrtRatioFallback (a, b) = sqrt (a / b) := by by_cases hpos : 0 < b · simp [sqrtRatioFallback, hpos] · have hz : b = 0 := le_antisymm (not_lt.mp hpos) hb simp [sqrtRatioFallback, hz] -
tendstoInProbability_iff_strict_abslemma — For row measures, real-valued row variables, a constant limit, and an index filter, convergence in probability is equivalent to convergence to zero of every strict absolute-error tail.hypothesesι :Type*ι → Type*∀ i, MeasurableSpace (X i)μ :(i : ι) → Measure (X i)U :(i : ι) → X i → ℝa :ℝl :Filter ιconclusionTendstoInProbability μ U l (fun _ _ => a)Proof (Lean source)
lemma tendstoInProbability_iff_strict_abs {ι : Type*} {X : ι → Type*} [∀ i, MeasurableSpace (X i)] (μ : (i : ι) → Measure (X i)) (U : (i : ι) → X i → ℝ) (a : ℝ) (l : Filter ι) : TendstoInProbability μ U l (fun _ _ => a) ↔ ∀ δ : ℝ, 0 < δ → Tendsto (fun i => μ i {x | δ < |U i x - a|}) l (nhds 0) := by rw [tendstoInProbability_iff_norm] constructor · intro h δ hδ refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds (h δ hδ) (fun _ => zero_le) ?_ intro i refine measure_mono fun x hx => ?_ change δ < |U i x - a| at hx change δ ≤ ‖U i x - a‖ simpa only [Real.norm_eq_abs] using hx.le · intro h δ hδ refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds (h (δ / 2) (by positivity)) (fun _ => zero_le) ?_ intro i refine measure_mono fun x hx => ?_ change δ ≤ ‖U i x - a‖ at hx change δ / 2 < |U i x - a| simpa only [Real.norm_eq_abs] using (half_lt_self hδ).trans_le hx -
coupled_sqrtRatio_tendstoInProbabilitylemma — Given first and second row measures, row coupling measures, proof that each row has the prescribed marginals, row numerator and denominator observables, their limits, a positive denominator limit, an index filter, pointwise nonnegativity of every denominator observable, and marginal convergence in probability, the ordinary square-root ratio converges in probability under every row coupling.hypothesesι :Type*ι → Type*ι → Type*∀ i, MeasurableSpace (X i)∀ i, MeasurableSpace (Y i)μ :(i : ι) → Measure (X i)ρ :(i : ι) → Measure (Y i)ν :(i : ι) → Measure (X i × Y i)hν :∀ i, IsCoupling (ν i) (μ i) (ρ i)U :(i : ι) → X i → ℝV :(i : ι) → Y i → ℝa b :ℝhb :0 < bl :Filter ιhVnonneg :∀ i y, 0 ≤ V i yhU :TendstoInProbability μ U l (fun _ _ => a)hV :TendstoInProbability ρ V l (fun _ _ => b)conclusionProof (Lean source)
lemma coupled_sqrtRatio_tendstoInProbability {ι : Type*} {X : ι → Type*} {Y : ι → Type*} [∀ i, MeasurableSpace (X i)] [∀ i, MeasurableSpace (Y i)] (μ : (i : ι) → Measure (X i)) (ρ : (i : ι) → Measure (Y i)) (ν : (i : ι) → Measure (X i × Y i)) (hν : ∀ i, IsCoupling (ν i) (μ i) (ρ i)) (U : (i : ι) → X i → ℝ) (V : (i : ι) → Y i → ℝ) (a b : ℝ) (hb : 0 < b) (l : Filter ι) (hVnonneg : ∀ i y, 0 ≤ V i y) (hU : TendstoInProbability μ U l (fun _ _ => a)) (hV : TendstoInProbability ρ V l (fun _ _ => b)) : TendstoInProbability ν (fun i q => sqrt (U i q.1 / V i q.2)) l (fun _ _ => sqrt (a / b)) := by have h := sqrtRatioFallback_tendstoInProbability μ ρ ν hν U V a b hb l hU hV have hfun : (fun (i : ι) (q : X i × Y i) => sqrtRatioFallback (U i q.1, V i q.2)) = (fun (i : ι) (q : X i × Y i) => sqrt (U i q.1 / V i q.2)) := by funext i q exact sqrtRatioFallback_eq_sqrt_div (hVnonneg i q.2) rw [← hfun] exact h -
coupled_sqrtRatio_tendsto_strict_abslemma — Given first and second row measures, row coupling measures, proof that each row has the prescribed marginals, row numerator and denominator observables, their limits, a positive denominator limit, an index filter, pointwise nonnegativity of every denominator observable, and strict-tail convergence of both marginals, every strict absolute-error tail of the ordinary square-root ratio tends to zero under the coupling.hypothesesι :Type*ι → Type*ι → Type*∀ i, MeasurableSpace (X i)∀ i, MeasurableSpace (Y i)μ :(i : ι) → Measure (X i)ρ :(i : ι) → Measure (Y i)ν :(i : ι) → Measure (X i × Y i)hν :∀ i, IsCoupling (ν i) (μ i) (ρ i)U :(i : ι) → X i → ℝV :(i : ι) → Y i → ℝa b :ℝhb :0 < bl :Filter ιhVnonneg :∀ i y, 0 ≤ V i yδ :ℝ0 < δProof (Lean source)
lemma coupled_sqrtRatio_tendsto_strict_abs {ι : Type*} {X : ι → Type*} {Y : ι → Type*} [∀ i, MeasurableSpace (X i)] [∀ i, MeasurableSpace (Y i)] (μ : (i : ι) → Measure (X i)) (ρ : (i : ι) → Measure (Y i)) (ν : (i : ι) → Measure (X i × Y i)) (hν : ∀ i, IsCoupling (ν i) (μ i) (ρ i)) (U : (i : ι) → X i → ℝ) (V : (i : ι) → Y i → ℝ) (a b : ℝ) (hb : 0 < b) (l : Filter ι) (hVnonneg : ∀ i y, 0 ≤ V i y) (hU : ∀ δ : ℝ, 0 < δ → Tendsto (fun i => μ i {x | δ < |U i x - a|}) l (nhds 0)) (hV : ∀ δ : ℝ, 0 < δ → Tendsto (fun i => ρ i {y | δ < |V i y - b|}) l (nhds 0)) : ∀ δ : ℝ, 0 < δ → Tendsto (fun i => ν i {q | δ < |sqrt (U i q.1 / V i q.2) - sqrt (a / b)|}) l (nhds 0) := by rw [← tendstoInProbability_iff_strict_abs] exact coupled_sqrtRatio_tendstoInProbability μ ρ ν hν U V a b hb l hVnonneg ((tendstoInProbability_iff_strict_abs μ U a l).2 hU) ((tendstoInProbability_iff_strict_abs ρ V b l).2 hV)
Convergence 5 core · 11 supporting Defines extended-metric-valued convergence in probability, scalar L² convergence and convergence in distribution, and normed-space stochastic-order notation used by the estimation layer. ★ tightness★ const_mul_tendsto_zero
Defines extended-metric-valued convergence in probability, scalar L² convergence and convergence in distribution, and normed-space stochastic-order notation used by the estimation layer.
The core predicates are Tendsto_L2, IsBigOp, and IsLittleOp; convergence in probability and
in law along a sequence on a fixed probability space are Modes.TendstoInProbability and
Modes.TendstoInLaw with constant row laws, unfolded by Tendsto_inProb_iff and
Tendsto_dist_iff. The main theorem set includes deterministic-scalar
Slutsky for distributional convergence (Modes.TendstoInLaw.const_mul_tendsto),
tightness from convergence in distribution (Modes.TendstoInLaw.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_L2 reviewed
⚑ flagged
Causalean.Stat
Given a sequence of real-valued random variables, a real-valued limiting random variable, and a measure on a measurable sample space, convergence means that the norm of the difference between the indexed random variable and the limit tends to zero as the index tends to infinity.
abbrev IsBigOp reviewed
⚑ flagged
Causalean.Stat
Given a sequence of random variables in a seminormed additive group, a real-valued rate sequence, and a measure on a measurable sample space, boundedness in probability at that rate — the familiar Xₙ = O_p(rₙ) — is the sequence specialization of the filter-general stochastic-boundedness predicate.
Definition (Lean source)
abbrev IsLittleOp reviewed
⚑ flagged
Causalean.Stat
Given a sequence of random variables in a seminormed additive group, a real-valued rate sequence, and a measure on a measurable sample space, negligibility in probability relative to that rate — the familiar Xₙ = o_p(rₙ) — is the sequence specialization of the filter-general stochastic little-o predicate.
Definition (Lean source)
theorem tightness reviewed
⚑ flagged
Causalean.Stat.Modes.TendstoInLaw
A real sequence that converges in distribution to a probability law is bounded in probability at the constant rate one.
Formal statement
Proof (Lean source)
theorem Modes.TendstoInLaw.tightness
{Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
{Xn : ℕ → Ω → ℝ} {Q : Measure ℝ} [IsProbabilityMeasure Q]
(hX : Modes.TendstoInLaw (fun _ : ℕ => μ) Xn atTop Q) :
IsBigOp Xn (fun _ => (1 : ℝ)) μ := by
have hXn : ∀ n, AEMeasurable (Xn n) μ := hX.forall_aemeasurable
intro δ hδ
by_cases hδtop : δ = ⊤
· exact ⟨1, one_pos, by simp [hδtop]⟩
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 hhalf_pos : 0 < δ / 2 := ENNReal.div_pos hδ.ne' (by norm_num)
have hQevent := (ENNReal.tendsto_nhds_zero.mp hQtail) (δ / 2) hhalf_pos
obtain ⟨N, hN⟩ := hQevent.exists
refine ⟨(N + 1 : ℕ), by positivity, ?_⟩
let F : Set ℝ := s N
have hFclosed : IsClosed F := by
exact isClosed_le continuous_const continuous_abs
rw [Tendsto_dist_iff Xn Q μ hXn] 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 hpoint : ∀ n, μ {ω | ((N + 1 : ℕ) : ℝ) * (fun _ => (1 : ℝ)) n ≤ |Xn n ω|}
≤ ((νs n : ProbabilityMeasure ℝ) : Measure ℝ) F := by
intro n
change μ {ω | ((N + 1 : ℕ) : ℝ) * (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 hNle : (N : ℝ) ≤ ((N + 1 : ℕ) : ℝ) := by norm_num
exact hNle.trans (by simpa using hω)
have hlim : limsup
(fun n => μ {ω | ((N + 1 : ℕ) : ℝ) * (fun _ => (1 : ℝ)) n ≤ |Xn n ω|})
atTop ≤ δ / 2 := calc
_ ≤ limsup
(fun n => ((νs n : ProbabilityMeasure ℝ) : Measure ℝ) F) atTop :=
Filter.limsup_le_limsup (Eventually.of_forall hpoint)
_ ≤ (ν : Measure ℝ) F := hpm
_ = Q F := rfl
_ ≤ δ / 2 := by simpa [F] using hN
have hhalf_lt : δ / 2 < δ := ENNReal.half_lt_self hδ.ne' hδtop
exact (((Filter.limsup_le_iff
(u := fun n => μ {ω | ((N + 1 : ℕ) : ℝ) * (fun _ => (1 : ℝ)) n ≤ |Xn n ω|})
(x := δ / 2)).mp hlim) δ hhalf_lt).mono fun _ hi => hi.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
have haLittle : Modes.IsLittleOpF (fun _ => μ) (fun n (_ : Ω) => a n) atTop
(fun _ => (1 : ℝ)) := by
intro ε hε
rw [ENNReal.tendsto_nhds_zero]
intro δ hδ
have haevent : ∀ᶠ n in atTop, |a n| < ε := by
have ht := (Metric.tendsto_nhds.mp ha) ε hε
simpa [Real.dist_eq] using ht
filter_upwards [haevent] with n hn
rw [show {ω : Ω | ε * (1 : ℝ) ≤ ‖a n‖} = ∅ by
ext ω
simp [Real.norm_eq_abs, not_le.mpr hn]]
simp
simpa only [one_mul] using Modes.IsLittleOpF.mul_boundedInProbability haLittle hX
(Eventually.of_forall fun _ => zero_lt_one)
(Eventually.of_forall fun _ => zero_lt_one)
11 supporting declarations (lemmas, instances)
-
Tendsto_inProb_ifflemma — Convergence in probability of a sequence in an extended-distance space to a limit under a measure is exactly convergence in measure of that sequence along the natural numbers.hypothesesconclusionModes.TendstoInProbability (fun _ : ℕ => μ) Xn atTop (fun _ => X)↔ TendstoInMeasure μ Xn atTop XProof (Lean source)
@[causal_defs_simps] lemma Tendsto_inProb_iff {E : Type*} [EDist E] (Xn : ℕ → Ω → E) (X : Ω → E) (μ : Measure Ω) : Modes.TendstoInProbability (fun _ : ℕ => μ) Xn atTop (fun _ => X) ↔ TendstoInMeasure μ Xn atTop X := Iff.rfl -
Tendsto_dist_ifflemma — Convergence in distribution of a sequence of real random variables to a probability law on the real line is exactly convergence, in the space of probability measures on the real line, of the pushforward laws of the random variables to that law.hypothesesconclusionModes.TendstoInLaw (fun _ : ℕ => μ) Xn atTop Q↔ Tendsto (β := ProbabilityMeasure ℝ) (fun n => ⟨μ.map (Xn n), Measure.isProbabilityMeasure_map (hXn n)⟩) atTop (𝓝 ⟨Q, ‹IsProbabilityMeasure Q›⟩)Proof (Lean source)
@[causal_defs_simps] lemma Tendsto_dist_iff (Xn : ℕ → Ω → ℝ) (Q : Measure ℝ) (μ : Measure Ω) [IsProbabilityMeasure μ] [IsProbabilityMeasure Q] (hXn : ∀ n, AEMeasurable (Xn n) μ) : Modes.TendstoInLaw (fun _ : ℕ => μ) Xn atTop Q ↔ Tendsto (β := ProbabilityMeasure ℝ) (fun n => ⟨μ.map (Xn n), Measure.isProbabilityMeasure_map (hXn n)⟩) atTop (𝓝 ⟨Q, ‹IsProbabilityMeasure Q›⟩) := by constructor · intro h simpa only [ProbabilityMeasure.coe_mk, Measure.map_id] using h.tendsto · intro h refine ⟨hXn, by fun_prop, ?_⟩ simpa only [ProbabilityMeasure.coe_mk, Measure.map_id] using h -
const_mul_tendstotheorem — If a real sequence converges in distribution and deterministic scalar multipliers converge to a constant, then the laws of the scaled sequence converge weakly to the limiting law scaled by that constant.hypothesesconclusionTendsto (β := ProbabilityMeasure ℝ) (fun n => ⟨μ.map (fun ω => a n * Xn n ω), Measure.isProbabilityMeasure_map ((measurable_const.mul measurable_id).aemeasurable.comp_aemeasurable (hX.forall_aemeasurable n))⟩) atTop (𝓝 ⟨Q.map (fun x : ℝ => a₀ * x), Measure.isProbabilityMeasure_map (measurable_const.mul measurable_id).aemeasurable⟩)Proof (Lean source)
theorem Modes.TendstoInLaw.const_mul_tendsto {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] {Xn : ℕ → Ω → ℝ} {Q : Measure ℝ} [IsProbabilityMeasure Q] {a : ℕ → ℝ} {a₀ : ℝ} (hX : Modes.TendstoInLaw (fun _ : ℕ => μ) Xn atTop Q) (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 (hX.forall_aemeasurable n))⟩) atTop (𝓝 ⟨Q.map (fun x : ℝ => a₀ * x), Measure.isProbabilityMeasure_map (measurable_const.mul measurable_id).aemeasurable⟩) := by have hXn : ∀ n, AEMeasurable (Xn n) μ := hX.forall_aemeasurable 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 have hX' := (Tendsto_dist_iff Xn Q μ hXn).mp 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.hypothesesΩ :sharedType u_1ℕ → Ω → ℝℕ → Ω → ℝrn :sharedℕ → ℝhrn_nonneg :∀ᶠ n : ℕ in atTop, 0 ≤ rn nhX :IsLittleOp Xn rn μhY :IsLittleOp Yn rn μconclusionIsLittleOp (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 μ := Modes.IsLittleOpF.add hX hY hrn_nonneg -
of_abs_le_const_multheorem — Domination by a positive constant times a stochastic little-o term preserves the stochastic little-o rate.hypothesesΩ :sharedType u_1ℕ → Ω → ℝℕ → Ω → ℝrn :sharedℕ → ℝC :ℝhC :0 < ChY :IsLittleOp Yn rn μhbound :∀ n ω, |Xn n ω| ≤ C * |Yn n ω|conclusionIsLittleOp 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ω change (ε / C) * rn n ≤ |Yn n ω| rw [div_mul_eq_mul_div, div_le_iff₀ hC] calc ε * rn n ≤ |Xn n ω| := by simpa [Real.norm_eq_abs] using hω _ ≤ C * |Yn n ω| := hbound n ω _ = |Yn n ω| * C := mul_comm _ _ -
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 -
of_abs_le_const_mul_one_on_eventtheorem — Given a positive constant, a sequence that is o_p(1), events whose complements have vanishing probability, and domination by that sequence on those events, the dominated sequence is itself o_p(1).hypothesesC :ℝG :ℕ → Set ΩhC :0 < ChY :IsLittleOp Yn (fun _ => (1 : ℝ)) μhbound :∀ n ωifω ∈ G nthen|Xn n ω| ≤ C * |Yn n ω|conclusionIsLittleOp Xn (fun _ => (1 : ℝ)) μProof (Lean source)
theorem IsLittleOp.of_abs_le_const_mul_one_on_event {C : ℝ} {G : ℕ → Set Ω} (hC : 0 < C) (hY : IsLittleOp Yn (fun _ => (1 : ℝ)) μ) (hG : Tendsto (fun n => μ ((G n)ᶜ)) atTop (𝓝 0)) (hbound : ∀ n ω, ω ∈ G n → |Xn n ω| ≤ C * |Yn n ω|) : IsLittleOp Xn (fun _ => (1 : ℝ)) μ := by intro ε hε have hYt := hY (ε / C) (div_pos hε hC) have hsub : ∀ n, {ω | ε * (1 : ℝ) ≤ ‖Xn n ω‖} ⊆ {ω | (ε / C) * (1 : ℝ) ≤ ‖Yn n ω‖} ∪ (G n)ᶜ := by intro n ω hω by_cases hg : ω ∈ G n · left have hx : ε ≤ |Xn n ω| := by simpa [Real.norm_eq_abs] using hω have hCy : ε ≤ C * |Yn n ω| := hx.trans (hbound n ω hg) have hy : ε / C ≤ |Yn n ω| := by rw [div_le_iff₀ hC] simpa [mul_comm] using hCy simpa [Real.norm_eq_abs] using hy · exact Or.inr hg have hsum : Tendsto (fun n => μ {ω | (ε / C) * (1 : ℝ) ≤ ‖Yn n ω‖} + μ ((G n)ᶜ)) atTop (𝓝 0) := by simpa using hYt.add hG refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hsum (fun n => bot_le) (fun n => ?_) calc μ {ω | ε * (1 : ℝ) ≤ ‖Xn n ω‖} ≤ μ ({ω | (ε / C) * (1 : ℝ) ≤ ‖Yn n ω‖} ∪ (G n)ᶜ) := measure_mono (hsub n) _ ≤ _ := measure_union_le _ _ -
mul_isBigOptheorem — If the two rates are eventually positive, then a stochastic little-o factor times a stochastically bounded factor is stochastic little-o at the product rate.hypothesesΩ :sharedType u_1ℕ → Ω → ℝℕ → Ω → ℝrn :sharedℕ → ℝsn :sharedℕ → ℝhrn :∀ᶠ n in atTop, 0 < rn nhsn :∀ᶠ n in atTop, 0 < sn nhX :IsLittleOp Xn rn μhY :IsBigOp Yn sn μconclusionIsLittleOp (fun n ω => Xn n ω * Yn n ω) (fun n => rn n * sn n) μProof (Lean source)
theorem IsLittleOp.mul_isBigOp (hrn : ∀ᶠ n in atTop, 0 < rn n) (hsn : ∀ᶠ n in atTop, 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 exact Modes.IsLittleOpF.mul_boundedInProbability hX hY hrn hsn -
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 simpa [mul_comm] using Modes.IsLittleOpF.mul_boundedInProbability hY hX (Eventually.of_forall fun _ => zero_lt_one) (Eventually.of_forall fun _ => zero_lt_one)
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 Modes.TendstoInProbability.comp_continuousAt,
Modes.TendstoInProbability.inv, Modes.TendstoInProbability.sub_const, Modes.TendstoInProbability.sub,
Modes.TendstoInProbability.isLittleOp_one, and Modes.TendstoInProbability.isBigOp_one. The file
also provides finite-dimensional continuous mapping principles
Modes.TendstoInProbability.pi_comp_continuousAt and
Modes.TendstoInProbability.matrix_comp_continuousAt, which lift entrywise convergence in
probability to continuous functionals of vectors and square matrices.
theorem comp_continuousAt reviewed
⚑ flagged
Causalean.Stat.Modes.TendstoInProbability
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 Modes.TendstoInProbability.inv (the case g = fun x => 1/x at a nonzero c).
Formal statement
hypotheses
Ω :
c :
ℝ
μ :
Measure Ω
g :
ℝ → ℝ
hg :
ContinuousAt g c
h :
Modes.TendstoInProbability (fun _ : ℕ => μ) Yn atTop (fun _ _ => c)
conclusion
Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => g (Yn n ω)) atTop (fun _ _ => g c)
Proof (Lean source)
theorem Modes.TendstoInProbability.comp_continuousAt
{Ω : Type*} [MeasurableSpace Ω] {Yn : ℕ → Ω → ℝ} {c : ℝ} {μ : Measure Ω}
{g : ℝ → ℝ} (hg : ContinuousAt g c)
(h : Modes.TendstoInProbability (fun _ : ℕ => μ) Yn atTop (fun _ _ => c)) :
Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => g (Yn n ω)) atTop (fun _ _ => g c) := by
simp only [causal_defs_simps] 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₀.hypothesesΩ :Y₀ :ℝμ :Measure Ωh :Modes.TendstoInProbability (fun _ : ℕ => μ) Yn atTop (fun _ _ => Y₀)hY₀ :Y₀ ≠ 0conclusionModes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => 1 / Yn n ω) atTop (fun _ _ => 1 / Y₀)Proof (Lean source)
theorem Modes.TendstoInProbability.inv {Ω : Type*} [MeasurableSpace Ω] {Yn : ℕ → Ω → ℝ} {Y₀ : ℝ} {μ : Measure Ω} (h : Modes.TendstoInProbability (fun _ : ℕ => μ) Yn atTop (fun _ _ => Y₀)) (hY₀ : Y₀ ≠ 0) : Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => 1 / Yn n ω) atTop (fun _ _ => 1 / Y₀) := by simp only [causal_defs_simps] 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.hypothesesconclusionModes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => Yn n ω - Y₀) atTop (fun _ _ => 0)Proof (Lean source)
theorem Modes.TendstoInProbability.sub_const {Ω : Type*} [MeasurableSpace Ω] {Yn : ℕ → Ω → ℝ} {Y₀ : ℝ} {μ : Measure Ω} (h : Modes.TendstoInProbability (fun _ : ℕ => μ) Yn atTop (fun _ _ => Y₀)) : Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => Yn n ω - Y₀) atTop (fun _ _ => 0) := by simp only [causal_defs_simps] 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 :Modes.TendstoInProbability (fun _ : ℕ => μ) Xn atTop (fun _ _ => a)hY :Modes.TendstoInProbability (fun _ : ℕ => μ) Yn atTop (fun _ _ => b)conclusionModes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => Xn n ω - Yn n ω) atTop (fun _ _ => a - b)Proof (Lean source)
theorem Modes.TendstoInProbability.sub {Ω : Type*} [MeasurableSpace Ω] {Xn Yn : ℕ → Ω → ℝ} {a b : ℝ} {μ : Measure Ω} (hX : Modes.TendstoInProbability (fun _ : ℕ => μ) Xn atTop (fun _ _ => a)) (hY : Modes.TendstoInProbability (fun _ : ℕ => μ) Yn atTop (fun _ _ => b)) : Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => Xn n ω - Yn n ω) atTop (fun _ _ => a - b) := by simp only [causal_defs_simps] 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.hypothesesΩ :h :Modes.TendstoInProbability (fun _ : ℕ => μ) Yn atTop (fun _ _ => 0)conclusionIsLittleOp Yn (fun _ => (1 : ℝ)) μProof (Lean source)
theorem Modes.TendstoInProbability.isLittleOp_one {Ω : Type*} [MeasurableSpace Ω] {Yn : ℕ → Ω → ℝ} {μ : Measure Ω} (h : Modes.TendstoInProbability (fun _ : ℕ => μ) Yn atTop (fun _ _ => 0)) : IsLittleOp Yn (fun _ => (1 : ℝ)) μ := by exact (Modes.tendstoInProbability_zero_iff_isLittleOpF_one (fun _ => μ) Yn atTop).mp h -
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 Modes.TendstoInProbability.isBigOp_one {Ω : Type*} [MeasurableSpace Ω] {Xn : ℕ → Ω → ℝ} {c : ℝ} {μ : Measure Ω} (h : Modes.TendstoInProbability (fun _ : ℕ => μ) Xn atTop (fun _ _ => c)) : IsBigOp Xn (fun _ => (1 : ℝ)) μ := by intro δ hδ refine ⟨|c| + 1, by positivity, ?_⟩ simp only [causal_defs_simps] at h rw [tendstoInMeasure_iff_norm] at h have ht := h 1 one_pos rw [ENNReal.tendsto_nhds_zero] at ht filter_upwards [ht δ hδ] with n hn refine (measure_mono ?_).trans hn intro ω hω simp only [Set.mem_setOf_eq, mul_one, Real.norm_eq_abs] at hω ⊢ have htri := abs_sub_abs_le_abs_sub (Xn n ω) c linarith -
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).hypothesesΩ ι :hg :ContinuousAt g ch :∀ i,Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => Yn n ω i) atTop (fun _ _ => c i)conclusionModes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => g (Yn n ω)) atTop (fun _ _ => g c)Proof (Lean source)
theorem Modes.TendstoInProbability.pi_comp_continuousAt {Ω ι : Type*} [MeasurableSpace Ω] [Fintype ι] {μ : Measure Ω} {Yn : ℕ → Ω → (ι → ℝ)} {c : ι → ℝ} {g : (ι → ℝ) → ℝ} (hg : ContinuousAt g c) (h : ∀ i, Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => Yn n ω i) atTop (fun _ _ => c i)) : Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => g (Yn n ω)) atTop (fun _ _ => g c) := by classical simp only [causal_defs_simps] 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 simp only [causal_defs_simps] 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,Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => Mn n ω i j) atTop (fun _ _ => M₀ i j)conclusionModes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => g (Mn n ω)) atTop (fun _ _ => g M₀)Proof (Lean source)
theorem Modes.TendstoInProbability.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, Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => Mn n ω i j) atTop (fun _ _ => M₀ i j)) : Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => g (Mn n ω)) atTop (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 := Modes.TendstoInProbability.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 · 2 supporting This module extends the scalar convergence-in-distribution interface to metric-space-valued random variables. ★ add_isLittleOp_one★ map_continuous★ map_continuous_ae
Vector convergence in distribution
This module extends the scalar convergence-in-distribution interface to
metric-space-valued random variables. Tendsto_dist_vec_iff expresses convergence in law
through pushforward probability measures, while
Modes.TendstoInLaw.add_isLittleOp_one, Modes.TendstoInLaw.congr_ae, and
Modes.TendstoInLaw.map_continuous provide the vector Slutsky, a.e.-congruence,
and continuous-mapping rules used by multivariate CLT and delta-method
arguments.
theorem add_isLittleOp_one reviewed
⚑ flagged
Causalean.Stat.Modes.TendstoInLaw
If a sequence in a normed additive group converges in distribution, a second sequence is a.e. measurable at every sample size, and their difference is negligible in probability at rate one, then the second sequence converges in distribution to the same law.
Formal statement
hypotheses
Ω E :
Xn Yn :
ℕ → Ω → E
Q :
hX :
Modes.TendstoInLaw (fun _ : ℕ => μ) Xn atTop Q
hYn :
∀ n, AEMeasurable (Yn n) μ
hRem :
IsLittleOp (fun n ω => Yn n ω - Xn n ω) (fun _ => (1 : ℝ)) μ
conclusion
Modes.TendstoInLaw (fun _ : ℕ => μ) Yn atTop Q
Proof (Lean source)
theorem Modes.TendstoInLaw.add_isLittleOp_one
{Ω E : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
[NormedAddCommGroup E] [MeasurableSpace E] [OpensMeasurableSpace E]
{Xn Yn : ℕ → Ω → E} {Q : Measure E} [IsProbabilityMeasure Q]
(hX : Modes.TendstoInLaw (fun _ : ℕ => μ) Xn atTop Q)
(hYn : ∀ n, AEMeasurable (Yn n) μ)
(hRem : IsLittleOp (fun n ω => Yn n ω - Xn n ω) (fun _ => (1 : ℝ)) μ) :
Modes.TendstoInLaw (fun _ : ℕ => μ) Yn atTop Q := by
have hXn : ∀ n, AEMeasurable (Xn n) μ := hX.forall_aemeasurable
refine ⟨hYn, by fun_prop, ?_⟩
have hX_tendsto :
Tendsto (β := ProbabilityMeasure E)
(fun n => ⟨μ.map (Xn n), Measure.isProbabilityMeasure_map (hXn n)⟩) atTop
(𝓝 ⟨Q, ‹IsProbabilityMeasure Q›⟩) := by
simpa only [ProbabilityMeasure.coe_mk, Measure.map_id] using hX.tendsto
have hXY : TendstoInMeasure μ (fun n ω => Yn n ω - Xn n ω) atTop (0 : Ω → E) := by
rw [tendstoInMeasure_iff_norm]
intro ε hε
simpa only [Pi.zero_apply, sub_zero, mul_one] using hRem ε hε
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
simpa only [ProbabilityMeasure.coe_mk, Measure.map_id] using
(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)‖) μ := by
fun_prop
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_tendsto 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.Modes.TendstoInLaw
If random elements converge in distribution and the applied map is continuous, then the transformed laws converge weakly to the pushforward of the limiting law.
Formal statement
hypotheses
conclusion
Tendsto (β := ProbabilityMeasure F) (fun n => ⟨μ.map (fun ω => g (Xn n ω)), Measure.isProbabilityMeasure_map (hg.measurable.aemeasurable.comp_aemeasurable (hX.forall_aemeasurable n))⟩) atTop (𝓝 ⟨Q.map g, Measure.isProbabilityMeasure_map hg.measurable.aemeasurable⟩)
Proof (Lean source)
theorem Modes.TendstoInLaw.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}
(hX : Modes.TendstoInLaw (fun _ : ℕ => μ) Xn atTop Q)
(hg : Continuous g) :
Tendsto (β := ProbabilityMeasure F)
(fun n =>
⟨μ.map (fun ω => g (Xn n ω)),
Measure.isProbabilityMeasure_map
(hg.measurable.aemeasurable.comp_aemeasurable (hX.forall_aemeasurable n))⟩)
atTop
(𝓝 ⟨Q.map g, Measure.isProbabilityMeasure_map hg.measurable.aemeasurable⟩) := by
have hXn : ∀ n, AEMeasurable (Xn n) μ := hX.forall_aemeasurable
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
have hX_tendsto :
Tendsto (β := ProbabilityMeasure E)
(fun n => ⟨μ.map (Xn n), Measure.isProbabilityMeasure_map (hXn n)⟩) atTop
(𝓝 ⟨Q, ‹IsProbabilityMeasure Q›⟩) := by
simpa only [ProbabilityMeasure.coe_mk, Measure.map_id] using hX.tendsto
have hpm := MeasureTheory.ProbabilityMeasure.tendsto_map_of_tendsto_of_continuous
(fun n => ⟨μ.map (Xn n), Measure.isProbabilityMeasure_map (hXn n)⟩)
⟨Q, ‹IsProbabilityMeasure Q›⟩ hX_tendsto 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
theorem map_continuous_ae reviewed
⚑ flagged
Causalean.Stat.Modes.TendstoInLaw
If random elements converge in distribution, the applied map is measurable, and it is continuous at almost every point under the limiting law, then the transformed laws converge weakly to the pushforward of the limiting law.
Formal statement
hypotheses
Ω E F :
Xn :
ℕ → Ω → E
Q :
g :
E → F
hX :
Modes.TendstoInLaw (fun _ : ℕ => μ) Xn atTop Q
hgmeas :
hg :
∀ᵐ x ∂Q, ContinuousAt g x
conclusion
Tendsto (β := ProbabilityMeasure F) (fun n => ⟨μ.map (fun ω => g (Xn n ω)), Measure.isProbabilityMeasure_map (hgmeas.aemeasurable.comp_aemeasurable (hX.forall_aemeasurable n))⟩) atTop (𝓝 ⟨Q.map g, Measure.isProbabilityMeasure_map hgmeas.aemeasurable⟩)
Proof (Lean source)
theorem Modes.TendstoInLaw.map_continuous_ae
{Ω 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}
(hX : Modes.TendstoInLaw (fun _ : ℕ => μ) Xn atTop Q)
(hgmeas : Measurable g) (hg : ∀ᵐ x ∂Q, ContinuousAt g x) :
Tendsto (β := ProbabilityMeasure F)
(fun n =>
⟨μ.map (fun ω => g (Xn n ω)),
Measure.isProbabilityMeasure_map
(hgmeas.aemeasurable.comp_aemeasurable (hX.forall_aemeasurable n))⟩)
atTop
(𝓝 ⟨Q.map g, Measure.isProbabilityMeasure_map hgmeas.aemeasurable⟩) := by
have hXn : ∀ n, AEMeasurable (Xn n) μ := hX.forall_aemeasurable
have hX_tendsto :
Tendsto (β := ProbabilityMeasure E)
(fun n => ⟨μ.map (Xn n), Measure.isProbabilityMeasure_map (hXn n)⟩) atTop
(𝓝 ⟨Q, ‹IsProbabilityMeasure Q›⟩) := by
simpa only [ProbabilityMeasure.coe_mk, Measure.map_id] using hX.tendsto
apply MeasureTheory.tendsto_of_forall_isClosed_limsup_le'
intro C hC
let A : Set E := g ⁻¹' C
have hAmeas : MeasurableSet A := hC.measurableSet.preimage hgmeas
have hnull : Q (closure A \ A) = 0 := by
apply measure_mono_null _ (MeasureTheory.ae_iff.mp hg)
intro x hx hcont
apply hx.2
change g x ∈ C
exact by
have hmem : g x ∈ closure C :=
hcont.continuousWithinAt.mem_closure hx.1 (Set.mapsTo_preimage g C)
simpa [hC.closure_eq] using hmem
have hQA : Q (closure A) = Q A :=
(measure_eq_measure_of_null_sdiff subset_closure hnull).symm
have hclosed := ProbabilityMeasure.limsup_measure_closed_le_of_tendsto
(F := closure A) hX_tendsto isClosed_closure
change limsup (fun n => (μ.map fun ω => g (Xn n ω)) C) atTop ≤ (Q.map g) C
calc
limsup
(fun n => (μ.map fun ω => g (Xn n ω)) C) atTop ≤
limsup (fun n => μ.map (Xn n) (closure A)) atTop := by
apply Filter.limsup_le_limsup
· filter_upwards with n
change (μ.map (g ∘ Xn n)) C ≤ (μ.map (Xn n)) (closure A)
rw [Measure.map_apply_of_aemeasurable
(hgmeas.aemeasurable.comp_aemeasurable (hXn n)) hC.measurableSet]
rw [Measure.map_apply_of_aemeasurable (hXn n) isClosed_closure.measurableSet]
apply measure_mono
intro ω hω
exact subset_closure hω
· exact isCoboundedUnder_le_of_le atTop fun _ => bot_le
· apply isBoundedUnder_of
refine ⟨1, fun n : ℕ => ?_⟩
calc
(μ.map (Xn n)) (closure A) ≤ (μ.map (Xn n)) univ :=
measure_mono (Set.subset_univ _)
_ = 1 := by
rw [Measure.map_apply_of_aemeasurable (hXn n) MeasurableSet.univ]
simp
_ ≤ Q (closure A) := by simpa [A] using hclosed
_ = Q A := hQA
_ = (Q.map g) C := by
rw [Measure.map_apply hgmeas hC.measurableSet]
2 supporting declarations (lemmas, instances)
-
Tendsto_dist_vec_ifflemma — For measurable row variables, a target probability law, and a fixed probability measure, vector convergence in distribution is equivalent to weak convergence of the pushforward probability measures.hypothesesconclusionModes.TendstoInLaw (fun _ : ℕ => μ) Xn atTop Q↔ Tendsto (β := ProbabilityMeasure E) (fun n => ⟨μ.map (Xn n), Measure.isProbabilityMeasure_map (hXn n)⟩) atTop (𝓝 ⟨Q, ‹IsProbabilityMeasure Q›⟩)Proof (Lean source)
lemma Tendsto_dist_vec_iff {Ω E : Type*} [MeasurableSpace Ω] [PseudoMetricSpace E] [MeasurableSpace E] [OpensMeasurableSpace E] (Xn : ℕ → Ω → E) (Q : Measure E) (μ : Measure Ω) [IsProbabilityMeasure μ] [IsProbabilityMeasure Q] (hXn : ∀ n, AEMeasurable (Xn n) μ) : Modes.TendstoInLaw (fun _ : ℕ => μ) Xn atTop Q ↔ Tendsto (β := ProbabilityMeasure E) (fun n => ⟨μ.map (Xn n), Measure.isProbabilityMeasure_map (hXn n)⟩) atTop (𝓝 ⟨Q, ‹IsProbabilityMeasure Q›⟩) := by constructor · intro h simpa only [ProbabilityMeasure.coe_mk, Measure.map_id] using h.tendsto · intro h refine ⟨hXn, by fun_prop, ?_⟩ simpa only [ProbabilityMeasure.coe_mk, Measure.map_id] using h -
congr_aetheorem — If a sequence in a pseudo-metric space converges in distribution, a second sequence is a.e. measurable at every sample size, and the sequences eventually agree almost everywhere, then the second sequence converges in distribution to the same law.hypothesesΩ E :Xn Yn :ℕ → Ω → EQ :hX :Modes.TendstoInLaw (fun _ : ℕ => μ) Xn atTop QhYn :∀ n, AEMeasurable (Yn n) μhXY :∀ᶠ n in atTop, Xn n =ᵐ[μ] Yn nconclusionModes.TendstoInLaw (fun _ : ℕ => μ) Yn atTop QProof (Lean source)
theorem Modes.TendstoInLaw.congr_ae {Ω E : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ] [PseudoMetricSpace E] [MeasurableSpace E] [OpensMeasurableSpace E] {Xn Yn : ℕ → Ω → E} {Q : Measure E} [IsProbabilityMeasure Q] (hX : Modes.TendstoInLaw (fun _ : ℕ => μ) Xn atTop Q) (hYn : ∀ n, AEMeasurable (Yn n) μ) (hXY : ∀ᶠ n in atTop, Xn n =ᵐ[μ] Yn n) : Modes.TendstoInLaw (fun _ : ℕ => μ) Yn atTop Q := by refine ⟨hYn, by fun_prop, hX.tendsto.congr' ?_⟩ filter_upwards [hXY] with n hn apply Subtype.ext exact Measure.map_congr hn
ExtendedContinuousMapping 1 core · 0 supporting This file proves a finite-dimensional extended continuous mapping principle. ★ map_varying_of_uniform_on_bounded
Extended continuous mapping for varying maps
This file proves a finite-dimensional extended continuous mapping principle. If random elements converge weakly and a sequence of maps converges uniformly to a continuous map on every norm-bounded set, applying the varying maps preserves weak convergence to the pushforward under the limiting map.
The result isolates the probabilistic tightness argument used by the Hadamard-directional functional delta method.
theorem map_varying_of_uniform_on_bounded reviewed
⚑ flagged
Causalean.Stat.Modes.TendstoInLaw
If random elements converge in distribution, the limiting map is continuous, the transformed random elements are a.e. measurable, and the varying maps approach the limiting map uniformly on every norm-bounded set, then the transformed laws converge weakly to the pushforward under the limiting map.
Formal statement
hypotheses
Ω E F :
Xn :
ℕ → Ω → E
Q :
fn :
ℕ → E → F
g :
E → F
hX :
Modes.TendstoInLaw (fun _ : ℕ => μ) Xn atTop Q
hg :
hYn :
∀ n, AEMeasurable (fun omega => fn n (Xn n omega)) μ
hUniform :
∀ (M : ℝ) (epsilon : ℝ),
0 < epsilon → ∀ᶠ n in atTop, ∀ x : E, ‖x‖ ≤ M → ‖fn n x - g x‖ < epsilon
conclusion
Tendsto (β := ProbabilityMeasure F) (fun n => ⟨μ.map (fun omega => fn n (Xn n omega)), Measure.isProbabilityMeasure_map (hYn n)⟩) atTop (𝓝 ⟨Q.map g, Measure.isProbabilityMeasure_map hg.measurable.aemeasurable⟩)
Proof (Lean source)
theorem Modes.TendstoInLaw.map_varying_of_uniform_on_bounded
{Ω E F : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
[NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E]
[NormedAddCommGroup F] [MeasurableSpace F] [BorelSpace F]
{Xn : ℕ → Ω → E} {Q : Measure E} [IsProbabilityMeasure Q]
{fn : ℕ → E → F} {g : E → F}
(hX : Modes.TendstoInLaw (fun _ : ℕ => μ) Xn atTop Q)
(hg : Continuous g)
(hYn : ∀ n, AEMeasurable (fun omega => fn n (Xn n omega)) μ)
(hUniform : ∀ (M : ℝ) (epsilon : ℝ), 0 < epsilon →
∀ᶠ n in atTop, ∀ x : E, ‖x‖ ≤ M → ‖fn n x - g x‖ < epsilon) :
Tendsto (β := ProbabilityMeasure F)
(fun n =>
⟨μ.map (fun omega => fn n (Xn n omega)),
Measure.isProbabilityMeasure_map (hYn n)⟩)
atTop
(𝓝 ⟨Q.map g,
Measure.isProbabilityMeasure_map hg.measurable.aemeasurable⟩) := by
have hXn : ∀ n, AEMeasurable (Xn n) μ := hX.forall_aemeasurable
let Zn : ℕ → Ω → F := fun n omega => g (Xn n omega)
let Yn : ℕ → Ω → F := fun n omega => fn n (Xn n omega)
let _ : IsProbabilityMeasure (Q.map g) :=
Measure.isProbabilityMeasure_map hg.measurable.aemeasurable
let _ : IsProbabilityMeasure (Q.map fun x : E => ‖x‖) :=
Measure.isProbabilityMeasure_map continuous_norm.measurable.aemeasurable
have hZn : ∀ n, AEMeasurable (Zn n) μ := fun n =>
hg.measurable.comp_aemeasurable (hXn n)
have hNormXn : ∀ n, AEMeasurable (fun omega => ‖Xn n omega‖) μ := fun n =>
continuous_norm.measurable.comp_aemeasurable (hXn n)
have hNormDist : Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n omega => ‖Xn n omega‖) atTop
(Q.map fun x : E => ‖x‖) := by
have hvec := Modes.TendstoInLaw.map_continuous (Q := Q)
(g := fun x : E => ‖x‖)
hX
continuous_norm
exact (Tendsto_dist_iff _ _ _ hNormXn).2 hvec
have hTight : IsBigOp (fun n omega => ‖Xn n omega‖) (fun _ => (1 : ℝ)) μ :=
Modes.TendstoInLaw.tightness hNormDist
have hRem : IsLittleOp (fun n omega => ‖Yn n omega - Zn n omega‖)
(fun _ => (1 : ℝ)) μ := by
intro epsilon hepsilon
rw [ENNReal.tendsto_nhds_zero]
intro delta hdelta
rcases hTight delta hdelta with ⟨M, hMpos, hAevent⟩
let A : ℕ → Set Ω := fun n => {omega | M ≤ ‖Xn n omega‖}
have hUevent := hUniform M epsilon hepsilon
filter_upwards [hAevent, hUevent] with n hAn hUn
have hsubset :
{omega | epsilon * (fun _ => (1 : ℝ)) n ≤ |‖Yn n omega - Zn n omega‖|}
⊆ A n := by
intro omega homega
simp only [mul_one, abs_of_nonneg (norm_nonneg _)] at homega
by_contra hnot
have hbound : ‖Xn n omega‖ ≤ M := (lt_of_not_ge hnot).le
exact (not_lt_of_ge homega) (hUn (Xn n omega) hbound)
have hAn' : μ (A n) ≤ delta := by simpa [A, abs_of_nonneg] using hAn
exact (measure_mono hsubset).trans hAn'
have hZdist : Modes.TendstoInLaw (fun _ : ℕ => μ) Zn atTop (Q.map g) := by
exact (Tendsto_dist_vec_iff _ _ _ hZn).2
(Modes.TendstoInLaw.map_continuous hX hg)
exact (Tendsto_dist_vec_iff _ _ _ hYn).1
(Modes.TendstoInLaw.add_isLittleOp_one hZdist hYn (by
intro ε hε
simpa only [norm_norm] using hRem ε hε))
ProbabilityTransfer 1 core · 0 supporting This module transfers stochastic asymptotic bounds between random sequences that agree on events whose probabilities tend to one. ★ isLittleOp_of_isLittleOp_on_highProbEvent
High-Probability Transfer Rules
This module transfers stochastic asymptotic bounds between random sequences that agree on events whose probabilities tend to one.
theorem isLittleOp_of_isLittleOp_on_highProbEvent reviewed
⚑ flagged
Causalean.Stat
Given events, failure-probability bounds that vanish, complement measures controlled by those bounds, two random sequences that agree on those events, and a stochastic little-o bound for the second sequence, the first sequence obeys the same stochastic little-o bound.
Formal statement
hypotheses
rn :
ℕ → ℝ
G :
ℕ → Set Ω
Δ :
ℕ → ℝ≥0∞
hfail :
∀ n, μ (G n)ᶜ ≤ Δ n
h_eq :
∀ n ω
if
ω ∈ G n
then
Xn n ω = Yn n ω
hY :
IsLittleOp Yn rn μ
conclusion
IsLittleOp Xn rn μ
Proof (Lean source)
theorem isLittleOp_of_isLittleOp_on_highProbEvent
{Xn Yn : ℕ → Ω → ℝ} {rn : ℕ → ℝ}
(G : ℕ → Set Ω) (Δ : ℕ → ℝ≥0∞)
(hΔ : Tendsto Δ atTop (𝓝 0))
(hfail : ∀ n, μ (G n)ᶜ ≤ Δ n)
(h_eq : ∀ n ω, ω ∈ G n → Xn n ω = Yn n ω)
(hY : IsLittleOp Yn rn μ) :
IsLittleOp Xn rn μ := by
apply IsLittleOp.of_eq_on_asymptotic ?_ hY
rw [ENNReal.tendsto_nhds_zero] at hΔ ⊢
intro ε hε
exact (hΔ ε hε).mono fun n hn => by
have hsubset : {ω | Xn n ω ≠ Yn n ω} ⊆ (G n)ᶜ := by
intro ω hne hmem
exact hne (h_eq n ω hmem)
exact (measure_mono hsubset).trans ((hfail n).trans hn)
QuadraticForm 1 core · 3 supporting This module provides two contact lemmas for weak-convergence proofs. ★ quadraticForm_of_operator_tendstoInProb
Continuous mapping for random quadratic forms
This module provides two contact lemmas for weak-convergence proofs. The first allows the pushforward target produced by continuous mapping to be replaced by an identified measure. The second is a quadratic-form Slutsky theorem: an operator converging in probability in operator norm may replace its limit inside a quadratic form evaluated at a tight random vector.
theorem quadraticForm_of_operator_tendstoInProb reviewed
⚑ flagged
Causalean.Stat.Modes.TendstoInLaw
If a vector sequence converges in distribution, a random continuous-linear operator family converges in probability in operator norm to a fixed operator, and the random quadratic forms are a.e. measurable, then their laws converge weakly to the pushforward of the vector limit through the fixed quadratic form.
Formal statement
hypotheses
Ω E :
Xn :
ℕ → Ω → E
Q :
hX :
Modes.TendstoInLaw (fun _ : ℕ => μ) Xn atTop Q
An :
ℕ → Ω → (E →L[ℝ] E)
A :
E →L[ℝ] E
hA :
Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ‖An n ω - A‖) atTop (fun _ _ => 0)
hQuadraticMeas :
∀ n, AEMeasurable (fun ω => ⟪An n ω (Xn n ω), Xn n ω⟫) μ
conclusion
Tendsto (β := ProbabilityMeasure ℝ) (fun n => ⟨μ.map (fun ω => ⟪An n ω (Xn n ω), Xn n ω⟫), Measure.isProbabilityMeasure_map (hQuadraticMeas n)⟩) atTop (𝓝 ⟨Q.map (fun x => ⟪A x, x⟫), Measure.isProbabilityMeasure_map ((A.continuous.inner continuous_id).measurable.aemeasurable)⟩)
Proof (Lean source)
theorem Modes.TendstoInLaw.quadraticForm_of_operator_tendstoInProb
{Ω E : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
[NormedAddCommGroup E] [InnerProductSpace ℝ E]
[MeasurableSpace E] [BorelSpace E]
{Xn : ℕ → Ω → E} {Q : Measure E} [IsProbabilityMeasure Q]
(hX : Modes.TendstoInLaw (fun _ : ℕ => μ) Xn atTop Q)
(An : ℕ → Ω → (E →L[ℝ] E)) (A : E →L[ℝ] E)
(hA : Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ‖An n ω - A‖) atTop
(fun _ _ => 0))
(hQuadraticMeas : ∀ n,
AEMeasurable (fun ω => ⟪An n ω (Xn n ω), Xn n ω⟫) μ) :
Tendsto (β := ProbabilityMeasure ℝ)
(fun n =>
⟨μ.map (fun ω => ⟪An n ω (Xn n ω), Xn n ω⟫),
Measure.isProbabilityMeasure_map (hQuadraticMeas n)⟩)
atTop
(𝓝 ⟨Q.map (fun x => ⟪A x, x⟫),
Measure.isProbabilityMeasure_map
((A.continuous.inner continuous_id).measurable.aemeasurable)⟩) := by
have hXn : ∀ n, AEMeasurable (Xn n) μ := hX.forall_aemeasurable
let q : E → ℝ := fun x => ⟪A x, x⟫
have hq : Continuous q := A.continuous.inner continuous_id
have hqXn : ∀ n, AEMeasurable (fun ω => q (Xn n ω)) μ := fun n =>
hq.measurable.aemeasurable.comp_aemeasurable (hXn n)
letI : IsProbabilityMeasure (Q.map q) :=
Measure.isProbabilityMeasure_map hq.measurable.aemeasurable
have hfixed : Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n ω => q (Xn n ω)) atTop (Q.map q) := by
exact (Tendsto_dist_iff _ _ _ hqXn).2 (Modes.TendstoInLaw.map_continuous hX hq)
have hnormMeas : ∀ n, AEMeasurable (fun ω => ‖Xn n ω‖) μ := fun n =>
continuous_norm.measurable.aemeasurable.comp_aemeasurable (hXn n)
letI : IsProbabilityMeasure (Q.map norm) :=
Measure.isProbabilityMeasure_map continuous_norm.measurable.aemeasurable
have hnormDist :
Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n ω => ‖Xn n ω‖) atTop (Q.map norm) := by
exact (Tendsto_dist_iff _ _ _ hnormMeas).2
(Modes.TendstoInLaw.map_continuous hX continuous_norm)
have hnormBig : IsBigOp (fun n ω => ‖Xn n ω‖) (fun _ => (1 : ℝ)) μ := by
exact Modes.TendstoInLaw.tightness hnormDist
have hnormSqBig : IsBigOp (fun n ω => ‖Xn n ω‖ * ‖Xn n ω‖)
(fun _ => (1 : ℝ)) μ := by
simpa only [one_mul] using Modes.BoundedInProbability.mul hnormBig hnormBig
(Eventually.of_forall fun _ => zero_lt_one)
(Eventually.of_forall fun _ => zero_lt_one)
have hdeltaLittle : IsLittleOp (fun n ω => ‖An n ω - A‖)
(fun _ => (1 : ℝ)) μ := Modes.TendstoInProbability.isLittleOp_one hA
have hproductLittle : IsLittleOp
(fun n ω => ‖An n ω - A‖ * (‖Xn n ω‖ * ‖Xn n ω‖))
(fun _ => (1 : ℝ)) μ := by
simpa using hdeltaLittle.mul_isBigOp
(Eventually.of_forall fun _ => zero_lt_one)
(Eventually.of_forall fun _ => zero_lt_one) hnormSqBig
have hrem : IsLittleOp
(fun n ω => ⟪An n ω (Xn n ω), Xn n ω⟫ - q (Xn n ω))
(fun _ => (1 : ℝ)) μ := by
refine IsLittleOp.of_abs_le_const_mul_one (C := 1) zero_lt_one hproductLittle ?_
intro n ω
rw [one_mul, abs_of_nonneg (mul_nonneg (norm_nonneg _)
(mul_nonneg (norm_nonneg _) (norm_nonneg _)))]
calc
|⟪An n ω (Xn n ω), Xn n ω⟫ - q (Xn n ω)|
= |⟪(An n ω - A) (Xn n ω), Xn n ω⟫| := by
simp only [q, sub_apply, inner_sub_left]
_ ≤ ‖(An n ω - A) (Xn n ω)‖ * ‖Xn n ω‖ :=
abs_real_inner_le_norm _ _
_ ≤ ‖An n ω - A‖ * (‖Xn n ω‖ * ‖Xn n ω‖) := by
calc
‖(An n ω - A) (Xn n ω)‖ * ‖Xn n ω‖
≤ (‖An n ω - A‖ * ‖Xn n ω‖) * ‖Xn n ω‖ := by
gcongr
exact (An n ω - A).le_opNorm (Xn n ω)
_ = ‖An n ω - A‖ * (‖Xn n ω‖ * ‖Xn n ω‖) := by ring
exact (Tendsto_dist_iff _ _ _ hQuadraticMeas).1
(Modes.TendstoInLaw.add_isLittleOp_one hfixed hQuadraticMeas hrem)
3 supporting declarations (lemmas, instances)
-
isBigOp_onetheorem — Every o_P(1) sequence is bounded in probability.Proof (Lean source)
theorem IsLittleOp.isBigOp_one {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} {A : ℕ → Ω → ℝ} (hA : IsLittleOp A (fun _ => (1 : ℝ)) μ) : IsBigOp A (fun _ => (1 : ℝ)) μ := by exact Modes.IsLittleOpF.boundedInProbability hA -
isBigOp_of_absorptiontheorem — Stochastic absorption. Suppose a nonnegative random coefficient is o_P(1), a nonnegative forcing sequence is O_P(1), and a nonnegative target sequence is eventually almost surely bounded by the forcing term plus that small coefficient times the target itself, with the stated nonnegativity conditions. Then the target sequence is O_P(1).hypothesesΩ :hA :IsLittleOp A (fun _ => (1 : ℝ)) μhB :IsBigOp B (fun _ => (1 : ℝ)) μhA_nonneg :∀ n ω, 0 ≤ A n ωhB_nonneg :∀ n ω, 0 ≤ B n ωhY_nonneg :∀ n ω, 0 ≤ Y n ωhbound :∀ᶠ n in atTop, ∀ᵐ ω ∂μ, Y n ω ≤ B n ω + A n ω * Y n ωconclusionIsBigOp Y (fun _ => (1 : ℝ)) μProof (Lean source)
theorem IsLittleOp.isBigOp_of_absorption {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} {A B Y : ℕ → Ω → ℝ} (hA : IsLittleOp A (fun _ => (1 : ℝ)) μ) (hB : IsBigOp B (fun _ => (1 : ℝ)) μ) (hA_nonneg : ∀ n ω, 0 ≤ A n ω) (hB_nonneg : ∀ n ω, 0 ≤ B n ω) (hY_nonneg : ∀ n ω, 0 ≤ Y n ω) (hbound : ∀ᶠ n in atTop, ∀ᵐ ω ∂μ, Y n ω ≤ B n ω + A n ω * Y n ω) : IsBigOp Y (fun _ => (1 : ℝ)) μ := by intro δ hδ have hhalf : 0 < δ / 2 := ENNReal.div_pos hδ.ne' (by norm_num) rcases hB (δ / 2) hhalf with ⟨M, hM, hBevent⟩ refine ⟨2 * M, mul_pos (by norm_num) hM, ?_⟩ let Aevent : ℕ → Set Ω := fun n => {ω | (1 / 2 : ℝ) ≤ |A n ω|} let Bevent : ℕ → Set Ω := fun n => {ω | M ≤ |B n ω|} let Cevent : ℕ → Set Ω := fun n => {ω | 2 * M ≤ |Y n ω|} have hAt : Tendsto (fun n => μ (Aevent n)) atTop (𝓝 0) := by simpa [Aevent] using hA (1 / 2) (by norm_num) have hAevent := (ENNReal.tendsto_nhds_zero.mp hAt) (δ / 2) hhalf filter_upwards [hAevent, hBevent, hbound] with n hAn hBn hboundn have hsubset : ∀ᵐ ω ∂μ, ω ∈ Cevent n → ω ∈ Aevent n ∪ Bevent n := by filter_upwards [hboundn] with ω hboundω intro hω by_contra hnot have hnotA : ¬ (1 / 2 : ℝ) ≤ |A n ω| := by intro h exact hnot (inl h) have hnotB : ¬ M ≤ |B n ω| := by intro h exact hnot (inr h) have hAlt : A n ω < 1 / 2 := by rw [← abs_of_nonneg (hA_nonneg n ω)] exact lt_of_not_ge hnotA have hBlt : B n ω < M := by rw [← abs_of_nonneg (hB_nonneg n ω)] exact lt_of_not_ge hnotB have hYlt : Y n ω < 2 * M := by nlinarith [hY_nonneg n ω] have hYge : 2 * M ≤ Y n ω := by change 2 * M ≤ |Y n ω| at hω rwa [abs_of_nonneg (hY_nonneg n ω)] at hω exact (not_lt_of_ge hYge) hYlt have hBn' : μ (Bevent n) ≤ δ / 2 := by simpa [Bevent] using hBn calc μ {ω | (2 * M) * (fun _ => (1 : ℝ)) n ≤ |Y n ω|} = μ (Cevent n) := by simp [Cevent] _ ≤ μ (Aevent n ∪ Bevent n) := measure_mono_ae hsubset _ ≤ μ (Aevent n) + μ (Bevent n) := measure_union_le _ _ _ ≤ δ / 2 + δ / 2 := add_le_add hAn hBn' _ = δ := ENNReal.add_halves δ -
map_continuous_of_map_eqtheorem — If random elements converge in distribution, the applied map is continuous, and the pushforward of the limiting law is the named target law, then the transformed laws converge weakly to that target law.hypothesesΩ E F :Xn :ℕ → Ω → EQ :R :g :E → FhX :Modes.TendstoInLaw (fun _ : ℕ => μ) Xn atTop Qhg :hmap :Q.map g = RconclusionTendsto (β := ProbabilityMeasure F) (fun n => ⟨μ.map (fun ω => g (Xn n ω)), Measure.isProbabilityMeasure_map (hg.measurable.aemeasurable.comp_aemeasurable (hX.forall_aemeasurable n))⟩) atTop (𝓝 ⟨R, ‹IsProbabilityMeasure R›⟩)Proof (Lean source)
theorem Modes.TendstoInLaw.map_continuous_of_map_eq {Ω 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] {R : Measure F} [IsProbabilityMeasure R] {g : E → F} (hX : Modes.TendstoInLaw (fun _ : ℕ => μ) Xn atTop Q) (hg : Continuous g) (hmap : Q.map g = R) : Tendsto (β := ProbabilityMeasure F) (fun n => ⟨μ.map (fun ω => g (Xn n ω)), Measure.isProbabilityMeasure_map (hg.measurable.aemeasurable.comp_aemeasurable (hX.forall_aemeasurable n))⟩) atTop (𝓝 ⟨R, ‹IsProbabilityMeasure R›⟩) := by simpa [hmap] using Modes.TendstoInLaw.map_continuous hX hg
Slutsky 3 core · 0 supporting This module supplies the two scalar forms of Slutsky's theorem used in asymptotic statistics. ★ add_tendstoInProbability_const★ mul_tendstoInProbability_const★ smul_tendstoInProbability_const
Random-multiplier Slutsky lemmas
This module supplies the two scalar forms of Slutsky's theorem used in
asymptotic statistics. A random sequence converging in probability to a
constant may be added to, or multiplied by, a sequence converging in
distribution. The proofs reduce the random part to an o_p(1) perturbation
and use the project's tightness and Slutsky-absorption lemmas.
theorem add_tendstoInProbability_const reviewed
⚑ flagged
Causalean.Stat.Modes.TendstoInLaw
If a real sequence converges in distribution, a second sequence is a.e. measurable, and the second sequence converges in probability to a constant, then their sum converges in distribution to the limiting law shifted by that constant.
Formal statement
hypotheses
Ω :
Xn Yn :
ℕ → Ω → ℝ
Q :
c :
ℝ
hX :
Modes.TendstoInLaw (fun _ : ℕ => μ) Xn atTop Q
hYn :
∀ n, AEMeasurable (Yn n) μ
hY :
Modes.TendstoInProbability (fun _ : ℕ => μ) Yn atTop (fun _ _ => c)
conclusion
@Modes.TendstoInLaw ℕ (fun _ => Ω) _ ℝ _ _ _ (fun _ => μ) _ (fun n ω => Xn n ω + Yn n ω) atTop (Q.map fun x => x + c) (Measure.isProbabilityMeasure_map (measurable_id.add measurable_const).aemeasurable)
Proof (Lean source)
theorem Modes.TendstoInLaw.add_tendstoInProbability_const
{Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
{Xn Yn : ℕ → Ω → ℝ} {Q : Measure ℝ} [IsProbabilityMeasure Q] {c : ℝ}
(hX : Modes.TendstoInLaw (fun _ : ℕ => μ) Xn atTop Q)
(hYn : ∀ n, AEMeasurable (Yn n) μ)
(hY : Modes.TendstoInProbability (fun _ : ℕ => μ) Yn atTop (fun _ _ => c)) :
@Modes.TendstoInLaw ℕ (fun _ => Ω) _ ℝ _ _ _ (fun _ => μ) _
(fun n ω => Xn n ω + Yn n ω) atTop (Q.map fun x => x + c)
(Measure.isProbabilityMeasure_map
(measurable_id.add measurable_const).aemeasurable) := by
have hXn : ∀ n, AEMeasurable (Xn n) μ := hX.forall_aemeasurable
have hBaseMeas : ∀ n, AEMeasurable (fun ω => Xn n ω + c) μ := fun n =>
(hXn n).add aemeasurable_const
letI : IsProbabilityMeasure (Q.map fun x : ℝ => x + c) :=
Measure.isProbabilityMeasure_map (measurable_id.add measurable_const).aemeasurable
have hBase : Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n ω => Xn n ω + c) atTop
(Q.map fun x => x + c) := by
exact (Tendsto_dist_iff _ _ _ hBaseMeas).2
(Modes.TendstoInLaw.map_continuous hX (continuous_id.add continuous_const))
have hRem : IsLittleOp (fun n ω => Yn n ω - c) (fun _ => (1 : ℝ)) μ :=
(Modes.TendstoInProbability.isLittleOp_one (Modes.TendstoInProbability.sub_const hY))
apply Modes.TendstoInLaw.add_isLittleOp_one hBase
(fun n => (hXn n).add (hYn n))
refine IsLittleOp.of_abs_le_const_mul_one (C := 1) one_pos hRem ?_
intro n ω
simp [Real.norm_eq_abs]
theorem mul_tendstoInProbability_const reviewed
⚑ flagged
Causalean.Stat.Modes.TendstoInLaw
If a real sequence converges in distribution, a sequence of multipliers is a.e. measurable, and the multipliers converge in probability to a constant, then the product sequence converges in distribution to the limiting law scaled by that constant.
Formal statement
hypotheses
Ω :
Xn Yn :
ℕ → Ω → ℝ
Q :
c :
ℝ
hX :
Modes.TendstoInLaw (fun _ : ℕ => μ) Xn atTop Q
hYn :
∀ n, AEMeasurable (Yn n) μ
hY :
Modes.TendstoInProbability (fun _ : ℕ => μ) Yn atTop (fun _ _ => c)
conclusion
@Modes.TendstoInLaw ℕ (fun _ => Ω) _ ℝ _ _ _ (fun _ => μ) _ (fun n ω => Xn n ω * Yn n ω) atTop (Q.map fun x => c * x) (Measure.isProbabilityMeasure_map (measurable_const.mul measurable_id).aemeasurable)
Proof (Lean source)
theorem Modes.TendstoInLaw.mul_tendstoInProbability_const
{Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
{Xn Yn : ℕ → Ω → ℝ} {Q : Measure ℝ} [IsProbabilityMeasure Q] {c : ℝ}
(hX : Modes.TendstoInLaw (fun _ : ℕ => μ) Xn atTop Q)
(hYn : ∀ n, AEMeasurable (Yn n) μ)
(hY : Modes.TendstoInProbability (fun _ : ℕ => μ) Yn atTop (fun _ _ => c)) :
@Modes.TendstoInLaw ℕ (fun _ => Ω) _ ℝ _ _ _ (fun _ => μ) _
(fun n ω => Xn n ω * Yn n ω) atTop (Q.map fun x => c * x)
(Measure.isProbabilityMeasure_map
(measurable_const.mul measurable_id).aemeasurable) := by
have hXn : ∀ n, AEMeasurable (Xn n) μ := hX.forall_aemeasurable
have hBaseMeas : ∀ n, AEMeasurable (fun ω => c * Xn n ω) μ := fun n =>
aemeasurable_const.mul (hXn n)
letI : IsProbabilityMeasure (Q.map fun x : ℝ => c * x) :=
Measure.isProbabilityMeasure_map (measurable_const.mul measurable_id).aemeasurable
have hBase : Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n ω => c * Xn n ω) atTop
(Q.map fun x => c * x) := by
exact (Tendsto_dist_iff _ _ _ hBaseMeas).2
(Modes.TendstoInLaw.const_mul_tendsto hX tendsto_const_nhds)
have hTight : IsBigOp Xn (fun _ => (1 : ℝ)) μ := Modes.TendstoInLaw.tightness hX
have hSmall : IsLittleOp (fun n ω => Yn n ω - c) (fun _ => (1 : ℝ)) μ :=
(Modes.TendstoInProbability.isLittleOp_one (Modes.TendstoInProbability.sub_const hY))
have hRem : IsLittleOp (fun n ω => Xn n ω * (Yn n ω - c))
(fun _ => (1 : ℝ)) μ := hTight.mul_isLittleOp_one_isLittleOp hSmall
apply Modes.TendstoInLaw.add_isLittleOp_one hBase
(fun n => (hXn n).mul (hYn n))
refine IsLittleOp.of_abs_le_const_mul_one (C := 1) one_pos hRem ?_
intro n ω
simp [Real.norm_eq_abs, mul_sub, mul_comm]
theorem smul_tendstoInProbability_const reviewed
⚑ flagged
Causalean.Stat.Modes.TendstoInLaw
If a vector sequence converges in distribution, scalar multipliers are a.e. measurable, and the multipliers converge in probability to a constant, then the scalar multiples converge in distribution to the limiting law scaled by that constant.
Formal statement
hypotheses
Omega E :
NormedSpace ℝ E
Xn :
ℕ → Omega → E
Yn :
ℕ → Omega → ℝ
Q :
c :
ℝ
hYn :
∀ n, AEMeasurable (Yn n) mu
conclusion
@Modes.TendstoInLaw ℕ (fun _ => Omega) _ E _ _ _ (fun _ => mu) _ (fun n omega => Yn n omega • Xn n omega) atTop (Q.map fun x => c • x) (Measure.isProbabilityMeasure_map (continuous_const_smul c).measurable.aemeasurable)
Proof (Lean source)
theorem Modes.TendstoInLaw.smul_tendstoInProbability_const
{Omega E : Type*} [MeasurableSpace Omega] {mu : Measure Omega}
[IsProbabilityMeasure mu]
[NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E]
{Xn : ℕ → Omega → E} {Yn : ℕ → Omega → ℝ}
{Q : Measure E} [IsProbabilityMeasure Q] {c : ℝ}
(hX : Modes.TendstoInLaw (fun _ : ℕ => mu) Xn atTop Q)
(hYn : ∀ n, AEMeasurable (Yn n) mu)
(hY : Modes.TendstoInProbability (fun _ : ℕ => mu) Yn atTop (fun _ _ => c)) :
@Modes.TendstoInLaw ℕ (fun _ => Omega) _ E _ _ _ (fun _ => mu) _
(fun n omega => Yn n omega • Xn n omega) atTop (Q.map fun x => c • x)
(Measure.isProbabilityMeasure_map
(continuous_const_smul c).measurable.aemeasurable) := by
have hXn : ∀ n, AEMeasurable (Xn n) mu := hX.forall_aemeasurable
have hBaseMeas : ∀ n, AEMeasurable (fun omega => c • Xn n omega) mu := fun n =>
aemeasurable_const.smul (hXn n)
letI : IsProbabilityMeasure (Q.map fun x : E => c • x) :=
Measure.isProbabilityMeasure_map (continuous_const_smul c).measurable.aemeasurable
have hBase : Modes.TendstoInLaw (fun _ : ℕ => mu) (fun n omega => c • Xn n omega) atTop
(Q.map fun x => c • x) :=
(Tendsto_dist_vec_iff _ _ _ hBaseMeas).2
(Modes.TendstoInLaw.map_continuous hX (continuous_const_smul c))
have hNormMeas : ∀ n, AEMeasurable (fun omega => ‖Xn n omega‖) mu := fun n =>
continuous_norm.measurable.comp_aemeasurable (hXn n)
letI : IsProbabilityMeasure (Q.map fun x : E => ‖x‖) :=
Measure.isProbabilityMeasure_map continuous_norm.measurable.aemeasurable
have hNormDist : Modes.TendstoInLaw (fun _ : ℕ => mu) (fun n omega => ‖Xn n omega‖) atTop
(Q.map fun x => ‖x‖) :=
(Tendsto_dist_iff _ _ _ hNormMeas).2
(Modes.TendstoInLaw.map_continuous hX continuous_norm)
have hTight : IsBigOp (fun n omega => ‖Xn n omega‖) (fun _ => (1 : ℝ)) mu :=
Modes.TendstoInLaw.tightness hNormDist
have hSmall : IsLittleOp (fun n omega => Yn n omega - c) (fun _ => (1 : ℝ)) mu :=
(Modes.TendstoInProbability.isLittleOp_one (Modes.TendstoInProbability.sub_const hY))
have hProduct : IsLittleOp (fun n omega => ‖Xn n omega‖ * (Yn n omega - c))
(fun _ => (1 : ℝ)) mu := hTight.mul_isLittleOp_one_isLittleOp hSmall
apply Modes.TendstoInLaw.add_isLittleOp_one hBase
(fun n => (hYn n).smul (hXn n))
have hRem : IsLittleOp (fun n omega =>
‖Yn n omega • Xn n omega - c • Xn n omega‖) (fun _ => (1 : ℝ)) mu := by
have heq : (fun n omega => ‖Yn n omega • Xn n omega - c • Xn n omega‖) =
fun n omega => ‖Xn n omega‖ * |Yn n omega - c| := by
funext n omega
rw [← sub_smul, norm_smul, Real.norm_eq_abs, mul_comm]
change IsLittleOp (fun n omega =>
‖Yn n omega • Xn n omega - c • Xn n omega‖) (fun _ => (1 : ℝ)) mu
rw [heq]
refine IsLittleOp.of_abs_le_const_mul_one (C := 1) one_pos hProduct ?_
intro n omega
simp [abs_mul]
intro ε hε
simpa only [norm_norm, Pi.smul_apply'] using hRem ε hε
StochasticOrder 5 core · 8 supporting This module provides filter-general, row-varying stochastic big-O and little-o. ★ tendstoInProbability_zero_iff_isLittleOpF_one★ mul★ mul_boundedInProbability
Stochastic order
This module provides filter-general, row-varying stochastic big-O and little-o. Together with
Causalean.Stat.Limit.Modes, it supplies one vocabulary for scalar and vector statistics,
triangular arrays, and finite-design rows. The definitions are filter-general, row-varying
extensions of the sequence definitions in van der Vaart (1998), §2.2, and Hansen (2022), §5.11;
the eventually-small formulation of O_p is primary because it composes directly with filters,
while boundedInProbability_iff_limsup recovers the textbook limsup form.
def BoundedInProbability reviewed
⚑ flagged
Causalean.Stat.Modes
Given row measures, normed row random variables, an index filter, and a real rate, boundedness in probability at that rate means that every positive probability tolerance has a positive finite multiplier for which the weak norm tail is eventually below the tolerance.
Definition (Lean source)
parameters
ι :
Type*
ι → Type*
∀ i, MeasurableSpace (Ω i)
E :
Type*
μ :
(i : ι) → Measure (Ω i)
X :
(i : ι) → Ω i → E
l :
Filter ι
r :
ι → ℝ
δ :
ℝ≥0∞
0 < δ
def
BoundedInProbability μ X l r :
Prop
given by
∃ M : ℝ,
clause 1
0 < M
clause 2
∀ᶠ i in l, μ i {ω | M * r i ≤ ‖X i ω‖} ≤ δ
def IsLittleOpF reviewed
⚑ flagged
Causalean.Stat.Modes
Given row measures, normed row random variables, an index filter, and a real rate, stochastic little-o at that rate means that the weak norm tail at every positive multiple of the rate tends to zero.
Definition (Lean source)
parameters
ι :
Type*
ι → Type*
∀ i, MeasurableSpace (Ω i)
E :
Type*
μ :
(i : ι) → Measure (Ω i)
X :
(i : ι) → Ω i → E
l :
Filter ι
r :
ι → ℝ
ε :
ℝ
0 < ε
def
IsLittleOpF μ X l r :
Prop
given by
Tendsto (fun i => μ i {ω | ε * r i ≤ ‖X i ω‖}) l (𝓝 0)
theorem tendstoInProbability_zero_iff_isLittleOpF_one reviewed
⚑ flagged
Causalean.Stat.Modes
For row measures, normed row random variables, and an index filter, convergence to zero in the row measures is equivalent to stochastic little-o at the constant unit rate in those same measures.
Formal statement
hypotheses
ι :
Type*
ι → Type*
∀ i, MeasurableSpace (Ω i)
E :
Type*
μ :
(i : ι) → Measure (Ω i)
X :
(i : ι) → Ω i → E
l :
Filter ι
conclusion
TendstoInProbability μ X l (fun _ _ => 0) ↔ IsLittleOpF μ X l (fun _ => 1)
Proof (Lean source)
theorem tendstoInProbability_zero_iff_isLittleOpF_one
{ι : Type*} {Ω : ι → Type*} [∀ i, MeasurableSpace (Ω i)]
{E : Type*} [SeminormedAddCommGroup E]
(μ : (i : ι) → Measure (Ω i)) (X : (i : ι) → Ω i → E) (l : Filter ι) :
TendstoInProbability μ X l (fun _ _ => 0) ↔
IsLittleOpF μ X l (fun _ => 1) := by
rw [tendstoInProbability_iff_norm]
simp only [IsLittleOpF, sub_zero, mul_one]
theorem mul reviewed
⚑ flagged
Causalean.Stat.Modes.BoundedInProbability
If two row families are bounded in probability at respective rates and both rates are eventually positive, then their product is bounded in probability at the product rate.
Formal statement
hypotheses
ι :
Type*
ι → Type*
∀ i, MeasurableSpace (Ω i)
E :
Type*
μ :
(i : ι) → Measure (Ω i)
X Y :
(i : ι) → Ω i → E
l :
Filter ι
r s :
ι → ℝ
hX :
BoundedInProbability μ X l r
hY :
BoundedInProbability μ Y l s
hr :
∀ᶠ i in l, 0 < r i
hs :
∀ᶠ i in l, 0 < s i
conclusion
BoundedInProbability μ (fun i ω => X i ω * Y i ω) l (fun i => r i * s i)
Proof (Lean source)
theorem BoundedInProbability.mul
{ι : Type*} {Ω : ι → Type*} [∀ i, MeasurableSpace (Ω i)]
{E : Type*} [NormedRing E]
{μ : (i : ι) → Measure (Ω i)} {X Y : (i : ι) → Ω i → E}
{l : Filter ι} {r s : ι → ℝ}
(hX : BoundedInProbability μ X l r) (hY : BoundedInProbability μ Y l s)
(hr : ∀ᶠ i in l, 0 < r i) (hs : ∀ᶠ i in l, 0 < s i) :
BoundedInProbability μ (fun i ω => X i ω * Y i ω) l (fun i => r i * s i) := by
intro δ hδ
by_cases hδtop : δ = ∞
· exact ⟨1, one_pos, by simp [hδtop]⟩
have hhalf : 0 < δ / 2 := ENNReal.div_pos hδ.ne' (by norm_num)
obtain ⟨M, hM, hXM⟩ := hX (δ / 2) hhalf
obtain ⟨N, hN, hYN⟩ := hY (δ / 2) hhalf
refine ⟨M * N, mul_pos hM hN, ?_⟩
filter_upwards [hr, hs, hXM, hYN] with i hri hsi hXi hYi
calc
μ i {ω | (M * N) * (r i * s i) ≤ ‖X i ω * Y i ω‖}
≤ μ i {ω | M * r i ≤ ‖X i ω‖} + μ i {ω | N * s i ≤ ‖Y i ω‖} :=
measure_mul_norm_tail_le (μ i) (X i) (Y i) hM hN hri hsi
_ ≤ δ / 2 + δ / 2 := add_le_add hXi hYi
_ = δ := ENNReal.add_halves δ
theorem mul_boundedInProbability reviewed
⚑ flagged
Causalean.Stat.Modes.IsLittleOpF
If one row family is stochastic little-o at one rate, another is bounded in probability at a second rate, and both rates are eventually positive, then their product is stochastic little-o at the product rate.
Formal statement
hypotheses
ι :
Type*
ι → Type*
∀ i, MeasurableSpace (Ω i)
E :
Type*
μ :
(i : ι) → Measure (Ω i)
X Y :
(i : ι) → Ω i → E
l :
Filter ι
r s :
ι → ℝ
hX :
IsLittleOpF μ X l r
hY :
BoundedInProbability μ Y l s
hr :
∀ᶠ i in l, 0 < r i
hs :
∀ᶠ i in l, 0 < s i
conclusion
IsLittleOpF μ (fun i ω => X i ω * Y i ω) l (fun i => r i * s i)
Proof (Lean source)
theorem IsLittleOpF.mul_boundedInProbability
{ι : Type*} {Ω : ι → Type*} [∀ i, MeasurableSpace (Ω i)]
{E : Type*} [NormedRing E]
{μ : (i : ι) → Measure (Ω i)} {X Y : (i : ι) → Ω i → E}
{l : Filter ι} {r s : ι → ℝ}
(hX : IsLittleOpF μ X l r) (hY : BoundedInProbability μ Y l s)
(hr : ∀ᶠ i in l, 0 < r i) (hs : ∀ᶠ i in l, 0 < s i) :
IsLittleOpF μ (fun i ω => X i ω * Y i ω) l (fun i => r i * s i) := by
intro ε hε
rw [ENNReal.tendsto_nhds_zero]
intro δ hδ
by_cases hδtop : δ = ∞
· simp [hδtop]
have hhalf : 0 < δ / 2 := ENNReal.div_pos hδ.ne' (by norm_num)
obtain ⟨M, hM, hYM⟩ := hY (δ / 2) hhalf
have hXt := hX (ε / M) (div_pos hε hM)
rw [ENNReal.tendsto_nhds_zero] at hXt
have hXsmall := hXt (δ / 2) hhalf
filter_upwards [hr, hs, hYM, hXsmall] with i hri hsi hYi hXi
have htail := measure_mul_norm_tail_le (μ i) (X i) (Y i)
(div_pos hε hM) hM hri hsi
rw [div_mul_cancel₀ ε hM.ne'] at htail
exact htail.trans (by simpa [ENNReal.add_halves] using add_le_add hXi hYi)
8 supporting declarations (lemmas, instances)
-
boundedInProbability_iff_stricttheorem — If the rate is eventually positive, then for row measures, row variables, a filter, and that rate, boundedness in probability using weak tail events is equivalent to the usual strict-tail formulation.hypothesesι :Type*ι → Type*∀ i, MeasurableSpace (Ω i)E :Type*μ :(i : ι) → Measure (Ω i)X :(i : ι) → Ω i → El :Filter ιr :ι → ℝhr :∀ᶠ i in l, 0 < r iconclusionBoundedInProbability μ X l r↔ ∀ δ : ℝ≥0∞, 0 < δ → ∃ M : ℝ, 0 < M ∧ ∀ᶠ i in l, μ i {ω | M * r i < ‖X i ω‖} ≤ δProof (Lean source)
theorem boundedInProbability_iff_strict {ι : Type*} {Ω : ι → Type*} [∀ i, MeasurableSpace (Ω i)] {E : Type*} [SeminormedAddCommGroup E] (μ : (i : ι) → Measure (Ω i)) (X : (i : ι) → Ω i → E) (l : Filter ι) (r : ι → ℝ) (hr : ∀ᶠ i in l, 0 < r i) : BoundedInProbability μ X l r ↔ ∀ δ : ℝ≥0∞, 0 < δ → ∃ M : ℝ, 0 < M ∧ ∀ᶠ i in l, μ i {ω | M * r i < ‖X i ω‖} ≤ δ := by constructor · intro h δ hδ obtain ⟨M, hM, htail⟩ := h δ hδ refine ⟨M, hM, ?_⟩ filter_upwards [htail] with i hi exact (measure_mono fun _ hω => (show M * r i ≤ _ from hω.le)).trans hi · intro h δ hδ obtain ⟨M, hM, htail⟩ := h δ hδ refine ⟨2 * M, by positivity, ?_⟩ filter_upwards [hr, htail] with i hri hi refine (measure_mono fun _ hω => ?_).trans hi change M * r i < _ exact (by nlinarith : M * r i < 2 * M * r i).trans_le hω -
isLittleOpF_iff_stricttheorem — If the rate is eventually positive, then for row measures, row variables, a filter, and that rate, stochastic little-o using weak tail events is equivalent to the usual strict-tail formulation.hypothesesι :Type*ι → Type*∀ i, MeasurableSpace (Ω i)E :Type*μ :(i : ι) → Measure (Ω i)X :(i : ι) → Ω i → El :Filter ιr :ι → ℝhr :∀ᶠ i in l, 0 < r iconclusionIsLittleOpF μ X l r↔ ∀ ε : ℝ, 0 < ε → Tendsto (fun i => μ i {ω | ε * r i < ‖X i ω‖}) l (𝓝 0)Proof (Lean source)
theorem isLittleOpF_iff_strict {ι : Type*} {Ω : ι → Type*} [∀ i, MeasurableSpace (Ω i)] {E : Type*} [SeminormedAddCommGroup E] (μ : (i : ι) → Measure (Ω i)) (X : (i : ι) → Ω i → E) (l : Filter ι) (r : ι → ℝ) (hr : ∀ᶠ i in l, 0 < r i) : IsLittleOpF μ X l r ↔ ∀ ε : ℝ, 0 < ε → Tendsto (fun i => μ i {ω | ε * r i < ‖X i ω‖}) l (𝓝 0) := by constructor · intro h ε hε refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds (h ε hε) (fun _ => zero_le) ?_ intro i exact measure_mono fun _ hω => (show ε * r i ≤ _ from hω.le) · intro h ε hε refine tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds (h (ε / 2) (by positivity)) (.of_forall fun _ => zero_le) ?_ filter_upwards [hr] with i hri refine measure_mono fun _ hω => ?_ change ε / 2 * r i < _ exact (by nlinarith : ε / 2 * r i < ε * r i).trans_le hω -
boundedInProbability_iff_limsuptheorem — For row measures, row variables, a filter, and a rate, boundedness in probability is equivalent to the textbook limsup tail criterion.hypothesesι :Type*ι → Type*∀ i, MeasurableSpace (Ω i)E :Type*μ :(i : ι) → Measure (Ω i)X :(i : ι) → Ω i → El :Filter ιr :ι → ℝconclusionBoundedInProbability μ X l r↔ ∀ δ : ℝ≥0∞, 0 < δ → ∃ M : ℝ, 0 < M ∧ l.limsup (fun i => μ i {ω | M * r i ≤ ‖X i ω‖}) ≤ δProof (Lean source)
theorem boundedInProbability_iff_limsup {ι : Type*} {Ω : ι → Type*} [∀ i, MeasurableSpace (Ω i)] {E : Type*} [SeminormedAddCommGroup E] (μ : (i : ι) → Measure (Ω i)) (X : (i : ι) → Ω i → E) (l : Filter ι) (r : ι → ℝ) : BoundedInProbability μ X l r ↔ ∀ δ : ℝ≥0∞, 0 < δ → ∃ M : ℝ, 0 < M ∧ l.limsup (fun i => μ i {ω | M * r i ≤ ‖X i ω‖}) ≤ δ := by constructor · intro h δ hδ obtain ⟨M, hM, htail⟩ := h δ hδ exact ⟨M, hM, Filter.limsup_le_of_le (u := fun i => μ i {ω | M * r i ≤ ‖X i ω‖}) (a := δ) (h := htail)⟩ · intro h δ hδ by_cases hδtop : δ = ∞ · exact ⟨1, one_pos, by simp [hδtop]⟩ have hhalf : 0 < δ / 2 := ENNReal.div_pos hδ.ne' (by norm_num) obtain ⟨M, hM, hlim⟩ := h (δ / 2) hhalf refine ⟨M, hM, ?_⟩ have hhalf_lt : δ / 2 < δ := ENNReal.half_lt_self hδ.ne' hδtop exact (((Filter.limsup_le_iff (u := fun i => μ i {ω | M * r i ≤ ‖X i ω‖}) (x := δ / 2)).mp hlim) δ hhalf_lt).mono fun _ hi => hi.le -
boundedInProbabilitytheorem — If a row family is stochastic little-o at a rate, then it is bounded in probability at the same rate.hypothesesι :Type*ι → Type*∀ i, MeasurableSpace (Ω i)E :Type*μ :(i : ι) → Measure (Ω i)X :(i : ι) → Ω i → El :Filter ιr :ι → ℝh :IsLittleOpF μ X l rconclusionBoundedInProbability μ X l rProof (Lean source)
theorem IsLittleOpF.boundedInProbability {ι : Type*} {Ω : ι → Type*} [∀ i, MeasurableSpace (Ω i)] {E : Type*} [SeminormedAddCommGroup E] {μ : (i : ι) → Measure (Ω i)} {X : (i : ι) → Ω i → E} {l : Filter ι} {r : ι → ℝ} (h : IsLittleOpF μ X l r) : BoundedInProbability μ X l r := by intro δ hδ refine ⟨1, one_pos, ?_⟩ have ht := h 1 one_pos rw [ENNReal.tendsto_nhds_zero] at ht simpa only [one_mul] using ht δ hδ -
addtheorem — If two row families are bounded in probability at the same rate, then their sum is bounded in probability at that rate.hypothesesι :Type*ι → Type*∀ i, MeasurableSpace (Ω i)E :Type*μ :(i : ι) → Measure (Ω i)X Y :(i : ι) → Ω i → El :Filter ιr :ι → ℝhX :BoundedInProbability μ X l rhY :BoundedInProbability μ Y l rconclusionBoundedInProbability μ (fun i ω => X i ω + Y i ω) l rProof (Lean source)
theorem BoundedInProbability.add {ι : Type*} {Ω : ι → Type*} [∀ i, MeasurableSpace (Ω i)] {E : Type*} [SeminormedAddCommGroup E] {μ : (i : ι) → Measure (Ω i)} {X Y : (i : ι) → Ω i → E} {l : Filter ι} {r : ι → ℝ} (hX : BoundedInProbability μ X l r) (hY : BoundedInProbability μ Y l r) : BoundedInProbability μ (fun i ω => X i ω + Y i ω) l r := by intro δ hδ by_cases hδtop : δ = ∞ · exact ⟨1, one_pos, by simp [hδtop]⟩ have hhalf : 0 < δ / 2 := ENNReal.div_pos hδ.ne' (by norm_num) obtain ⟨M, hM, hXM⟩ := hX (δ / 2) hhalf obtain ⟨N, hN, hYN⟩ := hY (δ / 2) hhalf refine ⟨M + N, add_pos hM hN, ?_⟩ filter_upwards [hXM, hYN] with i hXi hYi calc μ i {ω | (M + N) * r i ≤ ‖X i ω + Y i ω‖} ≤ μ i {ω | M * r i ≤ ‖X i ω‖} + μ i {ω | N * r i ≤ ‖Y i ω‖} := measure_add_norm_tail_le (μ i) (X i) (Y i) _ ≤ δ / 2 + δ / 2 := add_le_add hXi hYi _ = δ := ENNReal.add_halves δ -
addtheorem — If two row families are stochastic little-o at the same rate and that rate is eventually nonnegative, then their sum is stochastic little-o at that rate.hypothesesι :Type*ι → Type*∀ i, MeasurableSpace (Ω i)E :Type*μ :(i : ι) → Measure (Ω i)X Y :(i : ι) → Ω i → El :Filter ιr :ι → ℝhX :IsLittleOpF μ X l rhY :IsLittleOpF μ Y l rhr :∀ᶠ i in l, 0 ≤ r iconclusionIsLittleOpF μ (fun i ω => X i ω + Y i ω) l rProof (Lean source)
theorem IsLittleOpF.add {ι : Type*} {Ω : ι → Type*} [∀ i, MeasurableSpace (Ω i)] {E : Type*} [SeminormedAddCommGroup E] {μ : (i : ι) → Measure (Ω i)} {X Y : (i : ι) → Ω i → E} {l : Filter ι} {r : ι → ℝ} (hX : IsLittleOpF μ X l r) (hY : IsLittleOpF μ Y l r) (hr : ∀ᶠ i in l, 0 ≤ r i) : IsLittleOpF μ (fun i ω => X i ω + Y i ω) l r := by intro ε hε have ht : Tendsto (fun i => μ i {ω | ε / 2 * r i ≤ ‖X i ω‖} + μ i {ω | ε / 2 * r i ≤ ‖Y i ω‖}) l (𝓝 0) := by simpa using (hX (ε / 2) (by positivity)).add (hY (ε / 2) (by positivity)) refine tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds ht (.of_forall fun _ => zero_le) ?_ filter_upwards [hr] with i _hri have hhalf : ε / 2 + ε / 2 = ε := by ring simpa only [hhalf] using measure_add_norm_tail_le (μ i) (X i) (Y i) (a := ε / 2) (b := ε / 2) (r := r i) -
multheorem — If two row families are stochastic little-o at respective rates and both rates are eventually positive, then their product is stochastic little-o at the product rate.hypothesesι :Type*ι → Type*∀ i, MeasurableSpace (Ω i)E :Type*μ :(i : ι) → Measure (Ω i)X Y :(i : ι) → Ω i → El :Filter ιr s :ι → ℝhX :IsLittleOpF μ X l rhY :IsLittleOpF μ Y l shr :∀ᶠ i in l, 0 < r ihs :∀ᶠ i in l, 0 < s iconclusionIsLittleOpF μ (fun i ω => X i ω * Y i ω) l (fun i => r i * s i)Proof (Lean source)
theorem IsLittleOpF.mul {ι : Type*} {Ω : ι → Type*} [∀ i, MeasurableSpace (Ω i)] {E : Type*} [NormedRing E] {μ : (i : ι) → Measure (Ω i)} {X Y : (i : ι) → Ω i → E} {l : Filter ι} {r s : ι → ℝ} (hX : IsLittleOpF μ X l r) (hY : IsLittleOpF μ Y l s) (hr : ∀ᶠ i in l, 0 < r i) (hs : ∀ᶠ i in l, 0 < s i) : IsLittleOpF μ (fun i ω => X i ω * Y i ω) l (fun i => r i * s i) := hX.mul_boundedInProbability hY.boundedInProbability hr hs -
isLittleOpF_of_tendsto_ratiotheorem — If a row family is bounded in probability at a rate, the comparison rate is eventually positive, and the ratio of the first rate to the comparison rate tends to zero, then the family is stochastic little-o at the comparison rate.hypothesesι :Type*ι → Type*∀ i, MeasurableSpace (Ω i)E :Type*μ :(i : ι) → Measure (Ω i)X :(i : ι) → Ω i → El :Filter ιr s :ι → ℝhX :BoundedInProbability μ X l rhs :∀ᶠ i in l, 0 < s ihrs :Tendsto (fun i => r i / s i) l (𝓝 0)conclusionIsLittleOpF μ X l sProof (Lean source)
theorem BoundedInProbability.isLittleOpF_of_tendsto_ratio {ι : Type*} {Ω : ι → Type*} [∀ i, MeasurableSpace (Ω i)] {E : Type*} [SeminormedAddCommGroup E] {μ : (i : ι) → Measure (Ω i)} {X : (i : ι) → Ω i → E} {l : Filter ι} {r s : ι → ℝ} (hX : BoundedInProbability μ X l r) (hs : ∀ᶠ i in l, 0 < s i) (hrs : Tendsto (fun i => r i / s i) l (𝓝 0)) : IsLittleOpF μ X l s := by intro ε hε rw [ENNReal.tendsto_nhds_zero] intro δ hδ obtain ⟨M, hM, htail⟩ := hX δ hδ have hratio : ∀ᶠ i in l, r i / s i < ε / M := hrs.eventually_lt_const (div_pos hε hM) filter_upwards [hs, hratio, htail] with i hsi hri hi have hquot : (M * r i) / s i < ε := by calc (M * r i) / s i = (r i / s i) * M := by ring _ < ε := (lt_div_iff₀ hM).mp hri have hrate : M * r i ≤ ε * s i := ((div_lt_iff₀ hsi).mp hquot).le exact (measure_norm_tail_mono (μ i) (X i) hrate).trans hi
StochasticOrderEnvelope 3 core · 5 supporting This module turns deterministic or conditional-envelope estimates into the O_p and o_p statements used throughout statistical estimation. ★ of_sqEnvelope★ integral_abs_mul_le_eLpNorm_mul_eLpNorm★ integral_abs_mul_op_of_eLpNorm_op
Stochastic-order helpers from envelopes and L² rates
This module turns deterministic or conditional-envelope estimates into the O_p and o_p
statements used throughout statistical estimation. The square-envelope lemmas
IsBigOp.of_sqEnvelope and IsLittleOp.of_sqEnvelope say that an almost-sure bound
|X_n|^2 <= c_n, together with an O_p or o_p bound for c_n at rate r_n^2, yields the
corresponding stochastic-order bound for X_n at rate r_n.
The file also contains two generic reduction tools for truncation and bounded convergence:
IsLittleOp.of_eq_on_asymptotic transfers an o_p result across an asymptotically negligible
exception set, and lintegral_ofReal_tendsto_zero_of_bdd_isLittleOp upgrades bounded convergence
in probability to convergence of the nonnegative lintegral.
The final section packages Cauchy-Schwarz bounds in the forms needed by estimation remainders.
abs_integral_le_eLpNorm_two controls a mean by an L2 norm on a probability space,
integral_abs_mul_le_eLpNorm_mul_eLpNorm bounds an integrated product by the product of L2 norms,
and integral_op_of_eLpNorm_op / integral_abs_mul_op_of_eLpNorm_op lift random L2-rate
statements to stochastic-order bounds for integrated biases.
theorem of_sqEnvelope reviewed
⚑ flagged
Causalean.Stat.IsLittleOp
Square-envelope stochastic little-o lemma. Under a sampling measure, if the rate is eventually positive, X_n² is bounded above by c_n almost everywhere, and c_n is stochastic little-o of r_n² in that measure, then X_n is stochastic little-o of r_n in the same measure. Positivity permits squaring the tail threshold.
Formal statement
hypotheses
rn :
ℕ → ℝ
hrn :
∀ᶠ n in atTop, 0 < rn n
hbound :
∀ n, ∀ᵐ ω ∂μ, (Xn n ω) ^ 2 ≤ cn n ω
hcn_LittleOp :
IsLittleOp cn (fun n => (rn n) ^ 2) μ
conclusion
IsLittleOp Xn rn μ
Proof (Lean source)
theorem IsLittleOp.of_sqEnvelope
{Xn : ℕ → Ω → ℝ} {cn : ℕ → Ω → ℝ} {rn : ℕ → ℝ}
(hrn : ∀ᶠ n in atTop, 0 < rn n)
(hbound : ∀ n, ∀ᵐ ω ∂μ, (Xn n ω) ^ 2 ≤ cn n ω)
(hcn_LittleOp : IsLittleOp cn (fun n => (rn n) ^ 2) μ) :
IsLittleOp Xn rn μ := by
intro ε hε
have hε2 : 0 < ε ^ 2 := sq_pos_of_pos hε
have hcn := hcn_LittleOp (ε ^ 2) hε2
refine tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds hcn
(.of_forall fun _ => zero_le) ?_
filter_upwards [hrn] with n hrn_pos
apply MeasureTheory.measure_mono_ae
filter_upwards [hbound n] with ω hb hω
change ε * rn n ≤ |Xn n ω| at hω
change ε ^ 2 * rn n ^ 2 ≤ |cn n ω|
have hεr_nonneg : 0 ≤ ε * rn n := (mul_pos hε hrn_pos).le
have hsqX : (ε * rn n) ^ 2 ≤ (Xn n ω) ^ 2 := by
rw [← sq_abs (Xn n ω)]
nlinarith [sq_nonneg (|Xn n ω| - ε * rn n)]
calc
ε ^ 2 * rn n ^ 2 = (ε * rn n) ^ 2 := by ring
_ ≤ (Xn n ω) ^ 2 := hsqX
_ ≤ cn n ω := hb
_ ≤ |cn n ω| := le_abs_self _
theorem integral_abs_mul_le_eLpNorm_mul_eLpNorm reviewed
⚑ flagged
Causalean.Stat
Cauchy–Schwarz for products of L²-functions. If f is square-integrable against the measure ν and g is square-integrable against ν, then the integral of |f · g| against ν is at most the product of the L² norms ‖f‖₂ · ‖g‖₂. Stated for the absolute value of the product because that is the form consumed by the AIPW remainder bound.
Formal statement
Proof (Lean source)
theorem integral_abs_mul_le_eLpNorm_mul_eLpNorm
{f g : X → ℝ} (hf : MemLp f 2 ν) (hg : MemLp g 2 ν) :
∫ x, |f x * g x| ∂ν ≤ (eLpNorm f 2 ν).toReal * (eLpNorm g 2 ν).toReal := by
have hf' : MemLp f (ofReal (2 : ℝ)) ν := by simpa using hf
have hg' : MemLp g (ofReal (2 : ℝ)) ν := by simpa using hg
have hholder : (2 : ℝ).HolderConjugate 2 := Real.HolderConjugate.two_two
have h := MeasureTheory.integral_mul_norm_le_Lp_mul_Lq (μ := ν) (f := f) (g := g)
(p := 2) (q := 2) hholder hf' hg'
have hf_eq : ((∫ x, ‖f x‖ ^ (2 : ℝ) ∂ν) ^ ((1 : ℝ) / 2)) =
(eLpNorm f 2 ν).toReal := by
rw [hf.eLpNorm_eq_integral_rpow_norm (by norm_num) (by norm_num)]
rw [ENNReal.toReal_ofReal]
· norm_num
· exact Real.rpow_nonneg
(integral_nonneg_of_ae (Eventually.of_forall fun x => by positivity)) _
have hg_eq : ((∫ x, ‖g x‖ ^ (2 : ℝ) ∂ν) ^ ((1 : ℝ) / 2)) =
(eLpNorm g 2 ν).toReal := by
rw [hg.eLpNorm_eq_integral_rpow_norm (by norm_num) (by norm_num)]
rw [ENNReal.toReal_ofReal]
· norm_num
· exact Real.rpow_nonneg
(integral_nonneg_of_ae (Eventually.of_forall fun x => by positivity)) _
convert h using 1
· congr 1
funext x
simp [Real.norm_eq_abs, abs_mul]
· rw [hf_eq, hg_eq]
theorem integral_abs_mul_op_of_eLpNorm_op reviewed
⚑ flagged
Causalean.Stat
L² product rate ⇒ integrated absolute-product rate. Suppose each random function is square-integrable, the fixed factor is square-integrable, its L² norm is positive, and the random L² norm is little-o at those rates. Then the integrated absolute product is little-o at the product rate.
Formal statement
Proof (Lean source)
theorem integral_abs_mul_op_of_eLpNorm_op
{fn : ℕ → Ω → X → ℝ} {g : X → ℝ}
(hfn_memLp : ∀ n ω, MemLp (fn n ω) 2 ν)
(hg_memLp : MemLp g 2 ν)
(hg_pos : 0 < (eLpNorm g 2 ν).toReal)
{sn : ℕ → ℝ}
(hfn_rate :
IsLittleOp (fun n ω => (eLpNorm (fn n ω) 2 ν).toReal) sn μ) :
IsLittleOp
(fun n ω => ∫ x, |fn n ω x * g x| ∂ν)
(fun n => sn n * (eLpNorm g 2 ν).toReal) μ := by
let c : ℝ := (eLpNorm g 2 ν).toReal
have hc_pos : 0 < c := hg_pos
intro ε hε
have htarget := hfn_rate ε hε
have hpoint : ∀ n,
μ {ω | ε * (sn n * (eLpNorm g 2 ν).toReal) ≤
|∫ x, |fn n ω x * g x| ∂ν|} ≤
μ {ω | ε * sn n ≤ |(eLpNorm (fn n ω) 2 ν).toReal|} := by
intro n
apply measure_mono
intro ω hω
have hle := integral_abs_mul_le_eLpNorm_mul_eLpNorm (hfn_memLp n ω) hg_memLp
have hI_prod_nonneg : 0 ≤ ∫ x, |fn n ω x| * |g x| ∂ν :=
integral_nonneg fun x => mul_nonneg (abs_nonneg _) (abs_nonneg _)
have hIge : ε * (sn n * c) ≤ ∫ x, |fn n ω x * g x| ∂ν := by
simpa [c, abs_mul, abs_of_nonneg hI_prod_nonneg] using hω
have hnorm_nonneg : 0 ≤ (eLpNorm (fn n ω) 2 ν).toReal := ENNReal.toReal_nonneg
have hnorm : ε * sn n ≤ (eLpNorm (fn n ω) 2 ν).toReal := by
nlinarith
exact hnorm.trans (le_abs_self _)
refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds htarget
(fun _ => zero_le) hpoint
5 supporting declarations (lemmas, instances)
-
of_sqEnvelopetheorem — Square-envelope O_p lemma. If the rate is eventually positive, |X_n|² ≤ c_n almost surely, and c_n = O_p(r_n²), then X_n = O_p(r_n). Positivity permits squaring the tail threshold.hypothesesrn :ℕ → ℝhrn :∀ᶠ n in atTop, 0 < rn nhbound :∀ n, ∀ᵐ ω ∂μ, (Xn n ω) ^ 2 ≤ cn n ωhcn_BigOp :IsBigOp cn (fun n => (rn n) ^ 2) μconclusionIsBigOp Xn rn μProof (Lean source)
theorem IsBigOp.of_sqEnvelope {Xn : ℕ → Ω → ℝ} {cn : ℕ → Ω → ℝ} {rn : ℕ → ℝ} (hrn : ∀ᶠ n in atTop, 0 < rn n) (hbound : ∀ n, ∀ᵐ ω ∂μ, (Xn n ω) ^ 2 ≤ cn n ω) (hcn_BigOp : IsBigOp cn (fun n => (rn n) ^ 2) μ) : IsBigOp Xn rn μ := by intro δ hδ rcases hcn_BigOp δ hδ with ⟨K, hKpos, hKtail⟩ let M : ℝ := Real.sqrt K have hMpos : 0 < M := Real.sqrt_pos.2 hKpos have hMsq : M ^ 2 = K := Real.sq_sqrt hKpos.le refine ⟨M, hMpos, ?_⟩ filter_upwards [hrn, hKtail] with n hrn_pos hn refine (MeasureTheory.measure_mono_ae ?_).trans hn filter_upwards [hbound n] with ω hb hω change M * rn n ≤ |Xn n ω| at hω change K * rn n ^ 2 ≤ |cn n ω| have hMr_nonneg : 0 ≤ M * rn n := (mul_pos hMpos hrn_pos).le have hsqX : (M * rn n) ^ 2 ≤ (Xn n ω) ^ 2 := by rw [← sq_abs (Xn n ω)] nlinarith [sq_nonneg (|Xn n ω| - M * rn n)] calc K * rn n ^ 2 = (M * rn n) ^ 2 := by rw [← hMsq]; ring _ ≤ (Xn n ω) ^ 2 := hsqX _ ≤ cn n ω := hb _ ≤ |cn n ω| := le_abs_self _ -
of_eq_on_asymptotictheorem — Truncation reduction. If Xn differs from Yn only on a set whose μ-measure tends to 0, and Yn = o_p(rn), then Xn = o_p(rn).Proof (Lean source)
theorem IsLittleOp.of_eq_on_asymptotic {Xn Yn : ℕ → Ω → ℝ} {rn : ℕ → ℝ} (h_diff_to_zero : Tendsto (fun n => μ {ω | Xn n ω ≠ Yn n ω}) atTop (𝓝 0)) (h_tilde : IsLittleOp Yn rn μ) : IsLittleOp Xn rn μ := by intro ε hε have hY := h_tilde ε hε have hpoint : ∀ n, μ {ω | ε * rn n ≤ |Xn n ω|} ≤ μ {ω | Xn n ω ≠ Yn n ω} + μ {ω | ε * rn n ≤ |Yn n ω|} := by intro n calc μ {ω | ε * rn n ≤ |Xn n ω|} ≤ μ ({ω | Xn n ω ≠ Yn n ω} ∪ {ω | ε * rn n ≤ |Yn n ω|}) := by apply measure_mono intro ω hω by_cases hxy : Xn n ω = Yn n ω · exact inr (by simpa [hxy] using hω) · exact inl hxy _ ≤ μ {ω | Xn n ω ≠ Yn n ω} + μ {ω | ε * rn n ≤ |Yn n ω|} := MeasureTheory.measure_union_le _ _ have hsum : Tendsto (fun n => μ {ω | Xn n ω ≠ Yn n ω} + μ {ω | ε * rn n ≤ |Yn n ω|}) atTop (𝓝 0) := by simpa [Real.norm_eq_abs] using h_diff_to_zero.add hY rw [ENNReal.tendsto_nhds_zero] at hsum ⊢ intro δ hδ exact (hsum δ hδ).mono fun n hn => by simpa [Real.norm_eq_abs] using (hpoint n).trans hn -
lintegral_ofReal_tendsto_zero_of_bdd_isLittleOptheorem — Bounded convergence in probability ⇒ L¹ convergence. If Xn ω ∈ [0, M] with M ≥ 0 deterministic, each Xn n is measurable, and Xn = o_p(1) under μ (with μ a probability measure), then ∫⁻ ω, ENNReal.ofReal (Xn n ω) ∂μ → 0 in ℝ≥0∞.hypothesesXn :ℕ → Ω → ℝM :ℝhM :0 ≤ MhXn_meas :∀ n, Measurable (Xn n)hXn_nonneg :∀ n ω, 0 ≤ Xn n ωhXn_bdd :∀ n ω, Xn n ω ≤ MhXn_op :IsLittleOp Xn (fun _ => (1 : ℝ)) μProof (Lean source)
theorem lintegral_ofReal_tendsto_zero_of_bdd_isLittleOp [IsProbabilityMeasure μ] {Xn : ℕ → Ω → ℝ} {M : ℝ} (hM : 0 ≤ M) (hXn_meas : ∀ n, Measurable (Xn n)) (hXn_nonneg : ∀ n ω, 0 ≤ Xn n ω) (hXn_bdd : ∀ n ω, Xn n ω ≤ M) (hXn_op : IsLittleOp Xn (fun _ => (1 : ℝ)) μ) : Tendsto (fun n => ∫⁻ ω, ofReal (Xn n ω) ∂μ) atTop (𝓝 0) := by rw [ENNReal.tendsto_nhds_zero] intro δ hδ by_cases hδtop : δ = ⊤ · filter_upwards with n simp [hδtop] have hδreal_pos : 0 < δ.toReal := ENNReal.toReal_pos (ne_of_gt hδ) hδtop let η : ℝ := δ.toReal / 4 let α : ℝ := δ.toReal / (4 * (M + 1)) have hηpos : 0 < η := by dsimp [η] linarith have hαpos : 0 < α := by dsimp [α] exact div_pos hδreal_pos (mul_pos (by norm_num) (by linarith)) have hlintegral_le : ∀ n, ∫⁻ ω, ofReal (Xn n ω) ∂μ ≤ ofReal η + ofReal M * μ {ω | η * (1 : ℝ) ≤ |Xn n ω|} := by intro n let A : Set Ω := {ω | Xn n ω ≤ η} have hA : MeasurableSet A := by dsimp [A] exact measurableSet_le (hXn_meas n) measurable_const have hsmall : ∫⁻ ω in A, ofReal (Xn n ω) ∂μ ≤ ofReal η := by calc ∫⁻ ω in A, ofReal (Xn n ω) ∂μ ≤ ∫⁻ ω in A, ofReal η ∂μ := by apply setLIntegral_mono measurable_const intro ω hω exact ENNReal.ofReal_le_ofReal hω _ = ofReal η * μ A := by rw [setLIntegral_const] _ ≤ ofReal η * μ univ := by exact mul_le_mul' le_rfl (measure_mono (Set.subset_univ A)) _ = ofReal η := by simp [MeasureTheory.measure_univ] have hlarge : ∫⁻ ω in Aᶜ, ofReal (Xn n ω) ∂μ ≤ ofReal M * μ {ω | η * (1 : ℝ) ≤ |Xn n ω|} := by calc ∫⁻ ω in Aᶜ, ofReal (Xn n ω) ∂μ ≤ ∫⁻ ω in Aᶜ, ofReal M ∂μ := by apply setLIntegral_mono measurable_const intro ω hω exact ENNReal.ofReal_le_ofReal (hXn_bdd n ω) _ = ofReal M * μ Aᶜ := by rw [setLIntegral_const] _ ≤ ofReal M * μ {ω | η * (1 : ℝ) ≤ |Xn n ω|} := by apply mul_le_mul' le_rfl apply measure_mono intro ω hω have hη_lt : η < Xn n ω := lt_of_not_ge hω simpa [abs_of_nonneg (hXn_nonneg n ω)] using hη_lt.le calc ∫⁻ ω, ofReal (Xn n ω) ∂μ = ∫⁻ ω in A, ofReal (Xn n ω) ∂μ + ∫⁻ ω in Aᶜ, ofReal (Xn n ω) ∂μ := by exact (lintegral_add_compl (μ := μ) (fun ω => ofReal (Xn n ω)) hA).symm _ ≤ ofReal η + ofReal M * μ {ω | η * (1 : ℝ) ≤ |Xn n ω|} := add_le_add hsmall hlarge have hprob_event := (ENNReal.tendsto_nhds_zero.mp (hXn_op η hηpos)) (ofReal α) (ENNReal.ofReal_pos.mpr hαpos) filter_upwards [hprob_event] with n hn have hprod_le : ofReal M * μ {ω | η * (1 : ℝ) ≤ |Xn n ω|} ≤ ofReal M * ofReal α := by exact mul_le_mul' le_rfl hn have hsum_eq : ofReal η + ofReal M * ofReal α = ofReal (η + M * α) := by rw [← ENNReal.ofReal_mul hM] rw [← ENNReal.ofReal_add (le_of_lt hηpos) (mul_nonneg hM (le_of_lt hαpos))] have hterm_le : M * α ≤ δ.toReal / 4 := by dsimp [α] field_simp [show (4 : ℝ) * (M + 1) ≠ 0 by nlinarith] nlinarith [mul_le_mul_of_nonneg_left (by linarith : M ≤ M + 1) (le_of_lt hδreal_pos)] have hsum_lt : ofReal (η + M * α) < δ := by rw [ENNReal.ofReal_lt_iff_lt_toReal] · dsimp [η] nlinarith · dsimp [η] nlinarith [le_of_lt hδreal_pos, hM, le_of_lt hαpos] · exact hδtop exact le_of_lt <| (hlintegral_le n).trans_lt <| lt_of_le_of_lt (add_le_add le_rfl hprod_le) <| hsum_eq.trans_lt hsum_lt -
abs_integral_le_eLpNorm_twotheorem — Constant-case Cauchy–Schwarz. If f belongs to L² of the probability measure ν, then the absolute integral of f is at most its L² norm.hypothesesProof (Lean source)
theorem abs_integral_le_eLpNorm_two [IsProbabilityMeasure ν] {f : X → ℝ} (hf : MemLp f 2 ν) : |∫ x, f x ∂ν| ≤ (eLpNorm f 2 ν).toReal := by have h_l1 : |∫ x, f x ∂ν| ≤ (eLpNorm f 1 ν).toReal := by calc |∫ x, f x ∂ν| ≤ ∫ x, |f x| ∂ν := MeasureTheory.abs_integral_le_integral_abs _ = (eLpNorm f 1 ν).toReal := by rw [MeasureTheory.eLpNorm_one_eq_lintegral_enorm] simpa [Real.norm_eq_abs] using MeasureTheory.integral_norm_eq_lintegral_enorm hf.1 exact h_l1.trans (ENNReal.toReal_mono hf.eLpNorm_ne_top (MeasureTheory.eLpNorm_le_eLpNorm_of_exponent_le (by norm_num) hf.1)) -
integral_op_of_eLpNorm_optheorem — L² rate ⇒ integrated bias rate. If each random function is square-integrable, and its L² norm is little-o at that rate, then its integral is little-o at the same rate.hypothesesconclusionIsLittleOp (fun n ω => ∫ x, fn n ω x ∂ν) rn μProof (Lean source)
theorem integral_op_of_eLpNorm_op [IsProbabilityMeasure ν] {fn : ℕ → Ω → X → ℝ} (hfn_memLp : ∀ n ω, MemLp (fn n ω) 2 ν) {rn : ℕ → ℝ} (hfn_rate : IsLittleOp (fun n ω => (eLpNorm (fn n ω) 2 ν).toReal) rn μ) : IsLittleOp (fun n ω => ∫ x, fn n ω x ∂ν) rn μ := by refine IsLittleOp.of_abs_le_const_mul (C := 1) one_pos hfn_rate ?_ intro n ω simpa using abs_integral_le_eLpNorm_two (hfn_memLp n ω)
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, 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
Ω :
Type u_1
X :
Type u_2
S :
IIDSample Ω X μ P
g :
X → ℝ
hg_meas :
hg_int :
Integrable g P
conclusion
Modes.TendstoInProbability (fun _ : ℕ => μ) (S.sampleMean g) atTop (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) :
Modes.TendstoInProbability
(fun _ : ℕ => μ) (S.sampleMean g) atTop (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 `μ`
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, 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
Ω :
Type u_1
X :
Type u_2
S :
IIDSample Ω X μ P
ψ :
X → ℝ
hψ_meas :
hψ_sq_int :
Integrable (fun x => (ψ x) ^ 2) P
conclusion
Modes.TendstoInProbability (fun _ : ℕ => μ) (S.sampleMean (fun x => (ψ x) ^ 2)) atTop (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) :
Modes.TendstoInProbability (fun _ : ℕ => μ) (S.sampleMean (fun x => (ψ x) ^ 2)) atTop
(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)
@[fun_prop] theorem measurable_sampleMean (S : IIDSample Ω X μ P) {g : X → ℝ} (hg_meas : Measurable g) (N : ℕ) : Measurable (S.sampleMean g N) := by unfold IIDSample.sampleMean exact (Finset.measurable_sum _ (fun i _hi => hg_meas.comp (S.meas i))).const_mul _