Gram matrix rigidity

Two families of vectors in inner product spaces over 𝕜 = ℝ, ℂ with equal pairwise inner products are related by a linear isometry. In finite dimension this upgrades to a linear isometry equivalence of the ambient space, and the hypothesis can be packaged as equality of Matrix.gram matrices.

The engine is a general fact about a pair of linear maps, an isometric refinement of the first isomorphism theorem:

• LinearMap.ker_eq_ker_of_inner_eq: linear maps S, T (out of a common module, into two inner product spaces) with equal pullback inner products ⟪S x, S y⟫ = ⟪T x, T y⟫ have equal kernels, since S x = 0 iff ⟪S x, S x⟫ = 0.
• LinearMap.rangeEquivOfInnerEq: consequently S x ↦ T x descends to a linear isometry equivalence range S ≃ₗᵢ range T: both ranges are canonically isomorphic to the coimage M ⧸ ker S = M ⧸ ker T by the first isomorphism theorem, and the hypothesis says exactly that the two induced inner products on the coimage agree.

Everything else is specialization. Applying it to the two linear-combination maps Finsupp.linearCombination 𝕜 φ and Finsupp.linearCombination 𝕜 ψ of families φ, ψ with equal pairwise inner products (their pullback inner products then agree by sesquilinearity, inner_linearCombination_eq_of_inner_eq) turns "equal Gram data" into an isometry of spans:

• linearIsometryEquivSpanOfInnerEq: a linear isometry equivalence span 𝕜 (range φ) ≃ₗᵢ span 𝕜 (range ψ) sending each φ i to ψ i. No finiteness is assumed, and the ambient spaces may differ.
• exists_linearIsometryEquiv_map_eq_of_inner_eq: in a finite-dimensional ambient space this extends (by LinearIsometry.extend) to a linear isometry equivalence of the whole space.
• TauCeti.Matrix.gram_eq_gram_iff_exists_linearIsometryEquiv_map_eq: the same statement packaged as a characterization of Matrix.gram equality.

References

• R. A. Horn and C. R. Johnson, Matrix Analysis, 2nd ed., Cambridge University Press, 2013 — Gram matrices and factorization up to a unitary factor.
• T.-Y. Chien and S. Waldron, A Characterization of Projective Unitary Equivalence of Finite Frames and Applications, SIAM J. Discrete Math. 30 (2016), no. 2, 976–994, arXiv:1312.5393 — the frame-theoretic form: finite frames are unitarily equivalent iff their Gram matrices coincide.

The isometric first isomorphism theorem

theorem TauCeti.LinearMap.ker_eq_ker_of_inner_eq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {M : Type u_5} [AddCommGroup M] [Module 𝕜 M] (S : M →ₗ[𝕜] E) (T : M →ₗ[𝕜] F) (h : ∀ (x y : M), inner 𝕜 (S x) (S y) = inner 𝕜 (T x) (T y)) : S.ker = T.ker

Linear maps with equal pullback inner products have equal kernels: S x = 0 iff ⟪S x, S x⟫ = 0 iff ⟪T x, T x⟫ = 0 iff T x = 0.

noncomputable def TauCeti.LinearMap.rangeEquivOfInnerEq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {M : Type u_5} [AddCommGroup M] [Module 𝕜 M] (S : M →ₗ[𝕜] E) (T : M →ₗ[𝕜] F) (h : ∀ (x y : M), inner 𝕜 (S x) (S y) = inner 𝕜 (T x) (T y)) : ↥S.range ≃ₗᵢ[𝕜] ↥T.range

Isometric first isomorphism theorem. Two linear maps S, T out of a common module with equal pullback inner products, ⟪S x, S y⟫ = ⟪T x, T y⟫, have canonically isometric ranges, by S x ↦ T x. This is well defined because both ranges are first-isomorphism-theorem images of the common coimage M ⧸ ker S = M ⧸ ker T (ker_eq_ker_of_inner_eq), and isometric because the hypothesis is precisely the statement that the two inner products induced on the coimage agree.

Equations

• TauCeti.LinearMap.rangeEquivOfInnerEq S T h = (S.quotKerEquivRange.symm.trans ((S.ker.quotEquivOfEq T.ker ⋯).trans T.quotKerEquivRange)).isometryOfInner ⋯

@[simp]

theorem TauCeti.LinearMap.rangeEquivOfInnerEq_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {M : Type u_5} [AddCommGroup M] [Module 𝕜 M] (S : M →ₗ[𝕜] E) (T : M →ₗ[𝕜] F) (h : ∀ (x y : M), inner 𝕜 (S x) (S y) = inner 𝕜 (T x) (T y)) (x : M) (hx : S x ∈ S.range) : ↑((rangeEquivOfInnerEq S T h) ⟨S x, hx⟩) = T x

The equivalence built from equal Gram data sends φ i to ψ i; this is the property that characterises it, the construction itself going through linear combinations.

Families with equal pairwise inner products

Provenance

• Original repository: Davis--Kahan/DKPS formalization (Kitware, Inc.).
• Original module: ForMathlib.Analysis.InnerProductSpace.GramMatrix, moved to ForTauCeti in the Wave-1 staging migration; introduced at Davis--Kahan commit 56f7495.
• Extraction class: moved. The Wave-1 migration renamed the namespace ForMathlib to TauCeti; declaration names and proofs are unchanged.
• Original authors / copyright: Jon Crall, Claude Fable 5; Copyright (c) 2026 Kitware, Inc.; Apache 2.0.
• Spectra influence: none — this module imports only Mathlib and sibling ForTauCeti staging modules.

theorem TauCeti.inner_linearCombination_eq_of_inner_eq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {φ : ι → E} {ψ : ι → F} (h : ∀ (i j : ι), inner 𝕜 (φ i) (φ j) = inner 𝕜 (ψ i) (ψ j)) (c c' : ι →₀ 𝕜) : inner 𝕜 ((Finsupp.linearCombination 𝕜 φ) c) ((Finsupp.linearCombination 𝕜 φ) c') = inner 𝕜 ((Finsupp.linearCombination 𝕜 ψ) c) ((Finsupp.linearCombination 𝕜 ψ) c')

For families φ, ψ with equal pairwise inner products, the maps of linear combinations ∑ cᵢ • φ i and ∑ cᵢ • ψ i have equal pairwise inner products.

theorem TauCeti.ker_linearCombination_eq_of_inner_eq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {φ : ι → E} {ψ : ι → F} (h : ∀ (i j : ι), inner 𝕜 (φ i) (φ j) = inner 𝕜 (ψ i) (ψ j)) : (Finsupp.linearCombination 𝕜 φ).ker = (Finsupp.linearCombination 𝕜 ψ).ker

Families with equal pairwise inner products have linear-combination maps with equal kernels: ∑ cᵢ • φ i = 0 ↔ ∑ cᵢ • ψ i = 0.

noncomputable def TauCeti.linearIsometryEquivSpanOfInnerEq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (φ : ι → E) (ψ : ι → F) (h : ∀ (i j : ι), inner 𝕜 (φ i) (φ j) = inner 𝕜 (ψ i) (ψ j)) : ↥(Submodule.span 𝕜 (Set.range φ)) ≃ₗᵢ[𝕜] ↥(Submodule.span 𝕜 (Set.range ψ))

A linear isometry equivalence span 𝕜 (range φ) ≃ₗᵢ span 𝕜 (range ψ) sending each φ i to ψ i, when the families φ, ψ (in possibly different inner product spaces over 𝕜) have equal pairwise inner products. It is the isometric first isomorphism theorem LinearMap.rangeEquivOfInnerEq applied to the two linear-combination maps, whose ranges are the spans. No finiteness is required, and the ambient spaces need not coincide.

Such an isometry is determined on the spanning family φ (LinearMap.eqOn_span), hence unique; this uniqueness is not separately formalized here.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.linearIsometryEquivSpanOfInnerEq_apply_linearCombination {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (φ : ι → E) (ψ : ι → F) (h : ∀ (i j : ι), inner 𝕜 (φ i) (φ j) = inner 𝕜 (ψ i) (ψ j)) (c : ι →₀ 𝕜) (hc : (Finsupp.linearCombination 𝕜 φ) c ∈ Submodule.span 𝕜 (Set.range φ)) : ↑((linearIsometryEquivSpanOfInnerEq φ ψ h) ⟨(Finsupp.linearCombination 𝕜 φ) c, hc⟩) = (Finsupp.linearCombination 𝕜 ψ) c

linearIsometryEquivSpanOfInnerEq computes on linear combinations: it sends ∑ cᵢ • φ i to ∑ cᵢ • ψ i.

@[simp]

theorem TauCeti.linearIsometryEquivSpanOfInnerEq_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (φ : ι → E) (ψ : ι → F) (h : ∀ (i j : ι), inner 𝕜 (φ i) (φ j) = inner 𝕜 (ψ i) (ψ j)) (i : ι) (hi : φ i ∈ Submodule.span 𝕜 (Set.range φ)) : ↑((linearIsometryEquivSpanOfInnerEq φ ψ h) ⟨φ i, hi⟩) = ψ i

linearIsometryEquivSpanOfInnerEq sends each generator φ i to ψ i: the c = Finsupp.single i 1 case of linearIsometryEquivSpanOfInnerEq_apply_linearCombination.

theorem TauCeti.exists_linearIsometryEquiv_map_eq_of_inner_eq {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {φ ψ : ι → E} (h : ∀ (i j : ι), inner 𝕜 (φ i) (φ j) = inner 𝕜 (ψ i) (ψ j)) : ∃ (W : E ≃ₗᵢ[𝕜] E), ∀ (i : ι), W (φ i) = ψ i

If two families φ ψ : ι → E in a finite-dimensional inner product space have equal pairwise inner products, then there is a linear isometry equivalence W of E with W (φ i) = ψ i for every i. The span-to-span equivalence linearIsometryEquivSpanOfInnerEq is extended to E by LinearIsometry.extend and bundled as an equivalence by finite dimensionality.

theorem TauCeti.exists_rigidMotion_of_dist_eq {F : Type u_5} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] {ι : Type u_6} [Nonempty ι] {φ ψ : ι → F} (h : ∀ (i j : ι), ‖φ i - φ j‖ = ‖ψ i - ψ j‖) : ∃ (W : F ≃ₗᵢ[ℝ] F) (b : F), ∀ (i : ι), ψ i = W (φ i) + b

Rigid-motion rigidity. Two families in a finite-dimensional real inner product space with equal pairwise distances differ by a rigid motion: there is a linear isometry equivalence W and a translation b with ψ i = W (φ i) + b for every i.

This is the affine companion of exists_linearIsometryEquiv_map_eq_of_inner_eq, which needs equal inner products. Recentring at a base index turns equal distances into equal inner products by polarisation, and the linear statement then supplies W.

It is the classical fact underlying multidimensional scaling: a configuration is determined by its pairwise distances only up to a rigid motion, so a distance-based embedding can be compared with a target configuration only after alignment.

theorem TauCeti.eventually_exists_rigidMotion_dist_lt {F : Type u_5} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] {ι : Type u_6} [Finite ι] [Nonempty ι] {φ : ℕ → ι → F} {ψ : ι → F} (h : ∀ (i j : ι), Filter.Tendsto (fun (u : ℕ) => ‖φ u i - φ u j‖) Filter.atTop (nhds ‖ψ i - ψ j‖)) (ε : ℝ) : ε > 0 → ∀ᶠ (u : ℕ) in Filter.atTop, ∃ (W : F ≃ₗᵢ[ℝ] F) (b : F), ∀ (i : ι), ‖W (φ u i) + b - ψ i‖ < ε

Approximate rigid-motion rigidity. If the pairwise distances of a sequence of finite configurations converge to those of a target, then eventually each configuration is carried arbitrarily close to the target by some rigid motion.

This is the asymptotic form of exists_rigidMotion_of_dist_eq, and it is what a distance-based consistency statement needs: multidimensional scaling determines a configuration only up to a rigid motion, so convergence of the estimates can be asserted only after alignment.

The proof is a compactness argument and uses no spectral hypothesis. Recentring at a base index leaves all distances unchanged and bounds the configurations; a bounded sequence in a finite-dimensional space has a convergent subsequence; the limit has exactly the target's pairwise distances; and the exact statement then supplies a rigid motion, which by continuity serves the whole tail.

theorem TauCeti.exists_delta_forall_exists_rigidMotion {F : Type u_5} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] {ι : Type u_6} [Finite ι] [Nonempty ι] (D : ℝ) {ε : ℝ} (hε : 0 < ε) : ∃ δ > 0, ∀ (φ ψ : ι → F), (∀ (i j : ι), ‖ψ i - ψ j‖ ≤ D) → (∀ (i j : ι), |‖φ i - φ j‖ - ‖ψ i - ψ j‖| ≤ δ) → ∃ (W : F ≃ₗᵢ[ℝ] F) (b : F), ∀ (i : ι), ‖W (φ i) + b - ψ i‖ ≤ ε

Uniform approximate rigid-motion rigidity. For a fixed finite index type, a fixed tolerance ε and a fixed bound D on the diameter of the target, one δ > 0 serves every pair of configurations: if the target has diameter at most D and the pairwise distances agree to within δ, then some rigid motion carries the estimate to within ε of the target.

eventually_exists_rigidMotion_dist_lt is the sequential form of the same fact; the uniform form is what a random target needs, where a modulus that depends on the sample is of no use. The diameter bound cannot be dropped: the hypothesis and conclusion both scale linearly under a simultaneous rescaling of the two configurations, so δ must be allowed to depend on the size of the target.

The proof is again pure compactness and uses no spectral hypothesis: a counterexample sequence, recentred at a base index, is bounded in the finite-dimensional space of configurations, so both the estimates and the targets subconverge; the two limits have equal pairwise distances; exists_rigidMotion_of_dist_eq aligns them exactly; and that one rigid motion then serves a whole tail of the counterexample sequence.

Alignment error and the aligned configuration

Multidimensional scaling recovers a configuration only up to a rigid motion, so the quantity a distance-based consistency statement can control is not the uniform distance to the target but the least uniform distance achievable after moving the estimate by a rigid motion. That is alignmentError, and alignedConfig is an estimate that very nearly attains it.

def TauCeti.rigidTolerances {F : Type u_5} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type u_6} (ψ φ : ι → F) : Set ℝ

The uniform tolerances achievable by carrying φ onto ψ with a rigid motion.

Equations

• TauCeti.rigidTolerances ψ φ = {r : ℝ | ∃ (W : F ≃ₗᵢ[ℝ] F) (b : F), ∀ (i : ι), ‖W (φ i) + b - ψ i‖ ≤ r}

noncomputable def TauCeti.alignmentError {F : Type u_5} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type u_6} (ψ φ : ι → F) : ℝ

The alignment error of a configuration φ against a target ψ: the least uniform distance to ψ achievable by moving φ with a rigid motion. It vanishes exactly when the two configurations are congruent, and by exists_delta_forall_exists_rigidMotion it is small whenever the pairwise distances are close and the target is not too large.

Equations

• TauCeti.alignmentError ψ φ = sInf (TauCeti.rigidTolerances ψ φ)

theorem TauCeti.rigidTolerances_nonempty {F : Type u_5} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type u_6} [Finite ι] [Nonempty ι] (ψ φ : ι → F) : (rigidTolerances ψ φ).Nonempty

The set of rigidity tolerances is nonempty.

theorem TauCeti.bddBelow_rigidTolerances {F : Type u_5} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type u_6} [Nonempty ι] (ψ φ : ι → F) : BddBelow (rigidTolerances ψ φ)

The set of rigidity tolerances is bounded below, so its infimum exists.

theorem TauCeti.alignmentError_nonneg {F : Type u_5} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type u_6} [Nonempty ι] (ψ φ : ι → F) : 0 ≤ alignmentError ψ φ

The alignment error is nonnegative.

theorem TauCeti.alignmentError_le {F : Type u_5} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type u_6} [Nonempty ι] {ψ φ : ι → F} {r : ℝ} (h : ∃ (W : F ≃ₗᵢ[ℝ] F) (b : F), ∀ (i : ι), ‖W (φ i) + b - ψ i‖ ≤ r) : alignmentError ψ φ ≤ r

Any rigid motion achieving a uniform tolerance bounds the alignment error.

theorem TauCeti.exists_rigidMotion_norm_le_alignmentError_add {F : Type u_5} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type u_6} [Finite ι] [Nonempty ι] (ψ φ : ι → F) {t : ℝ} (ht : 0 < t) : ∃ (W : F ≃ₗᵢ[ℝ] F) (b : F), ∀ (i : ι), ‖W (φ i) + b - ψ i‖ ≤ alignmentError ψ φ + t

The alignment error is approached: for every positive slack some rigid motion achieves it.

noncomputable def TauCeti.alignedConfig {F : Type u_5} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type u_6} (ψ φ : ι → F) (t : ℝ) : ι → F

The aligned configuration: φ moved by a rigid motion that comes within slack t of the alignment error, and φ itself in the degenerate case where no such motion exists (which exists_rigidMotion_norm_le_alignmentError_add rules out for 0 < t).

This is the object a consistency statement can compare with the target without quantifying the alignment inside the probability: the motion is chosen sample by sample, so the statement "the aligned estimate converges to the target" needs no external alignment sequence.

Equations

• TauCeti.alignedConfig ψ φ t = if h : ∃ (W : F ≃ₗᵢ[ℝ] F) (b : F), ∀ (i : ι), ‖W (φ i) + b - ψ i‖ ≤ TauCeti.alignmentError ψ φ + t then fun (i : ι) => h.choose (φ i) + ⋯.choose else φ

theorem TauCeti.norm_alignedConfig_sub_le {F : Type u_5} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type u_6} [Finite ι] [Nonempty ι] (ψ φ : ι → F) {t : ℝ} (ht : 0 < t) (i : ι) : ‖alignedConfig ψ φ t i - ψ i‖ ≤ alignmentError ψ φ + t

The defining property of alignedConfig.

theorem TauCeti.dist_alignedConfig_le {F : Type u_5} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {ι : Type u_6} [Finite ι] [Nonempty ι] (ψ φ : ι → F) {t : ℝ} (ht : 0 < t) (i : ι) : dist (alignedConfig ψ φ t i) (ψ i) ≤ alignmentError ψ φ + t

The dist form of norm_alignedConfig_sub_le.

theorem TauCeti.exists_delta_alignmentError_le {F : Type u_5} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] {ι : Type u_6} [Finite ι] [Nonempty ι] (D : ℝ) {ε : ℝ} (hε : 0 < ε) : ∃ δ > 0, ∀ (φ ψ : ι → F), (∀ (i j : ι), ‖ψ i - ψ j‖ ≤ D) → (∀ (i j : ι), |‖φ i - φ j‖ - ‖ψ i - ψ j‖| ≤ δ) → alignmentError ψ φ ≤ ε

Uniform approximate rigidity, alignment-error form. One δ serves every pair: pairwise distances within δ of a target of diameter at most D force the alignment error below ε.

This is the shape a convergence-in-probability argument consumes, because δ does not depend on the sample.

theorem TauCeti.Matrix.gram_eq_gram_iff_exists_linearIsometryEquiv_map_eq {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {φ ψ : ι → E} : Matrix.gram 𝕜 φ = Matrix.gram 𝕜 ψ ↔ ∃ (W : E ≃ₗᵢ[𝕜] E), ∀ (i : ι), W (φ i) = ψ i

Gram rigidity, Matrix.gram form. Two families of vectors in a finite-dimensional inner product space have equal Gram matrices if and only if a linear isometry equivalence of the ambient space maps one family to the other.

noncomputable def TauCeti.familyMap {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {d : ℕ} (v : Fin d → E) : EuclideanSpace 𝕜 (Fin d) →ₗ[𝕜] E

The linear map EuclideanSpace 𝕜 (Fin d) →ₗ[𝕜] E sending the j-th standard basis vector to v j (extended linearly): x ↦ ∑ j, x j • v j.

Equations

• TauCeti.familyMap v = Fintype.linearCombination 𝕜 v ∘ₗ ↑(WithLp.linearEquiv 2 𝕜 (Fin d → 𝕜))

@[simp]

theorem TauCeti.familyMap_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {d : ℕ} (v : Fin d → E) (x : EuclideanSpace 𝕜 (Fin d)) : (familyMap v) x = ∑ i : Fin d, x.ofLp i • v i

The family map, unfolded to its expansion in the family.

theorem TauCeti.familyMap_inner_map_map {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {d : ℕ} {v : Fin d → E} (hv : Orthonormal 𝕜 v) (x y : EuclideanSpace 𝕜 (Fin d)) : inner 𝕜 ((familyMap v) x) ((familyMap v) y) = inner 𝕜 x y

The coordinate map of an orthonormal family preserves inner products.

noncomputable def TauCeti.familyIsometry {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {d : ℕ} {v : Fin d → E} (hv : Orthonormal 𝕜 v) : EuclideanSpace 𝕜 (Fin d) →ₗᵢ[𝕜] E

The bundled coordinate isometry EuclideanSpace 𝕜 (Fin d) →ₗᵢ[𝕜] E of an orthonormal family v, sending eⱼ ↦ vⱼ.

Equations

• TauCeti.familyIsometry hv = (TauCeti.familyMap v).isometryOfInner ⋯

@[simp]

theorem TauCeti.familyIsometry_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {d : ℕ} {v : Fin d → E} (hv : Orthonormal 𝕜 v) (x : EuclideanSpace 𝕜 (Fin d)) : (familyIsometry hv) x = ∑ i : Fin d, x.ofLp i • v i

The bundled isometry acts as the family map.

theorem TauCeti.familyIsometry_single {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {d : ℕ} {v : Fin d → E} (hv : Orthonormal 𝕜 v) (k : Fin d) : (familyIsometry hv) (EuclideanSpace.single k 1) = v k

It sends the k-th standard basis vector to v k.