Günther's identity on the momentum side

gunther_identity (position space, real-valued maps) is transported to coefficient sequences: for a vector sequence v whose components are rapidly decaying and conjReflect-fixed (so that its synthesis vsynth v is a smooth periodic real map),

-Δ̂ (∂ᵢv · ∂ⱼv) = ∂ᵢ(Lv · ∂ⱼv) + ∂ⱼ(Lv · ∂ᵢv) - 2 Lv · ∂ᵢ∂ⱼv + 2 ∑ₖ ∂ᵢ∂ₖv · ∂ⱼ∂ₖv

where products are seqConv, · is dotConv, ∂ᵢ is vpartial i, L is vlap, and Δ̂ = laplacianCoeff (so -Δ̂ is L on scalar sequences).

Consequently the polarized pieces Fb, Ub of the Günther operator satisfy ∂ᵢv · ∂ⱼv = ∂ᵢ Fb j v v + ∂ⱼ Fb i v v + Ub i j v v, which is the identity behind the ansatz of Theorem B. The dictionary between real maps ℝⁿ → ℝᴺ and vector sequences (vcoeff, vsynth) is set up here as well.

Real maps ↔ vector sequences

def NashEmbedding.VRapid (n N : ℕ) (v : VecSeq n N) : Prop

Componentwise rapid decay.

Equations

• NashEmbedding.VRapid n N v = ∀ (α : Fin N), NashEmbedding.Sobolev.IsRapidDecay n (v α)

def NashEmbedding.VReal {n N : ℕ} (v : VecSeq n N) : Prop

Componentwise conjReflect-fixed: the coefficients of a real-valued map.

Equations

• NashEmbedding.VReal v = ∀ (α : Fin N), NashEmbedding.Sobolev.conjReflect (v α) = v α

noncomputable def NashEmbedding.vcoeff {N : ℕ} (n : ℕ) (u : (Fin n → ℝ) → Fin N → ℝ) : VecSeq n N

The coefficient sequences of a real map u : ℝⁿ → ℝᴺ.

Equations

• NashEmbedding.vcoeff n u α = NashEmbedding.Sobolev.stdFourierCoeff n fun (x : Fin n → ℝ) => ↑(u x α)

noncomputable def NashEmbedding.vsynth {N : ℕ} (n : ℕ) (v : VecSeq n N) : (Fin n → ℝ) → Fin N → ℝ

The (real) synthesis of a vector sequence.

Equations

• NashEmbedding.vsynth n v x α = (NashEmbedding.Sobolev.fourierSynthesis n (v α) x).re

theorem NashEmbedding.VRapid.vmem {n N : ℕ} {v : VecSeq n N} (hv : VRapid n N v) (s : ℝ) : VMem n N s v

theorem NashEmbedding.vrapid_of_vmem {n N : ℕ} {v : VecSeq n N} (hv : ∀ (k : ℕ), VMem n N (↑k) v) : VRapid n N v

theorem NashEmbedding.isPeriodic2Pi_pderiv {n : ℕ} {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : (Fin n → ℝ) → V} (hf : Sobolev.IsPeriodic2Pi f) (i : Fin n) : Sobolev.IsPeriodic2Pi (pderiv i f)

Coordinate partials of periodic maps are periodic (any target).

theorem NashEmbedding.SmoothPeriodic.pderiv {n : ℕ} {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : (Fin n → ℝ) → V} (hf : SmoothPeriodic f) (i : Fin n) : SmoothPeriodic (NashEmbedding.pderiv i f)

theorem NashEmbedding.SmoothPeriodic.sumSqDeriv {n : ℕ} {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : (Fin n → ℝ) → V} (hf : SmoothPeriodic f) : SmoothPeriodic (NashEmbedding.sumSqDeriv f)

theorem NashEmbedding.SmoothPeriodic.dotProduct {n N : ℕ} {u w : (Fin n → ℝ) → Fin N → ℝ} (hu : SmoothPeriodic u) (hw : SmoothPeriodic w) : SmoothPeriodic fun (x : Fin n → ℝ) => u x ⬝ᵥ w x

theorem NashEmbedding.smoothPeriodic_ofReal_comp {n N : ℕ} {u : (Fin n → ℝ) → Fin N → ℝ} (hu : SmoothPeriodic u) (α : Fin N) : (ContDiff ℝ ↑⊤ fun (x : Fin n → ℝ) => ↑(u x α)) ∧ Sobolev.IsPeriodic2Pi fun (x : Fin n → ℝ) => ↑(u x α)

The complexified component x ↦ (u x α : ℂ) of a smooth periodic real map is smooth periodic.

theorem NashEmbedding.smoothPeriodic_ofReal_scalar {n : ℕ} {f : (Fin n → ℝ) → ℝ} (hf : SmoothPeriodic f) : (ContDiff ℝ ↑⊤ fun (x : Fin n → ℝ) => ↑(f x)) ∧ Sobolev.IsPeriodic2Pi fun (x : Fin n → ℝ) => ↑(f x)

theorem NashEmbedding.pderiv_ofReal {n : ℕ} {f : (Fin n → ℝ) → ℝ} (hf : ContDiff ℝ (↑⊤) f) (i : Fin n) : (pderiv i fun (x : Fin n → ℝ) => ↑(f x)) = fun (x : Fin n → ℝ) => ↑(pderiv i f x)

Casting to ℂ commutes with pderiv (scalar case).

theorem NashEmbedding.pderiv_ofReal_comp {n N : ℕ} {u : (Fin n → ℝ) → Fin N → ℝ} (hu : ContDiff ℝ (↑⊤) u) (i : Fin n) (α : Fin N) : (pderiv i fun (x : Fin n → ℝ) => ↑(u x α)) = fun (x : Fin n → ℝ) => ↑(pderiv i u x α)

Casting to ℂ commutes with pderiv (component case).

theorem NashEmbedding.vcoeff_vrapid {n N : ℕ} (hn : 0 < n) {u : (Fin n → ℝ) → Fin N → ℝ} (hu : SmoothPeriodic u) : VRapid n N (vcoeff n u)

theorem NashEmbedding.vcoeff_vreal {n N : ℕ} {u : (Fin n → ℝ) → Fin N → ℝ} : VReal (vcoeff n u)

theorem NashEmbedding.ofReal_vsynth {n N : ℕ} {v : VecSeq n N} (hr : VReal v) (x : Fin n → ℝ) (α : Fin N) : ↑(vsynth n v x α) = Sobolev.fourierSynthesis n (v α) x

The synthesis of a VReal sequence is real: ((vsynth v x α : ℝ) : ℂ) = a_check_α x.

theorem NashEmbedding.vsynth_smoothPeriodic {n N : ℕ} (hn : 0 < n) {v : VecSeq n N} (hv : VRapid n N v) : SmoothPeriodic (vsynth n v)

theorem NashEmbedding.vcoeff_vsynth {n N : ℕ} (hn : 0 < n) {v : VecSeq n N} (hv : VRapid n N v) (hr : VReal v) : vcoeff n (vsynth n v) = v

theorem NashEmbedding.vsynth_vcoeff {n N : ℕ} (hn : 0 < n) {u : (Fin n → ℝ) → Fin N → ℝ} (hu : SmoothPeriodic u) : vsynth n (vcoeff n u) = u

The dictionary for derivatives and dot products

theorem NashEmbedding.vcoeff_pderiv {n N : ℕ} (hn : 0 < n) {u : (Fin n → ℝ) → Fin N → ℝ} (hu : SmoothPeriodic u) (i : Fin n) : vcoeff n (pderiv i u) = vpartial i (vcoeff n u)

theorem NashEmbedding.vcoeff_sumSqDeriv {n N : ℕ} (hn : 0 < n) {u : (Fin n → ℝ) → Fin N → ℝ} (hu : SmoothPeriodic u) : vcoeff n (sumSqDeriv u) = vlap (vcoeff n u)

theorem NashEmbedding.stdFourierCoeff_dotProduct {n N : ℕ} (hn : 0 < n) {u w : (Fin n → ℝ) → Fin N → ℝ} (hu : SmoothPeriodic u) (hw : SmoothPeriodic w) : (Sobolev.stdFourierCoeff n fun (x : Fin n → ℝ) => ↑(u x ⬝ᵥ w x)) = dotConv (vcoeff n u) (vcoeff n w)

Coefficients of a dot product of real maps: dotConv of the coefficient sequences.

theorem NashEmbedding.stdFourierCoeff_pderiv_ofReal {n : ℕ} (hn : 0 < n) {f : (Fin n → ℝ) → ℝ} (hf : SmoothPeriodic f) (i : Fin n) : (Sobolev.stdFourierCoeff n fun (x : Fin n → ℝ) => ↑(pderiv i f x)) = Sobolev.partialCoeff i (Sobolev.stdFourierCoeff n fun (x : Fin n → ℝ) => ↑(f x))

Coefficients of ∂ᵢ of a real scalar function.

theorem NashEmbedding.stdFourierCoeff_sumSqDeriv_ofReal {n : ℕ} (hn : 0 < n) {f : (Fin n → ℝ) → ℝ} (hf : SmoothPeriodic f) : (Sobolev.stdFourierCoeff n fun (x : Fin n → ℝ) => ↑(sumSqDeriv f x)) = fun (m : Fin n → ℤ) => -Sobolev.laplacianCoeff (Sobolev.stdFourierCoeff n fun (x : Fin n → ℝ) => ↑(f x)) m

Coefficients of L = ∑ₖ ∂ₖ² of a real scalar function: -laplacianCoeff.

The identity on sequences

theorem NashEmbedding.gunther_identity_seq {n N : ℕ} (hn : 0 < n) {v : VecSeq n N} (hv : VRapid n N v) (hr : VReal v) (i j : Fin n) : (fun (m : Fin n → ℤ) => -Sobolev.laplacianCoeff (dotConv (vpartial i v) (vpartial j v)) m) = fun (m : Fin n → ℤ) => Sobolev.partialCoeff i (dotConv (vlap v) (vpartial j v)) m + Sobolev.partialCoeff j (dotConv (vlap v) (vpartial i v)) m - 2 * dotConv (vlap v) (vpartial i (vpartial j v)) m + 2 * ∑ k : Fin n, dotConv (vpartial i (vpartial k v)) (vpartial j (vpartial k v)) m

Günther's identity on the momentum side.

theorem NashEmbedding.dotConv_eq_Fb_Ub {n N : ℕ} (hn : 0 < n) {v : VecSeq n N} (hv : VRapid n N v) (hr : VReal v) (i j : Fin n) : dotConv (vpartial i v) (vpartial j v) = fun (m : Fin n → ℤ) => Sobolev.partialCoeff i (Fb j v v) m + Sobolev.partialCoeff j (Fb i v v) m + Ub i j v v m

The ansatz identity: ∂ᵢv · ∂ⱼv = ∂ᵢ Fb j v v + ∂ⱼ Fb i v v + Ub i j v v.

theorem NashEmbedding.Ub_symm {n N : ℕ} {v : VecSeq n N} (i j : Fin n) : Ub i j v v = Ub j i v v

Ub is symmetric on the diagonal.