Bridge between EuclideanSpace and dotProduct

This file provides helper lemmas bridging the covering number theorem (lemma_1_18_covering_number_euclidean_ball, proved in EuclideanSpace ℝ (Fin d)) to a dotProduct-based formulation on Fin d → ℝ.

Main results

• dotProduct_eq_euclideanNorm_sq: dotProduct v v = ‖(WithLp.equiv 2 _).symm v‖²
• epsilon_net_dotProduct_of_euclidean: existence of an ε-net with dotProduct-based bounds

theorem dotProduct_eq_euclideanNorm_sq {d : ℕ} (v : Fin d → ℝ) : v ⬝ᵥ v = ‖(WithLp.equiv 2 (Fin d → ℝ)).symm v‖ ^ 2

Key bridge: dotProduct v v equals the squared L2 norm in EuclideanSpace.

theorem epsilon_net_dotProduct_of_euclidean {d : ℕ} (hd : 0 < d) : ∃ (N : Finset (Fin d → ℝ)), N.card ≤ 6 ^ d ∧ (∀ z ∈ N, z ⬝ᵥ z ≤ 1) ∧ ∀ (v : Fin d → ℝ), v ⬝ᵥ v ≤ 1 → ∃ z ∈ N, (v - z) ⬝ᵥ (v - z) ≤ 1 / 4

Bridge: IsEpsilonNet in EuclideanSpace gives a dotProduct-based covering.