Exact concatenated coordinates connecting energy regularization to the actual external/base Gevrey forcing.

theorem EulerEnergyWordCoordinates.wordAtLevel_word (period : ℝ) [Fact (0 < period)] {s : ℕ} (q n : ℕ) (w : Fin n → Fin 4) (h : n + q ≤ s) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) {m : ℕ} (hm : m ≤ q) (v : Fin m → Fin 4) : EulerCylinderSobolevSpace.word period ((EulerSobolevWordLevel.wordAtLevel period q n w h) u) hm v = EulerCylinderSobolevSpace.word period u ⋯ (Fin.append v w)

A derivative of a genuine word-at-level block is the literal concatenated strong derivative.

theorem EulerEnergyWordCoordinates.boundedWordBlock_eq_wordAtLevel (period : ℝ) [Fact (0 < period)] {s : ℕ} (q n : ℕ) (h : q + n ≤ s) (w : Fin n → Fin 4) : EulerMildTopWord.boundedWordBlock period q n h w = EulerSobolevWordLevel.wordAtLevel period q n w ⋯

Bounded word blocks and the spatial-estimate word-at-level operator are the same genuine map.

theorem EulerEnergyWordCoordinates.wordAtLevel_comp (period : ℝ) [Fact (0 < period)] {s p q n m : ℕ} (w : Fin n → Fin 4) (v : Fin m → Fin 4) (h : n + q ≤ s) (h' : m + p ≤ q) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : (EulerSobolevWordLevel.wordAtLevel period p m v h') ((EulerSobolevWordLevel.wordAtLevel period q n w h) u) = (EulerSobolevWordLevel.wordAtLevel period p (m + n) (Fin.append v w) ⋯) u

Two actual Sobolev word blocks compose by literal word concatenation.

def EulerEnergyWordCoordinates.energyLength {N q : ℕ} (I : EulerGevreyMetricComparison.ExternalWord N) (a : EulerBaseWordMetric.BaseWord q) : ℕ

The total derivative length in one external/base energy component.

Equations

• EulerEnergyWordCoordinates.energyLength I a = ↑a.fst + ↑I.fst

def EulerEnergyWordCoordinates.energyWord {N q : ℕ} (I : EulerGevreyMetricComparison.ExternalWord N) (a : EulerBaseWordMetric.BaseWord q) : Fin (energyLength I a) → Fin 4

The literal base-then-external concatenated derivative word of an energy component.

Equations

• EulerEnergyWordCoordinates.energyWord I a = Fin.append a.snd I.snd

theorem EulerEnergyWordCoordinates.energyLength_le {s N q : ℕ} (h : N + q ≤ s) (I : EulerGevreyMetricComparison.ExternalWord N) (a : EulerBaseWordMetric.BaseWord q) : energyLength I a ≤ s

Every total energy word stays below the advertised external-plus-base cutoff.

theorem EulerEnergyWordCoordinates.energyValues_eq_word (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (hN : N + q ≤ s) (I : EulerGevreyMetricComparison.ExternalWord N) (a : EulerBaseWordMetric.BaseWord q) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : EulerGevreyMetricComparison.energyValues period q N hN u I a = EulerCylinderSobolevSpace.word period u ⋯ (energyWord I a)

The actual external/base metric-energy coordinate is exactly its concatenated strong derivative.

theorem EulerEnergyWordCoordinates.energyValueFamily_eq (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (hN : N + q ≤ s + 1) (T : ℝ) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1)))) (I : EulerGevreyMetricComparison.ExternalWord N) (t : ↑(Set.Icc 0 T)) : (EulerRegularizedEnergyFamily.energyValueFamily period energyLength energyWord ⋯ T u I) t = EulerGevreyMetricComparison.energyValues period q N hN (u t) I

The actual continuous energy family used by regularization is exactly the spatial Gevrey energy family.

theorem EulerEnergyWordCoordinates.topTransport_block (period : ℝ) [Fact (0 < period)] {s N : ℕ} (hN : N + 6 ≤ s) (I : EulerGevreyMetricComparison.ExternalWord N) (a : EulerBaseWordMetric.BaseWord 6) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) : (EulerMildTopWord.boundedWordBlock period 1 (energyLength I a) ⋯ (energyWord I a)) u = (EulerSobolevWordLevel.wordAtLevel period 1 (↑a.fst) a.snd ⋯) ((EulerSobolevWordLevel.wordAtLevel period 7 (↑I.fst) I.snd ⋯) u)

The H¹ concatenated word is exactly the twice-blocked derivative used by the actual top transport.