Actual Euler evolutions and their genuine H³ difference-energy law. The record contains only the fields, their classical Euler equation, the Helmholtz constraints, and continuity of their ordinary L² jets.

A genuine smooth L² gradient belongs to the closed ordinary gradient space, even when its scalar potential is not square-integrable. The solenoidal remainder is both curl-free and harmonic, hence zero by the actual L² integration-by-parts identity.

theorem EulerOrdinarySobolev.solenoidal_orbit (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : EulerMeanSmoothRepresentative.SmoothOrbit (EulerMeanSolenoidal.solenoidalProjection A.toLp)

theorem EulerOrdinarySobolev.curl_zero_of_symmetric (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (x : EulerSmoothLimit.Space) (i j : Fin 3), ((fderiv ℝ A.field x) (EuclideanSpace.single i 1)).ofLp j = ((fderiv ℝ A.field x) (EuclideanSpace.single j 1)).ofLp i) : EulerMeanCutoffCurl.vectorCurl A.field = 0

theorem EulerOrdinarySobolev.gradient_mem_of_symmetric (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (x : EulerSmoothLimit.Space) (i j : Fin 3), ((fderiv ℝ A.field x) (EuclideanSpace.single i 1)).ofLp j = ((fderiv ℝ A.field x) (EuclideanSpace.single j 1)).ofLp i) : A.toLp ∈ EulerMeanSolenoidal.gradientSpace

theorem EulerOrdinarySobolev.gradient_mem (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (p : EulerSmoothLimit.Space → ℝ) (hp : ContDiff ℝ (↑⊤) p) (hgrad : ∀ (x : EulerSmoothLimit.Space), A.field x = gradient p x) : A.toLp ∈ EulerMeanSolenoidal.gradientSpace

theorem EulerOrdinarySobolev.gradient_pairing_zero (A U : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (p : EulerSmoothLimit.Space → ℝ) (hp : ContDiff ℝ (↑⊤) p) (hgrad : ∀ (x : EulerSmoothLimit.Space), A.field x = gradient p x) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence U.field x = 0) : inner ℝ A.toLp U.toLp = 0

theorem EulerOrdinarySobolev.potential_smooth (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (p : EulerSmoothLimit.Space → ℝ) (hp : Differentiable ℝ p) (hgrad : ∀ (x : EulerSmoothLimit.Space), A.field x = gradient p x) : ContDiff ℝ (↑⊤) p

theorem EulerOrdinarySobolev.gradient_pairing_zero_of_differentiable (A U : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (p : EulerSmoothLimit.Space → ℝ) (hp : Differentiable ℝ p) (hgrad : ∀ (x : EulerSmoothLimit.Space), A.field x = gradient p x) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence U.field x = 0) : inner ℝ A.toLp U.toLp = 0

@[instance_reducible]

noncomputable def EulerOrdinarySobolev.instOrdinaryEulerDifference1 : NormedAddCommGroup EulerSmoothLimit.Space

Cache the standard NormedAddCommGroup Space instance to shorten typeclass synthesis.

Equations

• EulerOrdinarySobolev.instOrdinaryEulerDifference1 = inferInstance

@[instance_reducible]

noncomputable def EulerOrdinarySobolev.instOrdinaryEulerDifference2 : NormedSpace ℝ EulerSmoothLimit.Space

Cache the standard NormedSpace ℝ Space instance to shorten typeclass synthesis.

Equations

• EulerOrdinarySobolev.instOrdinaryEulerDifference2 = inferInstance

structure EulerOrdinarySobolev.Evolution (T : ℝ) (hT : 0 ≤ T) : Type

Evolution data, collecting velocity, pressureForce, velocity_continuous, pressure_continuous, solenoidal, gradient and their compatibility conditions.

• velocity : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

  Velocity field of Evolution, of type Icc (0 : ℝ) T → SmoothL2Field Space.

• pressureForce : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

  Pressure force of Evolution, of type Icc (0 : ℝ) T → SmoothL2Field Space.

• velocity_continuous (n : ℕ) : Continuous fun (t : ↑(Set.Icc 0 T)) => (self.velocity t).jetLp n
• pressure_continuous (n : ℕ) : Continuous fun (t : ↑(Set.Icc 0 T)) => (self.pressureForce t).jetLp n
• solenoidal (t : ↑(Set.Icc 0 T)) : (self.velocity t).toLp ∈ EulerMeanSolenoidal.solenoidalSpace
• gradient (t : ↑(Set.Icc 0 T)) : (self.pressureForce t).toLp ∈ EulerMeanSolenoidal.gradientSpace
• time_law (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : EulerSmoothLimit.Space) : HasDerivAt (fun (r : ℝ) => (self.velocity (Set.projIcc 0 T hT r)).field x) (-(fderiv ℝ (self.velocity ⟨t, ⋯⟩).field x) ((self.velocity ⟨t, ⋯⟩).field x) - (self.pressureForce ⟨t, ⋯⟩).field x) t

def EulerOrdinarySobolev.evolutionOfClassical (T : ℝ) (hT : 0 ≤ T) (U G : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hU : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (U t).jetLp n) (hG : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (G t).jetLp n) (u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space) (p : ℝ × EulerSmoothLimit.Space → ℝ) (hu : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), u (↑t, x) = (U t).field x) (hp : ∀ (t : ↑(Set.Icc 0 T)), Differentiable ℝ fun (x : EulerSmoothLimit.Space) => p (↑t, x)) (hg : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), gradient (fun (y : EulerSmoothLimit.Space) => p (↑t, y)) x = (G t).field x) (hdiv : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence (U t).field x = 0) (hdiff : ∀ t ∈ Set.Ioo 0 T, ∀ (x : EulerSmoothLimit.Space), DifferentiableAt ℝ u (t, x)) (heuler : ∀ t ∈ Set.Ioo 0 T, ∀ (x : EulerSmoothLimit.Space), EulerLagrangian.momentumResidual u p (t, x) = 0) : Evolution T hT

Evolution of classical, bundling velocity, pressureForce, velocity_continuous, pressure_continuous and the required compatibility proofs.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerOrdinarySobolev.continuous_jet_fieldSub {K : Type u_1} [TopologicalSpace K] (A B : K → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : K) => (A t).jetLp n) (hB : ∀ (n : ℕ), Continuous fun (t : K) => (B t).jetLp n) (n : ℕ) : Continuous fun (t : K) => (fieldSub (A t) (B t)).jetLp n

noncomputable def EulerOrdinarySobolev.Evolution.derivative {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Derivative, given by EulerSmoothEulerEvolution.rhs U.velocity U.velocity_continuous U.pressureForce.

Equations

• U.derivative = EulerSmoothEulerEvolution.rhs U.velocity ⋯ U.pressureForce

theorem EulerOrdinarySobolev.Evolution.derivative_field {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : (U.derivative t).field x = -(fderiv ℝ (U.velocity t).field x) ((U.velocity t).field x) - (U.pressureForce t).field x

theorem EulerOrdinarySobolev.Evolution.derivative_continuous {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (n : ℕ) : Continuous fun (t : ↑(Set.Icc 0 T)) => (U.derivative t).jetLp n

noncomputable def EulerOrdinarySobolev.Evolution.difference {T : ℝ} {hT : 0 ≤ T} (U V : Evolution T hT) (t : ↑(Set.Icc 0 T)) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Difference, given by fieldSub (V.velocity t) (U.velocity t).

Equations

• U.difference V t = EulerOrdinarySobolev.fieldSub (V.velocity t) (U.velocity t)

noncomputable def EulerOrdinarySobolev.Evolution.pressureDifference {T : ℝ} {hT : 0 ≤ T} (U V : Evolution T hT) (t : ↑(Set.Icc 0 T)) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Pressure difference, given by fieldSub (V.pressureForce t) (U.pressureForce t).

Equations

• U.pressureDifference V t = EulerOrdinarySobolev.fieldSub (V.pressureForce t) (U.pressureForce t)

noncomputable def EulerOrdinarySobolev.Evolution.differenceDerivative {T : ℝ} {hT : 0 ≤ T} (U V : Evolution T hT) (t : ↑(Set.Icc 0 T)) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Difference derivative, given by fieldSub (V.derivative t) (U.derivative t).

Equations

• U.differenceDerivative V t = EulerOrdinarySobolev.fieldSub (V.derivative t) (U.derivative t)

theorem EulerOrdinarySobolev.Evolution.difference_continuous {T : ℝ} {hT : 0 ≤ T} (U V : Evolution T hT) (n : ℕ) : Continuous fun (t : ↑(Set.Icc 0 T)) => (U.difference V t).jetLp n

theorem EulerOrdinarySobolev.Evolution.differenceDerivative_continuous {T : ℝ} {hT : 0 ≤ T} (U V : Evolution T hT) (n : ℕ) : Continuous fun (t : ↑(Set.Icc 0 T)) => (U.differenceDerivative V t).jetLp n

theorem EulerOrdinarySobolev.Evolution.differenceDerivative_eq {T : ℝ} {hT : 0 ≤ T} (U V : Evolution T hT) (t : ↑(Set.Icc 0 T)) : U.differenceDerivative V t = differenceRhs (U.velocity t) (U.difference V t) (U.pressureDifference V t)

theorem EulerOrdinarySobolev.Evolution.difference_time_law {T : ℝ} {hT : 0 ≤ T} (U V : Evolution T hT) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : EulerSmoothLimit.Space) : HasDerivAt (fun (r : ℝ) => (U.difference V (Set.projIcc 0 T hT r)).field x) ((U.differenceDerivative V ⟨t, ⋯⟩).field x) t

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

Energy path, given by ⟨fun t => wordEnergy 3 (U.difference V t),wordEnergy_continuous _ (U.difference_continuous V) 3⟩.

Equations

• U.energyPath V = { toFun := fun (t : ↑(Set.Icc 0 T)) => EulerOrdinarySobolev.wordEnergy 3 (U.difference V t), continuous_toFun := ⋯ }

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

Energy derivative, given by energyProduction (U.difference V t) (U.differenceDerivative V t).

Equations

• U.energyDerivative V t = EulerOrdinarySobolev.energyProduction (U.difference V t) (U.differenceDerivative V t)

theorem EulerOrdinarySobolev.Evolution.energy_hasDerivWithinAt {T : ℝ} {hT : 0 ≤ T} (U V : Evolution T hT) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (U.energyPath V)) (U.energyDerivative V t) (Set.Icc 0 T) ↑t

theorem EulerOrdinarySobolev.Evolution.energyDerivative_bound {T : ℝ} {hT : 0 ≤ T} (U V : Evolution T hT) (M : ℝ) (hM : ∀ (t : ↑(Set.Icc 0 T)), WordBound 4 M (U.velocity t)) (t : ↑(Set.Icc 0 T)) : U.energyDerivative V t ≤ 3600 * h3ProductConstant * (M + √((U.energyPath V) t)) * (U.energyPath V) t