Stat.Concentration.Hilbert
Concentration inequalities for Hilbert-space-valued random variables.
CrossInnerProduct 2 core · 4 supporting This module bounds cross-inner products and low-rank orthogonal projections from uniform directional second-moment envelopes. ★ indep_inner_sq_integral_le★ projection_norm_tail_le_two
Independent finite-dimensional cross-inner-product bounds
This module bounds cross-inner products and low-rank orthogonal projections from uniform directional second-moment envelopes. The results combine independence with elementary second-moment tail bounds and are reusable in finite-dimensional calibration arguments.
lemma indep_inner_sq_integral_le reviewed
⚑ flagged
Causalean.Stat.Concentration
Let X and Y be random vectors in M-dimensional Euclidean space that are measurable, square-integrable, and independent of each other. If, for a real number Λ, the second moment of the inner product of X with any fixed vector u is at most Λ times the squared norm of u, and the same holds for Y, then the expected squared inner product of X and Y is at most M Λ². No centering of X or Y is assumed.
Formal statement
hypotheses
Ω :
Type*
μ :
M :
X Y :
Ω → EuclideanSpace ℝ (Fin M)
Λ :
ℝ
hX :
hY :
hXL2 :
MemLp X 2 μ
hYL2 :
MemLp Y 2 μ
hind :
IndepFun X Y μ
hXmom :
∀ u, (∫ ω, inner ℝ u (X ω) ^ 2 ∂μ) ≤ Λ * ‖u‖ ^ 2
hYmom :
∀ u, (∫ ω, inner ℝ u (Y ω) ^ 2 ∂μ) ≤ Λ * ‖u‖ ^ 2
conclusion
(∫ ω, inner ℝ (X ω) (Y ω) ^ 2 ∂μ) ≤ M * Λ ^ 2
Proof (Lean source)
lemma indep_inner_sq_integral_le {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
[IsProbabilityMeasure μ] {M : ℕ} [MeasurableSpace (EuclideanSpace ℝ (Fin M))]
[BorelSpace (EuclideanSpace ℝ (Fin M))]
(X Y : Ω → EuclideanSpace ℝ (Fin M)) (Λ : ℝ)
(hX : Measurable X) (hY : Measurable Y) (hXL2 : MemLp X 2 μ) (hYL2 : MemLp Y 2 μ)
(hind : IndepFun X Y μ)
(hXmom : ∀ u, (∫ ω, inner ℝ u (X ω) ^ 2 ∂μ) ≤ Λ * ‖u‖ ^ 2)
(hYmom : ∀ u, (∫ ω, inner ℝ u (Y ω) ^ 2 ∂μ) ≤ Λ * ‖u‖ ^ 2) :
(∫ ω, inner ℝ (X ω) (Y ω) ^ 2 ∂μ) ≤ M * Λ ^ 2 := by
by_cases hM : M = 0
· subst M
have hzeroX : X = 0 := funext fun _ => Subsingleton.elim _ _
have hzeroY : Y = 0 := funext fun _ => Subsingleton.elim _ _
simp [hzeroX, hzeroY]
have i0 : Fin (finrank ℝ (EuclideanSpace ℝ (Fin M))) :=
⟨0, by simpa using Nat.pos_of_ne_zero hM⟩
have hΛ : 0 ≤ Λ := by
have hi := hXmom ((stdOrthonormalBasis ℝ (EuclideanSpace ℝ (Fin M))) i0)
have hnonneg : 0 ≤ ∫ ω, inner ℝ
((stdOrthonormalBasis ℝ (EuclideanSpace ℝ (Fin M))) i0) (X ω) ^ 2 ∂μ :=
integral_nonneg (fun _ => sq_nonneg _)
simp only [OrthonormalBasis.norm_eq_one, one_pow, mul_one] at hi
exact hnonneg.trans hi
let νX := Measure.map X μ
let νY := Measure.map Y μ
have hXnorm : Integrable (fun x : EuclideanSpace ℝ (Fin M) => ‖x‖ ^ 2) νX := by
dsimp [νX]
apply (integrable_map_measure (continuous_norm.pow 2 |>.aestronglyMeasurable)
hX.aemeasurable).2
simpa [Function.comp_def] using hXL2.norm.integrable_sq
have hYnorm : Integrable (fun y : EuclideanSpace ℝ (Fin M) => ‖y‖ ^ 2) νY := by
dsimp [νY]
apply (integrable_map_measure (continuous_norm.pow 2 |>.aestronglyMeasurable)
hY.aemeasurable).2
simpa [Function.comp_def] using hYL2.norm.integrable_sq
have hcross : Integrable
(fun z : EuclideanSpace ℝ (Fin M) × EuclideanSpace ℝ (Fin M) =>
inner ℝ z.1 z.2 ^ 2) (νX.prod νY) := by
apply (hXnorm.mul_prod hYnorm).mono' (by fun_prop)
filter_upwards [] with z
have habs : |inner ℝ z.1 z.2| ≤ ‖z.1‖ * ‖z.2‖ := by
simpa only [Real.norm_eq_abs] using (norm_inner_le_norm (𝕜 := ℝ) z.1 z.2)
have hs := (sq_le_sq₀ (abs_nonneg (inner ℝ z.1 z.2))
(mul_nonneg (norm_nonneg z.1) (norm_nonneg z.2))).2 habs
rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)]
simpa only [sq_abs, mul_pow] using hs
have hjoint : Measure.map (fun ω => (X ω, Y ω)) μ = νX.prod νY := by
exact hind.map_prod_eq_prod_map_map hX.aemeasurable hY.aemeasurable
calc
(∫ ω, inner ℝ (X ω) (Y ω) ^ 2 ∂μ) =
∫ z, inner ℝ z.1 z.2 ^ 2 ∂(νX.prod νY) := by
rw [← hjoint, integral_map (hX.prodMk hY).aemeasurable (by fun_prop)]
_ = ∫ x, ∫ y, inner ℝ x y ^ 2 ∂νY ∂νX := integral_prod _ hcross
_ ≤ ∫ x, Λ * ‖x‖ ^ 2 ∂νX := by
apply integral_mono_ae
· exact hcross.integral_prod_left
· exact hXnorm.const_mul Λ
· filter_upwards [] with x
rw [integral_map hY.aemeasurable (by fun_prop)]
exact hYmom x
_ = Λ * ∫ x, ‖x‖ ^ 2 ∂νX := integral_const_mul _ _
_ ≤ Λ * (M * Λ) := by
gcongr
rw [integral_map hX.aemeasurable (by fun_prop)]
have hparse : (fun ω => ‖X ω‖ ^ 2) = fun ω => ∑ i,
inner ℝ ((stdOrthonormalBasis ℝ (EuclideanSpace ℝ (Fin M))) i) (X ω) ^ 2 := by
funext ω
exact (stdOrthonormalBasis ℝ (EuclideanSpace ℝ (Fin M))).sum_sq_inner_right (X ω) |>.symm
rw [hparse]
rw [integral_finsetSum _ (fun i _ => (hXL2.const_inner _).integrable_sq)]
calc
(∑ i : Fin (finrank ℝ (EuclideanSpace ℝ (Fin M))), ∫ ω, inner ℝ
((stdOrthonormalBasis ℝ (EuclideanSpace ℝ (Fin M))) i) (X ω) ^ 2 ∂μ) ≤
∑ _ : Fin (finrank ℝ (EuclideanSpace ℝ (Fin M))), Λ := by
gcongr with i
simpa using hXmom ((stdOrthonormalBasis ℝ (EuclideanSpace ℝ (Fin M))) i)
_ = M * Λ := by simp
_ = M * Λ ^ 2 := by ring
lemma projection_norm_tail_le_two reviewed
⚑ flagged
Causalean.Stat.Concentration
Let X be a square-integrable random vector in M-dimensional Euclidean space and let S be a linear subspace of dimension at most two. If, for a nonnegative number Λ, the second moment of the inner product of X with any fixed vector u is at most Λ times the squared norm of u, then for every positive threshold a, the probability that the orthogonal projection of X onto S has norm strictly greater than a is at most 2Λ / a².
Formal statement
hypotheses
Ω :
Type*
μ :
M :
S :
hS :
finrank ℝ S ≤ 2
X :
Ω → EuclideanSpace ℝ (Fin M)
Λ a :
ℝ
hΛ :
0 ≤ Λ
ha :
0 < a
hXL2 :
MemLp X 2 μ
hmom :
∀ u, (∫ ω, inner ℝ u (X ω) ^ 2 ∂μ) ≤ Λ * ‖u‖ ^ 2
conclusion
μ.real {ω | a < ‖S.orthogonalProjection (X ω)‖} ≤ 2 * Λ / a ^ 2
Proof (Lean source)
lemma projection_norm_tail_le_two {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
[IsProbabilityMeasure μ] {M : ℕ} [MeasurableSpace (EuclideanSpace ℝ (Fin M))]
[BorelSpace (EuclideanSpace ℝ (Fin M))]
(S : Submodule ℝ (EuclideanSpace ℝ (Fin M))) (hS : finrank ℝ S ≤ 2)
(X : Ω → EuclideanSpace ℝ (Fin M)) (Λ a : ℝ) (hΛ : 0 ≤ Λ) (ha : 0 < a)
(hXL2 : MemLp X 2 μ)
(hmom : ∀ u, (∫ ω, inner ℝ u (X ω) ^ 2 ∂μ) ≤ Λ * ‖u‖ ^ 2) :
μ.real {ω | a < ‖S.orthogonalProjection (X ω)‖} ≤ 2 * Λ / a ^ 2 := by
have ht := absolute_error_tail_le_second_moment μ
(fun ω => ‖S.orthogonalProjection (X ω)‖) a ha
(integrable_projection_norm_sq μ S X hXL2)
change (μ {ω | a < ‖S.orthogonalProjection (X ω)‖}).toReal ≤ 2 * Λ / a ^ 2
simpa only [abs_norm] using ht.trans (div_le_div_of_nonneg_right
(projection_second_moment_le_two μ S hS X Λ hΛ hXL2 hmom) (sq_nonneg a))
4 supporting declarations (lemmas, instances)
-
integrable_indep_inner_sqlemma — The squared inner product of two independent square-integrable finite-dimensional vectors is integrable. This statement assumes the hX condition, the hY condition, the hXL2 condition, the hYL2 condition, the hind condition. This is the stated conclusion.hypothesesΩ :Type*μ :M :X Y :Ω → EuclideanSpace ℝ (Fin M)hX :hY :hXL2 :MemLp X 2 μhYL2 :MemLp Y 2 μhind :IndepFun X Y μconclusionIntegrable (fun ω => inner ℝ (X ω) (Y ω) ^ 2) μProof (Lean source)
lemma integrable_indep_inner_sq {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] {M : ℕ} [MeasurableSpace (EuclideanSpace ℝ (Fin M))] [BorelSpace (EuclideanSpace ℝ (Fin M))] (X Y : Ω → EuclideanSpace ℝ (Fin M)) (hX : Measurable X) (hY : Measurable Y) (hXL2 : MemLp X 2 μ) (hYL2 : MemLp Y 2 μ) (hind : IndepFun X Y μ) : Integrable (fun ω => inner ℝ (X ω) (Y ω) ^ 2) μ := by let νX := Measure.map X μ let νY := Measure.map Y μ have hXnorm : Integrable (fun x : EuclideanSpace ℝ (Fin M) => ‖x‖ ^ 2) νX := by dsimp [νX] apply (integrable_map_measure (continuous_norm.pow 2 |>.aestronglyMeasurable) hX.aemeasurable).2 simpa [Function.comp_def] using hXL2.norm.integrable_sq have hYnorm : Integrable (fun y : EuclideanSpace ℝ (Fin M) => ‖y‖ ^ 2) νY := by dsimp [νY] apply (integrable_map_measure (continuous_norm.pow 2 |>.aestronglyMeasurable) hY.aemeasurable).2 simpa [Function.comp_def] using hYL2.norm.integrable_sq have hcross : Integrable (fun z : EuclideanSpace ℝ (Fin M) × EuclideanSpace ℝ (Fin M) => inner ℝ z.1 z.2 ^ 2) (νX.prod νY) := by apply (hXnorm.mul_prod hYnorm).mono' (by fun_prop) filter_upwards [] with z have habs : |inner ℝ z.1 z.2| ≤ ‖z.1‖ * ‖z.2‖ := by simpa only [Real.norm_eq_abs] using (norm_inner_le_norm (𝕜 := ℝ) z.1 z.2) have hs := (sq_le_sq₀ (abs_nonneg (inner ℝ z.1 z.2)) (mul_nonneg (norm_nonneg z.1) (norm_nonneg z.2))).2 habs rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)] simpa only [sq_abs, mul_pow] using hs have hjoint : Measure.map (fun ω => (X ω, Y ω)) μ = νX.prod νY := hind.map_prod_eq_prod_map_map hX.aemeasurable hY.aemeasurable rw [← hjoint] at hcross apply (integrable_map_measure (by fun_prop) (hX.prodMk hY).aemeasurable).1 at hcross simpa [Function.comp_def] using hcross -
indep_inner_tail_lelemma — Markov's inequality converts an independent cross-inner-product second-moment envelope into an absolute tail bound. This statement assumes the hX condition, the hY condition, the hXL2 condition, the hYL2 condition, the hind condition, the ha condition, the hmom condition. This is the stated conclusion.hypothesesΩ :Type*μ :M :X Y :Ω → EuclideanSpace ℝ (Fin M)Λ a :ℝhX :hY :hXL2 :MemLp X 2 μhYL2 :MemLp Y 2 μhind :IndepFun X Y μha :0 < ahmom :(∫ ω, inner ℝ (X ω) (Y ω) ^ 2 ∂μ) ≤ M * Λ ^ 2conclusionμ.real {ω | a < |inner ℝ (X ω) (Y ω)|} ≤ M * Λ ^ 2 / a ^ 2Proof (Lean source)
lemma indep_inner_tail_le {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] {M : ℕ} [MeasurableSpace (EuclideanSpace ℝ (Fin M))] [BorelSpace (EuclideanSpace ℝ (Fin M))] (X Y : Ω → EuclideanSpace ℝ (Fin M)) (Λ a : ℝ) (hX : Measurable X) (hY : Measurable Y) (hXL2 : MemLp X 2 μ) (hYL2 : MemLp Y 2 μ) (hind : IndepFun X Y μ) (ha : 0 < a) (hmom : (∫ ω, inner ℝ (X ω) (Y ω) ^ 2 ∂μ) ≤ M * Λ ^ 2) : μ.real {ω | a < |inner ℝ (X ω) (Y ω)|} ≤ M * Λ ^ 2 / a ^ 2 := by exact (absolute_error_tail_le_second_moment μ (fun ω => inner ℝ (X ω) (Y ω)) a ha (integrable_indep_inner_sq μ X Y hX hY hXL2 hYL2 hind)).trans (div_le_div_of_nonneg_right hmom (sq_nonneg a)) -
projection_second_moment_le_twolemma — Projection onto a subspace of dimension at most two has expected squared norm at most twice the common directional second-moment envelope. This statement assumes the hS condition, the hΛ condition, the hXL2 condition, the hmom condition. This is the stated conclusion.hypothesesΩ :Type*μ :M :S :hS :finrank ℝ S ≤ 2X :Ω → EuclideanSpace ℝ (Fin M)Λ :ℝhΛ :0 ≤ ΛhXL2 :MemLp X 2 μhmom :∀ u, (∫ ω, inner ℝ u (X ω) ^ 2 ∂μ) ≤ Λ * ‖u‖ ^ 2conclusion(∫ ω, ‖S.orthogonalProjection (X ω)‖ ^ 2 ∂μ) ≤ 2 * ΛProof (Lean source)
lemma projection_second_moment_le_two {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] {M : ℕ} [MeasurableSpace (EuclideanSpace ℝ (Fin M))] [BorelSpace (EuclideanSpace ℝ (Fin M))] (S : Submodule ℝ (EuclideanSpace ℝ (Fin M))) (hS : finrank ℝ S ≤ 2) (X : Ω → EuclideanSpace ℝ (Fin M)) (Λ : ℝ) (hΛ : 0 ≤ Λ) (hXL2 : MemLp X 2 μ) (hmom : ∀ u, (∫ ω, inner ℝ u (X ω) ^ 2 ∂μ) ≤ Λ * ‖u‖ ^ 2) : (∫ ω, ‖S.orthogonalProjection (X ω)‖ ^ 2 ∂μ) ≤ 2 * Λ := by let b := stdOrthonormalBasis ℝ S have heq : (fun ω => ‖S.orthogonalProjection (X ω)‖ ^ 2) = fun ω => ∑ i, inner ℝ ((b i : S)) (S.orthogonalProjection (X ω)) ^ 2 := by funext ω exact (b.sum_sq_inner_right (S.orthogonalProjection (X ω))).symm rw [heq] have hi (i : Fin (finrank ℝ S)) : Integrable (fun ω => inner ℝ ((b i : S)) (S.orthogonalProjection (X ω)) ^ 2) μ := by have he : (fun ω => inner ℝ ((b i : S)) (S.orthogonalProjection (X ω)) ^ 2) = fun ω => inner ℝ (b i : EuclideanSpace ℝ (Fin M)) (X ω) ^ 2 := by funext ω rw [S.inner_orthogonalProjection_eq_of_mem_left] rw [he] exact (hXL2.const_inner _).integrable_sq rw [integral_finsetSum _ (fun i _ => hi i)] calc (∑ i : Fin (finrank ℝ S), ∫ ω, inner ℝ ((b i : S)) (S.orthogonalProjection (X ω)) ^ 2 ∂μ) ≤ ∑ _ : Fin (finrank ℝ S), Λ := by gcongr with i rw [show (fun ω => inner ℝ ((b i : S)) (S.orthogonalProjection (X ω)) ^ 2) = fun ω => inner ℝ (b i : EuclideanSpace ℝ (Fin M)) (X ω) ^ 2 by funext ω rw [S.inner_orthogonalProjection_eq_of_mem_left]] have h := hmom (b i : EuclideanSpace ℝ (Fin M)) rw [show ‖(b i : EuclideanSpace ℝ (Fin M))‖ = ‖b i‖ from rfl, OrthonormalBasis.norm_eq_one, one_pow, mul_one] at h exact h _ = finrank ℝ S * Λ := by simp _ ≤ 2 * Λ := by exact mul_le_mul_of_nonneg_right (by exact_mod_cast hS) hΛ -
integrable_projection_norm_sqlemma — The squared norm of a finite-dimensional orthogonal projection is integrable whenever the original vector is square integrable. This statement assumes the hXL2 condition. This is the stated conclusion.hypothesesconclusionIntegrable (fun ω => ‖S.orthogonalProjection (X ω)‖ ^ 2) μProof (Lean source)
lemma integrable_projection_norm_sq {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) {M : ℕ} [MeasurableSpace (EuclideanSpace ℝ (Fin M))] [BorelSpace (EuclideanSpace ℝ (Fin M))] (S : Submodule ℝ (EuclideanSpace ℝ (Fin M))) (X : Ω → EuclideanSpace ℝ (Fin M)) (hXL2 : MemLp X 2 μ) : Integrable (fun ω => ‖S.orthogonalProjection (X ω)‖ ^ 2) μ := by let b := stdOrthonormalBasis ℝ S have heq : (fun ω => ‖S.orthogonalProjection (X ω)‖ ^ 2) = fun ω => ∑ i, inner ℝ ((b i : S)) (S.orthogonalProjection (X ω)) ^ 2 := by funext ω exact (b.sum_sq_inner_right (S.orthogonalProjection (X ω))).symm rw [heq] apply integrable_finsetSum intro i hi have he : (fun ω => inner ℝ ((b i : S)) (S.orthogonalProjection (X ω)) ^ 2) = fun ω => inner ℝ (b i : EuclideanSpace ℝ (Fin M)) (X ω) ^ 2 := by funext ω rw [S.inner_orthogonalProjection_eq_of_mem_left] rw [he] exact (hXL2.const_inner _).integrable_sq