Bridge lemmas: EuclideanSpace ↔ Fin n → ℝ with dotProduct

This file provides bridge lemmas connecting the EuclideanSpace ℝ (Fin p) / @inner formulation used in theorem_1_19_tail_bound to the Fin n → ℝ / dotProduct formulation used in single_support_thm119_bound.

Main results

• dotProduct_eq_inner_euclidean — dotProduct v w = ⟪toEuc v, toEuc w⟫
• euclidean_norm_le_one_iff — ‖toEuc v‖ ≤ 1 ↔ dotProduct v v ≤ 1
• subgaussian_inner_from_dotProduct — bridge sub-Gaussianity from coordinate to inner product
• theorem_1_19_tail_bound_vec — Theorem 1.19 restated for Fin p → ℝ and dotProduct

Basic type equivalence bridges

@[reducible, inline]

abbrev toEuc (n : ℕ) : (Fin n → ℝ) → EuclideanSpace ℝ (Fin n)

Abbreviation for the embedding Fin n → ℝ ↪ EuclideanSpace ℝ (Fin n).

@[reducible, inline]

abbrev fromEuc (n : ℕ) : EuclideanSpace ℝ (Fin n) → Fin n → ℝ

Abbreviation for the projection EuclideanSpace ℝ (Fin n) → Fin n → ℝ.

theorem dotProduct_nonneg_self {n : ℕ} (v : Fin n → ℝ) : 0 ≤ v ⬝ᵥ v

dotProduct v v ≥ 0 for any real vector.

Inner product bridge

theorem dotProduct_eq_inner_euclidean {n : ℕ} (v w : Fin n → ℝ) : v ⬝ᵥ w = inner ℝ (toEuc n v) (toEuc n w)

dotProduct v w equals the EuclideanSpace inner product of the corresponding vectors. This is the fundamental bridge between the Matrix/dotProduct world and the EuclideanSpace/inner world.

Norm bridge

theorem euclidean_norm_eq_sqrt_dotProduct {n : ℕ} (v : Fin n → ℝ) : ‖toEuc n v‖ = √(v ⬝ᵥ v)

The EuclideanSpace norm of toEuc v equals √(dotProduct v v).

theorem euclidean_norm_le_one_iff {n : ℕ} (v : Fin n → ℝ) : ‖toEuc n v‖ ≤ 1 ↔ v ⬝ᵥ v ≤ 1

‖toEuc v‖ ≤ 1 in EuclideanSpace iff dotProduct v v ≤ 1. This bridges the unit ball conditions between the two formulations.

Function conversion lemmas

theorem inner_toEuc_eq_dotProduct {Ω : Sort u_1} {n : ℕ} (a : Fin n → ℝ) (Z : Ω → Fin n → ℝ) (ω : Ω) : inner ℝ (toEuc n a) (toEuc n (Z ω)) = a ⬝ᵥ Z ω

Converting a random vector via toEuc preserves the pointwise inner product.

Sub-Gaussianity bridge

theorem subgaussian_inner_from_dotProduct {p : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Z : Ω → Fin p → ℝ} {σsq : ℝ} (hsg : ∀ (a : Fin p → ℝ), a ⬝ᵥ a ≤ 1 → IsSubGaussian (fun (ω : Ω) => a ⬝ᵥ Z ω) σsq μ) (θ : EuclideanSpace ℝ (Fin p)) (hθ : ‖θ‖ ≤ 1) : IsSubGaussian (fun (ω : Ω) => inner ℝ θ (toEuc p (Z ω))) σsq μ

If dotProduct a (Z ω) is IsSubGaussian for all unit vectors a (in the ℓ₂ sense), then @inner ℝ _ _ θ (toEuc ∘ Z) is IsSubGaussian for all unit vectors θ in EuclideanSpace.

theorem subgaussian_inner_from_coord {n : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {ε : Ω → Fin n → ℝ} {σsq : ℝ} (hσ : 0 ≤ σsq) (hε : ∀ (i : Fin n), IsSubGaussian (fun (ω : Ω) => ε ω i) σsq μ) (hε_indep : ProbabilityTheory.iIndepFun (fun (i : Fin n) (ω : Ω) => ε ω i) μ) (hε_meas : ∀ (i : Fin n), Measurable fun (ω : Ω) => ε ω i) (a : EuclideanSpace ℝ (Fin n)) (ha : ‖a‖ ≤ 1) : IsSubGaussian (fun (ω : Ω) => inner ℝ a (toEuc n (ε ω))) σsq μ

If each coordinate ε_i is IsSubGaussian(σ²) and the coordinates are independent, then for any unit vector a in EuclideanSpace, ⟨a, ε⟩ is IsSubGaussian(σ²).

This composes theorem_1_6_subgaussian_vector (coordinate independence → linear combination sub-Gaussianity) with the dotProduct ↔ inner bridge to produce the hypothesis needed by theorem_1_19_tail_bound.

Theorem 1.19 tail bound for Fin p → ℝ and dotProduct

theorem theorem_1_19_tail_bound_vec {p : ℕ} (hp : 0 < p) {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {Z : Ω → Fin p → ℝ} {σsq : ℝ} (hσ : 0 < σsq) (hsg : ∀ (a : Fin p → ℝ), a ⬝ᵥ a ≤ 1 → IsSubGaussian (fun (ω : Ω) => a ⬝ᵥ Z ω) σsq μ) (t : ℝ) (ht : 0 < t) : μ {ω : Ω | ∃ (θ : Fin p → ℝ), θ ⬝ᵥ θ ≤ 1 ∧ θ ⬝ᵥ Z ω > t} ≤ ENNReal.ofReal (6 ^ p * Real.exp (-(t ^ 2 / (8 * σsq))))

Theorem 1.19 tail bound (vector version). A version of theorem_1_19_tail_bound stated for Fin p → ℝ with dotProduct instead of EuclideanSpace ℝ (Fin p) with @inner.

The sub-Gaussianity condition uses the ℓ₂ unit ball: dotProduct a a ≤ 1.

This is the version that can be directly applied to the noise vector ε in the proof of Theorem 2.14, where inner products are expressed as dotProduct ε (X.mulVec v).