Every integer Sobolev order propagates on the same interval on which the actual H³ norm is bounded. There is no order-dependent shortening of time and no postulated energy differential inequality.

def EulerOrdinarySobolev.wordCount (m : ℕ) : ℝ

Word count, given by ∑ n ∈ range (m+1), (3 : ℝ)^n.

Equations

• EulerOrdinarySobolev.wordCount m = ∑ n ∈ Finset.range (m + 1), 3 ^ n

theorem EulerOrdinarySobolev.wordCount_nonneg (m : ℕ) : 0 ≤ wordCount m

theorem EulerOrdinarySobolev.tensorNorm_le_wordCount (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (m : ℕ) (N : ℝ) (hN : WordBound m N A) : tensorNorm m A ≤ wordCount m * N

theorem EulerOrdinarySobolev.tensorNorm_le_energy (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (m : ℕ) : tensorNorm m A ≤ wordCount m * √(wordEnergy m A)

noncomputable def EulerOrdinarySobolev.Evolution.integerEnergyPath {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (m : ℕ) : C(↑(Set.Icc 0 T), ℝ)

Integer energy path, given by ⟨fun t => wordEnergy m (U.velocity t),wordEnergy_continuous U.velocity U.velocity_continuous m⟩.

Equations

• U.integerEnergyPath m = { toFun := fun (t : ↑(Set.Icc 0 T)) => EulerOrdinarySobolev.wordEnergy m (U.velocity t), continuous_toFun := ⋯ }

noncomputable def EulerOrdinarySobolev.Evolution.integerEnergyDerivative {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (m : ℕ) (t : ↑(Set.Icc 0 T)) : ℝ

Integer energy derivative, given by integerEnergyProduction m (U.velocity t) (U.derivative t).

Equations

• U.integerEnergyDerivative m t = EulerOrdinarySobolev.integerEnergyProduction m (U.velocity t) (U.derivative t)

theorem EulerOrdinarySobolev.Evolution.derivative_eq_eulerRhs {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (t : ↑(Set.Icc 0 T)) : U.derivative t = eulerRhs (U.velocity t) (U.pressureForce t)

theorem EulerOrdinarySobolev.Evolution.integerEnergy_hasDerivWithinAt {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (m : ℕ) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (U.integerEnergyPath m)) (U.integerEnergyDerivative m t) (Set.Icc 0 T) ↑t

theorem EulerOrdinarySobolev.Evolution.integerEnergyDerivative_bound {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (m : ℕ) (hm : 3 ≤ m) (M : ℝ) (hM : ∀ (t : ↑(Set.Icc 0 T)), WordBound 3 M (U.velocity t)) (t : ↑(Set.Icc 0 T)) : U.integerEnergyDerivative m t ≤ tameEnergyConstant m * M * (U.integerEnergyPath m) t

theorem EulerOrdinarySobolev.Evolution.integer_energy_bound {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (m : ℕ) (hm : 3 ≤ m) (M : ℝ) (hM : ∀ (t : ↑(Set.Icc 0 T)), WordBound 3 M (U.velocity t)) (t : ↑(Set.Icc 0 T)) : wordEnergy m (U.velocity t) ≤ wordEnergy m (U.velocity ⟨0, ⋯⟩) * Real.exp (tameEnergyConstant m * M * ↑t)

theorem EulerOrdinarySobolev.Evolution.integer_energy_uniform {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (m : ℕ) (hm : 3 ≤ m) (M : ℝ) (hM : ∀ (t : ↑(Set.Icc 0 T)), WordBound 3 M (U.velocity t)) (t : ↑(Set.Icc 0 T)) : wordEnergy m (U.velocity t) ≤ wordEnergy m (U.velocity ⟨0, ⋯⟩) * Real.exp (tameEnergyConstant m * M * T)

theorem EulerOrdinarySobolev.Evolution.tensorNorm_uniform {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (m : ℕ) (hm : 3 ≤ m) (M : ℝ) (hM : ∀ (t : ↑(Set.Icc 0 T)), WordBound 3 M (U.velocity t)) (t : ↑(Set.Icc 0 T)) : tensorNorm m (U.velocity t) ≤ wordCount m * √(wordEnergy m (U.velocity ⟨0, ⋯⟩) * Real.exp (tameEnergyConstant m * M * T))

theorem EulerOrdinarySobolev.Evolution.higher_energy_of_h3 {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (m : ℕ) (hm : 3 ≤ m) (M : ℝ) (hM : ∀ (t : ↑(Set.Icc 0 T)), tensorNorm 3 (U.velocity t) ≤ M) (t : ↑(Set.Icc 0 T)) : wordEnergy m (U.velocity t) ≤ wordEnergy m (U.velocity ⟨0, ⋯⟩) * Real.exp (tameEnergyConstant m * M * T)