Type conversion

def EuclideanBridge.euclideanToFun {d : ℕ} : EuclideanSpace ℝ (Fin d) → Fin d → ℝ

Convert from EuclideanSpace to Fin d → ℝ.

def EuclideanBridge.funToEuclidean {d : ℕ} : (Fin d → ℝ) → EuclideanSpace ℝ (Fin d)

Convert from Fin d → ℝ to EuclideanSpace.

@[simp]

theorem EuclideanBridge.euclideanToFun_funToEuclidean {d : ℕ} (v : Fin d → ℝ) : euclideanToFun (funToEuclidean v) = v

@[simp]

theorem EuclideanBridge.funToEuclidean_euclideanToFun {d : ℕ} (v : EuclideanSpace ℝ (Fin d)) : funToEuclidean (euclideanToFun v) = v

@[simp]

theorem EuclideanBridge.euclideanToFun_apply {d : ℕ} (v : EuclideanSpace ℝ (Fin d)) (i : Fin d) : euclideanToFun v i = v.ofLp i

Pointwise access is preserved by euclideanToFun.

@[simp]

theorem EuclideanBridge.funToEuclidean_apply {d : ℕ} (v : Fin d → ℝ) (i : Fin d) : (funToEuclidean v).ofLp i = v i

Pointwise access is preserved by funToEuclidean.

Norm relationships

theorem EuclideanBridge.sup_norm_le_euclidean_norm {d : ℕ} (u : EuclideanSpace ℝ (Fin d)) : ‖euclideanToFun u‖ ≤ ‖u‖

The sup norm on the underlying Fin d → ℝ is at most the L2 norm. This is the key inequality for the SubGaussianVec bridge.

theorem EuclideanBridge.euclidean_norm_le_sqrt_d_mul_sup_norm {d : ℕ} (v : Fin d → ℝ) : ‖funToEuclidean v‖ ≤ √↑d * ‖v‖

The L2 norm is at most √d times the sup norm.

Measurability

theorem EuclideanBridge.measurable_euclideanToFun {d : ℕ} : Measurable euclideanToFun

euclideanToFun is measurable.

theorem EuclideanBridge.measurable_funToEuclidean {d : ℕ} : Measurable funToEuclidean

funToEuclidean is measurable.

SubGaussianVec bridges

theorem EuclideanBridge.subGaussianVec_euclidean_of_fun {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → EuclideanSpace ℝ (Fin d)} {σsq : ℝ} (hσ : 0 ≤ σsq) (h : Rigollet.Chapter4.Thm_4_6.IsSubGaussianVec μ (fun (ω : Ω) (j : Fin d) => (X ω).ofLp j) σsq) : Cor49.IsSubGaussianVec μ X σsq

If the sub-Gaussian condition holds for Thm_4_6's IsSubGaussianVec (which now uses L2-norm unit vectors), then it holds for Cor_4_9's IsSubGaussianVec. Both use L2-norm test vectors, so the bridge is direct.

theorem EuclideanBridge.subGaussianVec_fun_of_euclidean_scaled {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → EuclideanSpace ℝ (Fin d)} {σsq : ℝ} (hσ : 0 ≤ σsq) (h : Cor49.IsSubGaussianVec μ X σsq) (hAEM : AEMeasurable X μ) : Rigollet.Chapter4.Thm_4_6.IsSubGaussianVec μ (fun (ω : Ω) (j : Fin d) => (X ω).ofLp j) (↑d * σsq)

Reverse direction: if the sub-Gaussian condition holds for all L2-norm unit vectors (Cor_4_9's definition), then Thm_4_6's IsSubGaussianVec also holds with variance proxy scaled by d. Both now use L2 norm test vectors, so the core bound is direct; the scaling by d provides a monotone upper bound.

Composition bridge

theorem EuclideanBridge.euclideanToFun_comp_eq {d : ℕ} {Y : Type u_1} (f : Y → EuclideanSpace ℝ (Fin d)) (y : Y) (j : Fin d) : euclideanToFun (f y) j = (f y).ofLp j

Composing a function to EuclideanSpace with euclideanToFun extracts the same pointwise function.

theorem EuclideanBridge.funToEuclidean_comp_eq {d : ℕ} {Y : Type u_1} (f : Y → Fin d → ℝ) (y : Y) (j : Fin d) : (funToEuclidean (f y)).ofLp j = f y j

Composing a function to Fin d → ℝ with funToEuclidean gives the same pointwise function.