Bump construction for Theorem A

A fixed one-dimensional bump η, its dilations η(β·) with closed-form mass identities, and the product bump ∏ₖ η(βₖ yₖ) on ℝⁿ with its Gram matrix ∫ ∂ᵢψ ∂ⱼψ (diagonal, explicit).

Main contents

• bumpRadius n — radius ρ with ρ √n < π/2, so a rotated product bump supported in the box of radius ρ lies in (-π,π)ⁿ.
• eta n — a C^∞ bump on ℝ, η = 1 on [-ρ/2, ρ/2], supp η = (-ρ,ρ).
• etaMass n = ∫ η², etaDerivMass n = ∫ η'², both positive.
• dil n β t = η (β t); ∫ (dil β)² = etaMass/β, ∫ (dil β)'² = β·etaDerivMass, ∫ dil β · (dil β)' = 0.

The basic one-dimensional bump

noncomputable def NashEmbedding.bumpRadius (n : ℕ) : ℝ

Radius ρ := π / (2√n + 1); then ρ √n < π/2 for every n.

Equations

• NashEmbedding.bumpRadius n = Real.pi / (2 * √↑n + 1)

theorem NashEmbedding.bumpRadius_pos (n : ℕ) : 0 < bumpRadius n

theorem NashEmbedding.bumpRadius_mul_sqrt_lt (n : ℕ) : bumpRadius n * √↑n < Real.pi / 2

noncomputable def NashEmbedding.bump1D (n : ℕ) : ContDiffBump 0

The basic bump as a ContDiffBump centred at 0, rIn = ρ/2, rOut = ρ.

Equations

• NashEmbedding.bump1D n = { rIn := NashEmbedding.bumpRadius n / 2, rOut := NashEmbedding.bumpRadius n, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }

noncomputable def NashEmbedding.eta (n : ℕ) : ℝ → ℝ

The basic bump as a function ℝ → ℝ.

Equations

• NashEmbedding.eta n t = ↑(NashEmbedding.bump1D n) t

theorem NashEmbedding.eta_contDiff (n : ℕ) : ContDiff ℝ (↑⊤) (eta n)

theorem NashEmbedding.eta_continuous (n : ℕ) : Continuous (eta n)

theorem NashEmbedding.eta_hasCompactSupport (n : ℕ) : HasCompactSupport (eta n)

theorem NashEmbedding.eta_nonneg (n : ℕ) (t : ℝ) : 0 ≤ eta n t

theorem NashEmbedding.eta_zero (n : ℕ) : eta n 0 = 1

theorem NashEmbedding.eta_eq_zero_of_le {n : ℕ} {t : ℝ} (ht : bumpRadius n ≤ |t|) : eta n t = 0

theorem NashEmbedding.eta_support (n : ℕ) : Function.support (eta n) = Metric.ball 0 (bumpRadius n)

theorem NashEmbedding.abs_lt_of_eta_ne_zero {n : ℕ} {t : ℝ} (h : eta n t ≠ 0) : |t| < bumpRadius n

noncomputable def NashEmbedding.etaMass (n : ℕ) : ℝ

∫ η².

Equations

• NashEmbedding.etaMass n = ∫ (t : ℝ), NashEmbedding.eta n t ^ 2

noncomputable def NashEmbedding.etaDerivMass (n : ℕ) : ℝ

∫ η'².

Equations

• NashEmbedding.etaDerivMass n = ∫ (t : ℝ), deriv (NashEmbedding.eta n) t ^ 2

theorem NashEmbedding.deriv_eta_continuous (n : ℕ) : Continuous (deriv (eta n))

theorem NashEmbedding.deriv_eta_hasCompactSupport (n : ℕ) : HasCompactSupport (deriv (eta n))

theorem NashEmbedding.etaMass_pos (n : ℕ) : 0 < etaMass n

theorem NashEmbedding.etaDerivMass_pos (n : ℕ) : 0 < etaDerivMass n

Dilations

noncomputable def NashEmbedding.dil (n : ℕ) (β : ℝ) : ℝ → ℝ

The dilated bump η(βt).

Equations

• NashEmbedding.dil n β t = NashEmbedding.eta n (β * t)

theorem NashEmbedding.dil_contDiff (n : ℕ) (β : ℝ) : ContDiff ℝ (↑⊤) (dil n β)

theorem NashEmbedding.dil_continuous (n : ℕ) (β : ℝ) : Continuous (dil n β)

theorem NashEmbedding.dil_hasCompactSupport (n : ℕ) {β : ℝ} (hβ : 0 < β) : HasCompactSupport (dil n β)

theorem NashEmbedding.abs_lt_of_dil_ne_zero {n : ℕ} {β t : ℝ} (hβ : 1 ≤ β) (h : dil n β t ≠ 0) : |t| < bumpRadius n

theorem NashEmbedding.deriv_dil (n : ℕ) (β t : ℝ) : deriv (dil n β) t = β * deriv (eta n) (β * t)

theorem NashEmbedding.deriv_dil_continuous (n : ℕ) (β : ℝ) : Continuous (deriv (dil n β))

theorem NashEmbedding.deriv_dil_hasCompactSupport (n : ℕ) {β : ℝ} (hβ : 0 < β) : HasCompactSupport (deriv (dil n β))

theorem NashEmbedding.integral_dil_sq (n : ℕ) {β : ℝ} (hβ : 0 < β) : ∫ (t : ℝ), dil n β t ^ 2 = etaMass n / β

theorem NashEmbedding.integral_deriv_dil_sq (n : ℕ) {β : ℝ} (hβ : 0 < β) : ∫ (t : ℝ), deriv (dil n β) t ^ 2 = β * etaDerivMass n

theorem NashEmbedding.integral_dil_mul_deriv (n : ℕ) {β : ℝ} (hβ : 0 < β) : ∫ (t : ℝ), dil n β t * deriv (dil n β) t = 0

The product bump on ℝⁿ

noncomputable def NashEmbedding.prodBump (n : ℕ) (β y : Fin n → ℝ) : ℝ

The product bump ψ_β(y) = ∏ₖ η(βₖ yₖ).

Equations

• NashEmbedding.prodBump n β y = ∏ k : Fin n, NashEmbedding.dil n (β k) (y k)

theorem NashEmbedding.prodBump_contDiff {n : ℕ} (β : Fin n → ℝ) : ContDiff ℝ (↑⊤) (prodBump n β)

theorem NashEmbedding.prodBump_continuous {n : ℕ} (β : Fin n → ℝ) : Continuous (prodBump n β)

theorem NashEmbedding.abs_lt_of_prodBump_ne_zero {n : ℕ} {β : Fin n → ℝ} (hβ : ∀ (k : Fin n), 1 ≤ β k) {y : Fin n → ℝ} (h : prodBump n β y ≠ 0) (k : Fin n) : |y k| < bumpRadius n

theorem NashEmbedding.prodBump_hasCompactSupport {n : ℕ} {β : Fin n → ℝ} (hβ : ∀ (k : Fin n), 1 ≤ β k) : HasCompactSupport (prodBump n β)

noncomputable def NashEmbedding.factor (n : ℕ) (β : Fin n → ℝ) (i k : Fin n) : ℝ → ℝ

The k-th factor of ∂ᵢψ_β: the derivative of the dilated bump when k = i, the dilated bump itself otherwise.

Equations

• NashEmbedding.factor n β i k = if k = i then deriv (NashEmbedding.dil n (β k)) else NashEmbedding.dil n (β k)

theorem NashEmbedding.prodBump_update {n : ℕ} (β y : Fin n → ℝ) (i : Fin n) (t : ℝ) : prodBump n β (Function.update y i t) = dil n (β i) t * ∏ k ∈ Finset.univ.erase i, dil n (β k) (y k)

theorem NashEmbedding.fderiv_prodBump_single {n : ℕ} (β y : Fin n → ℝ) (i : Fin n) : (fderiv ℝ (prodBump n β) y) (Pi.single i 1) = ∏ k : Fin n, factor n β i k (y k)

The Gram matrix

noncomputable def NashEmbedding.gram {n : ℕ} (χ : (Fin n → ℝ) → ℝ) (i j : Fin n) : ℝ

The Gram matrix ∫ ∂ᵢχ ∂ⱼχ of a real function on ℝⁿ.

Equations

• NashEmbedding.gram χ i j = ∫ (x : Fin n → ℝ), (fderiv ℝ χ x) (Pi.single i 1) * (fderiv ℝ χ x) (Pi.single j 1)

theorem NashEmbedding.gram_prodBump {n : ℕ} {β : Fin n → ℝ} (hβ : ∀ (k : Fin n), 0 < β k) (i j : Fin n) : gram (prodBump n β) i j = if i = j then β i * etaDerivMass n * ∏ k ∈ Finset.univ.erase i, etaMass n / β k else 0

The Gram matrix of the product bump is diagonal with explicit entries.

Rotation by a matrix with |det| = 1

noncomputable def NashEmbedding.rotBump (n : ℕ) (β : Fin n → ℝ) (M : Matrix (Fin n) (Fin n) ℝ) (x : Fin n → ℝ) : ℝ

χ(x) = ψ_β(M x).

Equations

• NashEmbedding.rotBump n β M x = NashEmbedding.prodBump n β (M.mulVec x)

theorem NashEmbedding.mulVec_eq_clm {n : ℕ} (M : Matrix (Fin n) (Fin n) ℝ) : (fun (x : Fin n → ℝ) => M.mulVec x) = ⇑(LinearMap.toContinuousLinearMap M.mulVecLin)

theorem NashEmbedding.mulVec_contDiff {n : ℕ} (M : Matrix (Fin n) (Fin n) ℝ) : ContDiff ℝ ↑⊤ fun (x : Fin n → ℝ) => M.mulVec x

theorem NashEmbedding.rotBump_contDiff {n : ℕ} (β : Fin n → ℝ) (M : Matrix (Fin n) (Fin n) ℝ) : ContDiff ℝ (↑⊤) (rotBump n β M)

theorem NashEmbedding.fderiv_rotBump_single {n : ℕ} (β : Fin n → ℝ) (M : Matrix (Fin n) (Fin n) ℝ) (x : Fin n → ℝ) (i : Fin n) : (fderiv ℝ (rotBump n β M) x) (Pi.single i 1) = ∑ k : Fin n, M k i * (fderiv ℝ (prodBump n β) (M.mulVec x)) (Pi.single k 1)

theorem NashEmbedding.det_ne_zero_of_abs_det_eq_one {n : ℕ} {M : Matrix (Fin n) (Fin n) ℝ} (hdet : |M.det| = 1) : M.det ≠ 0

theorem NashEmbedding.integrable_comp_mulVec {n : ℕ} {M : Matrix (Fin n) (Fin n) ℝ} (hdet : |M.det| = 1) {G : (Fin n → ℝ) → ℝ} (hG : Continuous G) (hGi : MeasureTheory.Integrable G MeasureTheory.volume) : MeasureTheory.Integrable (fun (x : Fin n → ℝ) => G (M.mulVec x)) MeasureTheory.volume

theorem NashEmbedding.integral_comp_mulVec {n : ℕ} {M : Matrix (Fin n) (Fin n) ℝ} (hdet : |M.det| = 1) {G : (Fin n → ℝ) → ℝ} (hG : Continuous G) : ∫ (x : Fin n → ℝ), G (M.mulVec x) = ∫ (y : Fin n → ℝ), G y

noncomputable def NashEmbedding.prodBumpPD (n : ℕ) (β : Fin n → ℝ) (k : Fin n) (y : Fin n → ℝ) : ℝ

The k-th partial derivative of the product bump, as a function.

Equations

• NashEmbedding.prodBumpPD n β k y = (fderiv ℝ (NashEmbedding.prodBump n β) y) (Pi.single k 1)

theorem NashEmbedding.prodBumpPD_continuous {n : ℕ} (β : Fin n → ℝ) (k : Fin n) : Continuous (prodBumpPD n β k)

theorem NashEmbedding.prodBumpPD_hasCompactSupport {n : ℕ} {β : Fin n → ℝ} (hβ : ∀ (k : Fin n), 1 ≤ β k) (k : Fin n) : HasCompactSupport (prodBumpPD n β k)

theorem NashEmbedding.gram_rotBump {n : ℕ} {β : Fin n → ℝ} (hβ : ∀ (k : Fin n), 1 ≤ β k) {M : Matrix (Fin n) (Fin n) ℝ} (hdet : |M.det| = 1) (i j : Fin n) : gram (rotBump n β M) i j = ∑ k : Fin n, M k i * M k j * (β k * etaDerivMass n * ∏ l ∈ Finset.univ.erase k, etaMass n / β l)

Gram of the rotated bump: Gram_χ = Mᵀ Gram_ψ M, with Gram_ψ diagonal.

Amplitude

theorem NashEmbedding.gram_const_mul {n : ℕ} {χ : (Fin n → ℝ) → ℝ} (hχ : Differentiable ℝ χ) (A : ℝ) (i j : Fin n) : gram (fun (x : Fin n → ℝ) => A * χ x) i j = A ^ 2 * gram χ i j

Spectral assembly

Orthogonality facts for a real orthogonal (unitary) matrix.

theorem NashEmbedding.mul_transpose_eq_one_of_unitary {n : ℕ} {U : Matrix (Fin n) (Fin n) ℝ} (hU : U ∈ Matrix.unitaryGroup (Fin n) ℝ) : U * U.transpose = 1

theorem NashEmbedding.row_sq_sum_of_unitary {n : ℕ} {U : Matrix (Fin n) (Fin n) ℝ} (hU : U ∈ Matrix.unitaryGroup (Fin n) ℝ) (i : Fin n) : ∑ k : Fin n, U i k ^ 2 = 1

theorem NashEmbedding.abs_det_transpose_of_unitary {n : ℕ} {U : Matrix (Fin n) (Fin n) ℝ} (hU : U ∈ Matrix.unitaryGroup (Fin n) ℝ) : |U.transpose.det| = 1

theorem NashEmbedding.sum_sq_transpose_mulVec_of_unitary {n : ℕ} {U : Matrix (Fin n) (Fin n) ℝ} (hU : U ∈ Matrix.unitaryGroup (Fin n) ℝ) (x : Fin n → ℝ) : ∑ k : Fin n, U.transpose.mulVec x k ^ 2 = ∑ j : Fin n, x j ^ 2

theorem NashEmbedding.sum_abs_mul_abs_le_one_of_unitary {n : ℕ} {U : Matrix (Fin n) (Fin n) ℝ} (hU : U ∈ Matrix.unitaryGroup (Fin n) ℝ) (i j : Fin n) : ∑ k : Fin n, |U i k| * |U j k| ≤ 1

Row-wise Cauchy–Schwarz: ∑ₖ |Uᵢₖ| |Uⱼₖ| ≤ 1.

theorem NashEmbedding.exists_bump_gram_approx {n : ℕ} {B : Matrix (Fin n) (Fin n) ℝ} (hB : B.PosSemidef) {K : ℝ} (hK : 0 < K) : ∃ (χ : (Fin n → ℝ) → ℝ), ContDiff ℝ (↑⊤) χ ∧ HasCompactSupport χ ∧ (∀ (x : Fin n → ℝ), χ x ≠ 0 → ∀ (j : Fin n), |x j| < Real.pi) ∧ ∀ (i j : Fin n), |gram χ i j - B i j| ≤ K

Bump with prescribed Gram matrix up to K. For every real PSD matrix B and every K > 0 there is a C^∞ compactly supported χ with supp χ ⊂ (-π,π)ⁿ and |∫ ∂ᵢχ ∂ⱼχ − Bᵢⱼ| ≤ K for all i, j.