Actual L² stability of two ordinary Euler solutions. The pressure and the entire transport term cancel before estimating the remaining reference-gradient term. All time derivatives are genuine one-sided derivatives at the endpoints.

theorem EulerOrdinarySobolev.advection_norm_gradient (W U : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (K : ℝ) (hK : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ U.field x‖ ≤ K) : ‖(advectionField W U).toLp‖ ≤ K * ‖W.toLp‖

theorem EulerOrdinarySobolev.differenceRhs_l2_bound (U W P : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (K : ℝ) (hK : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ U.field x‖ ≤ K) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence (U.addField W).field x = 0) (hW : W.toLp ∈ EulerMeanSolenoidal.solenoidalSpace) (hP : P.toLp ∈ EulerMeanSolenoidal.gradientSpace) : 2 * inner ℝ W.toLp (differenceRhs U W P).toLp ≤ 2 * K * ‖W.toLp‖ ^ 2

theorem EulerOrdinarySobolev.linear_stability_within (X X' : ℝ → ℝ) (C T : ℝ) (hcont : ContinuousOn X (Set.Icc 0 T)) (hder : ∀ t ∈ Set.Ico 0 T, HasDerivWithinAt X (X' t) (Set.Icc 0 T) t) (hineq : ∀ t ∈ Set.Ico 0 T, X' t ≤ C * X t) (t : ℝ) : t ∈ Set.Icc 0 T → X t ≤ X 0 * Real.exp (C * t)

noncomputable def EulerOrdinarySobolev.Evolution.velocityPath {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)

Velocity path, given by ordinaryWordPath U.velocity U.velocity_continuous (Fin.elim0 : Fin 0 → Fin 3).

Equations

• U.velocityPath = EulerOrdinarySobolev.ordinaryWordPath U.velocity ⋯ Fin.elim0

@[simp]

theorem EulerOrdinarySobolev.Evolution.velocityPath_apply {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (t : ↑(Set.Icc 0 T)) : U.velocityPath t = (U.velocity t).toLp

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

L2 energy path as an element of C(Icc (0 : ℝ) T,ℝ).

Equations

• U.l2EnergyPath V = { toFun := fun (t : ↑(Set.Icc 0 T)) => ‖(U.difference V t).toLp‖ ^ 2, continuous_toFun := ⋯ }

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

L2 energy derivative, given by 2*⟪(U.difference V t).toLp,(U.differenceDerivative V t).toLp⟫_ℝ.

Equations

• U.l2EnergyDerivative V t = 2 * inner ℝ (U.difference V t).toLp (U.differenceDerivative V t).toLp

theorem EulerOrdinarySobolev.Evolution.l2Energy_hasDerivWithinAt {T : ℝ} {hT : 0 ≤ T} (U V : Evolution T hT) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (U.l2EnergyPath V)) (U.l2EnergyDerivative V t) (Set.Icc 0 T) ↑t

theorem EulerOrdinarySobolev.Evolution.l2EnergyDerivative_bound {T : ℝ} {hT : 0 ≤ T} (U V : Evolution T hT) (K : ℝ) (hK : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (U.velocity t).field x‖ ≤ K) (t : ↑(Set.Icc 0 T)) : U.l2EnergyDerivative V t ≤ 2 * K * (U.l2EnergyPath V) t

theorem EulerOrdinarySobolev.Evolution.l2_energy_bound {T : ℝ} {hT : 0 ≤ T} (U V : Evolution T hT) (K : ℝ) (hK : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (U.velocity t).field x‖ ≤ K) (t : ↑(Set.Icc 0 T)) : ‖(U.difference V t).toLp‖ ^ 2 ≤ ‖(U.difference V ⟨0, ⋯⟩).toLp‖ ^ 2 * Real.exp (2 * K * ↑t)

theorem EulerOrdinarySobolev.Evolution.l2_stability {T : ℝ} {hT : 0 ≤ T} (U V : Evolution T hT) (K : ℝ) (hK : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (U.velocity t).field x‖ ≤ K) (t : ↑(Set.Icc 0 T)) : ‖(U.difference V t).toLp‖ ≤ ‖(U.difference V ⟨0, ⋯⟩).toLp‖ * Real.exp (K * ↑t)

theorem EulerOrdinarySobolev.Evolution.velocityPath_norm_sub_le {T : ℝ} {hT : 0 ≤ T} (U V : Evolution T hT) (K : ℝ) (hK0 : 0 ≤ K) (hK : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (U.velocity t).field x‖ ≤ K) : ‖V.velocityPath - U.velocityPath‖ ≤ ‖V.velocityPath ⟨0, ⋯⟩ - U.velocityPath ⟨0, ⋯⟩‖ * Real.exp (K * T)

theorem EulerOrdinarySobolev.Evolution.l2_stability_of_h3 {T : ℝ} {hT : 0 ≤ T} (U V : Evolution T hT) (M : ℝ) (hM : ∀ (t : ↑(Set.Icc 0 T)), tensorNorm 3 (U.velocity t) ≤ M) (t : ↑(Set.Icc 0 T)) : ‖(U.difference V t).toLp‖ ≤ ‖(U.difference V ⟨0, ⋯⟩).toLp‖ * Real.exp (9 * EulerSmoothSobolev.smoothEmbeddingConstant * M * ↑t)