NashEmbedding: Realizable Metrics — Theorems

Closure properties, injective realization, flat torus, positive-definite metric closure, and stability under perturbation.

theorem NashEmbedding.contDiff_matrix {n : ℕ} {g : (Fin n → ℝ) → Matrix (Fin n) (Fin n) ℝ} (h : ∀ (i j : Fin n), ContDiff ℝ ↑⊤ fun (x : Fin n → ℝ) => g x i j) : ContDiff ℝ (↑⊤) g

Bridge lemma for the Mathlib v4.31 pin, where Matrix is a def (no longer abbrev). rw's syntactic matching no longer sees through Matrix, but apply/exact/refine unify up to defeq — so a term-mode bridge closes the gap. Mirrors continuous_matrix.

Closure properties of realizable metrics (Lemma 1.4)

theorem NashEmbedding.realizable_sum {n : ℕ} {g₁ g₂ : (Fin n → ℝ) → Matrix (Fin n) (Fin n) ℝ} (h₁ : IsRealizable g₁) (h₂ : IsRealizable g₂) : IsRealizable (g₁ + g₂)

theorem NashEmbedding.realizable_nonneg_smul {n : ℕ} {g : (Fin n → ℝ) → Matrix (Fin n) (Fin n) ℝ} {t : ℝ} (hg : IsRealizable g) (ht : 0 ≤ t) : IsRealizable (t • g)

theorem NashEmbedding.realizable_translate {n : ℕ} {g : (Fin n → ℝ) → Matrix (Fin n) (Fin n) ℝ} {y : Fin n → ℝ} (hg : IsRealizable g) : IsRealizable (translate y g)

theorem NashEmbedding.realizable_finComb {n M : ℕ} {g : Fin M → (Fin n → ℝ) → Matrix (Fin n) (Fin n) ℝ} {t : Fin M → ℝ} {y : Fin M → Fin n → ℝ} (hg : ∀ (α : Fin M), IsRealizable (g α)) (ht : ∀ (α : Fin M), 0 ≤ t α) : IsRealizable (∑ α : Fin M, t α • translate (y α) (g α))

Injective realization theorems

theorem NashEmbedding.injRealizable_posDef {n : ℕ} {g : (Fin n → ℝ) → Matrix (Fin n) (Fin n) ℝ} (hg : IsInjRealizable g) : IsPosDefSmoothMetric g

theorem NashEmbedding.partialDeriv_concat_castAdd {n N₁ N₂ : ℕ} {u₁ : (Fin n → ℝ) → Fin N₁ → ℝ} {u₂ : (Fin n → ℝ) → Fin N₂ → ℝ} (hd₁ : ContDiff ℝ (↑⊤) u₁) (hd₂ : ContDiff ℝ (↑⊤) u₂) (i : Fin n) (x : Fin n → ℝ) (j : Fin N₁) : partialDeriv i (fun (x : Fin n → ℝ) => Fin.append (u₁ x) (u₂ x)) x (Fin.castAdd N₂ j) = partialDeriv i u₁ x j

theorem NashEmbedding.linearIndependent_of_append_proj {n N₁ N₂ : ℕ} {f₁ : Fin n → Fin N₁ → ℝ} {f₂ : Fin n → Fin N₂ → ℝ} (hli : LinearIndependent ℝ f₁) : LinearIndependent ℝ fun (i : Fin n) => Fin.append (f₁ i) (f₂ i)

theorem NashEmbedding.partialDeriv_concat {n N₁ N₂ : ℕ} {u₁ : (Fin n → ℝ) → Fin N₁ → ℝ} {u₂ : (Fin n → ℝ) → Fin N₂ → ℝ} (hd₁ : ContDiff ℝ (↑⊤) u₁) (hd₂ : ContDiff ℝ (↑⊤) u₂) (i : Fin n) (x : Fin n → ℝ) : partialDeriv i (fun (x : Fin n → ℝ) => Fin.append (u₁ x) (u₂ x)) x = Fin.append (partialDeriv i u₁ x) (partialDeriv i u₂ x)

theorem NashEmbedding.injRealizable_promotion {n : ℕ} {g₁ g₂ : (Fin n → ℝ) → Matrix (Fin n) (Fin n) ℝ} (h₁ : IsInjRealizable g₁) (h₂ : IsRealizable g₂) : IsInjRealizable (g₁ + g₂)

The flat-torus embedding (Lemma 1.10)

theorem NashEmbedding.flatMetric_isPosDefSmoothMetric {n : ℕ} : IsPosDefSmoothMetric (flatMetric n)

theorem NashEmbedding.flatTorusEmb_smoothPeriodic {n : ℕ} : SmoothPeriodic (flatTorusEmb n)

theorem NashEmbedding.flatTorusEmb_isInjectiveEmbedding {n : ℕ} : IsInjectiveEmbedding (flatTorusEmb n)

theorem NashEmbedding.flatTorusEmb_injRealizes {n : ℕ} : IsInjRealizable (flatMetric n)

Closure of positive-definite metrics (Lemma 1.11)

theorem NashEmbedding.posDefSmoothMetric_add {n : ℕ} {g g' : (Fin n → ℝ) → Matrix (Fin n) (Fin n) ℝ} (hg : IsPosDefSmoothMetric g) (hg' : IsPosDefSmoothMetric g') : IsPosDefSmoothMetric (g + g')

theorem NashEmbedding.posDefSmoothMetric_pos_smul {n : ℕ} {g : (Fin n → ℝ) → Matrix (Fin n) (Fin n) ℝ} {t : ℝ} (hg : IsPosDefSmoothMetric g) (ht : 0 < t) : IsPosDefSmoothMetric (t • g)

Stability of positive-definite metrics (Lemma 1.12)

theorem NashEmbedding.posDefSmoothMetric_stability {n : ℕ} {g : (Fin n → ℝ) → Matrix (Fin n) (Fin n) ℝ} (hg : IsPosDefSmoothMetric g) : ∃ η > 0, ∀ (h : (Fin n → ℝ) → Matrix (Fin n) (Fin n) ℝ), Continuous h → Sobolev.IsPeriodic2Pi h → (∀ (x : Fin n → ℝ), (h x).IsHermitian) → (∀ (x : Fin n → ℝ), matOpNorm (h x) < η) → ∀ (x : Fin n → ℝ), (g x + h x).PosDef