The reverse bridge from ordinary scalar-pressure Euler to the projected equation. The only regularity inputs are the velocity and its actual strong time derivative in all spatial Sobolev orders. Neither a pressure-force regularity hypothesis nor a projected equation is assumed. The scalar pressure may be changed by an arbitrary function of time.

Characterization of the ordinary smooth Euler class by its actual velocity alone. Pressure regularity follows from the projected equation. Every solution has one continuous strong time derivative in every spatial Sobolev order.

def EulerOrdinarySobolev.IsSmoothProjectedEuler {T : ℝ} {hT : 0 ≤ T} (A : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : Prop

Is smooth projected euler as an element of Prop.

Equations

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

noncomputable def EulerOrdinarySobolev.evolutionOfProjectedEquation {T : ℝ} {hT : 0 ≤ T} (A : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : IsSmoothProjectedEuler A) : Evolution T hT

Evolution of projected equation, 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.Evolution.isSmoothProjectedEuler {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (hpos : 0 < T) : IsSmoothProjectedEuler U.velocity

theorem EulerOrdinarySobolev.exists_evolution_iff_projected {T : ℝ} {hT : 0 ≤ T} (hpos : 0 < T) (A : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : (∃ (U : Evolution T hT), U.velocity = A) ↔ IsSmoothProjectedEuler A

theorem EulerOrdinarySobolev.Evolution.sobolevTimeDerivative {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (q : ℕ) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (EulerSmoothFieldSobolevTime.sobolevPath U.velocity ⋯ q)) ((EulerSmoothFieldSobolevTime.sobolevPath U.derivative ⋯ q) t) (Set.Icc 0 T) ↑t

theorem EulerOrdinarySobolev.Evolution.sobolevSolutionClass {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (q : ℕ) : Continuous ⇑(EulerSmoothFieldSobolevTime.sobolevPath U.velocity ⋯ q) ∧ Continuous ⇑(EulerSmoothFieldSobolevTime.sobolevPath U.derivative ⋯ q) ∧ ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (EulerSmoothFieldSobolevTime.sobolevPath U.velocity ⋯ q)) ((EulerSmoothFieldSobolevTime.sobolevPath U.derivative ⋯ q) t) (Set.Icc 0 T) ↑t

theorem EulerOrdinarySobolev.instOrdinaryEulerClassicalClass1 : Fact (0 < 1)

noncomputable def EulerOrdinarySobolev.scalarEulerForce (A B : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

The force obtained from the actual velocity and its actual time derivative.

Equations

• EulerOrdinarySobolev.scalarEulerForce A B = EulerOrdinarySobolev.fieldNeg (B.addField (EulerOrdinarySobolev.advectionField A A))

theorem EulerOrdinarySobolev.scalarEulerForce_field (A B : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) : (scalarEulerForce A B).field x = -(B.field x + (fderiv ℝ A.field x) (A.field x))

theorem EulerOrdinarySobolev.scalarEulerForce_continuous {T : ℝ} (A B : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (A t).jetLp n) (hB : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (B t).jetLp n) (n : ℕ) : Continuous fun (t : ↑(Set.Icc 0 T)) => (scalarEulerForce (A t) (B t)).jetLp n

theorem EulerOrdinarySobolev.isSmoothProjectedEuler_of_scalarEuler {T : ℝ} {hT : 0 ≤ T} (A B : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (A t).jetLp n) (hd : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T), HasDerivAt (fun (r : ℝ) => (A (Set.projIcc 0 T hT r)).toLp) (B ⟨t, ⋯⟩).toLp t) (p : ℝ → EulerSmoothLimit.Space → ℝ) (hdiv : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence (A t).field x = 0) (hp : ∀ t ∈ Set.Ioo 0 T, Differentiable ℝ (p t)) (he : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : EulerSmoothLimit.Space), (B ⟨t, ⋯⟩).field x + (fderiv ℝ (A ⟨t, ⋯⟩).field x) ((A ⟨t, ⋯⟩).field x) + gradient (p t) x = 0) : IsSmoothProjectedEuler A

An ordinary scalar Euler equation implies the actual projected L² equation. Spatial differentiability of pressure is used only at interior times.

noncomputable def EulerOrdinarySobolev.evolutionOfScalarEuler {T : ℝ} {hT : 0 ≤ T} (A B : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (A t).jetLp n) (hd : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T), HasDerivAt (fun (r : ℝ) => (A (Set.projIcc 0 T hT r)).toLp) (B ⟨t, ⋯⟩).toLp t) (p : ℝ → EulerSmoothLimit.Space → ℝ) (hdiv : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence (A t).field x = 0) (hp : ∀ t ∈ Set.Ioo 0 T, Differentiable ℝ (p t)) (he : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : EulerSmoothLimit.Space), (B ⟨t, ⋯⟩).field x + (fderiv ℝ (A ⟨t, ⋯⟩).field x) ((A ⟨t, ⋯⟩).field x) + gradient (p t) x = 0) : Evolution T hT

Evolution of scalar euler, given by evolutionOfProjectedEquation A (isSmoothProjectedEuler_of_scalarEuler A B hA hd p hdiv hp he).

Equations

• EulerOrdinarySobolev.evolutionOfScalarEuler A B hA hd p hdiv hp he = EulerOrdinarySobolev.evolutionOfProjectedEquation A ⋯

theorem EulerOrdinarySobolev.evolutionOfScalarEuler_velocity {T : ℝ} {hT : 0 ≤ T} (A B : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (A t).jetLp n) (hd : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T), HasDerivAt (fun (r : ℝ) => (A (Set.projIcc 0 T hT r)).toLp) (B ⟨t, ⋯⟩).toLp t) (p : ℝ → EulerSmoothLimit.Space → ℝ) (hdiv : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence (A t).field x = 0) (hp : ∀ t ∈ Set.Ioo 0 T, Differentiable ℝ (p t)) (he : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : EulerSmoothLimit.Space), (B ⟨t, ⋯⟩).field x + (fderiv ℝ (A ⟨t, ⋯⟩).field x) ((A ⟨t, ⋯⟩).field x) + gradient (p t) x = 0) : (evolutionOfScalarEuler A B hA hd p hdiv hp he).velocity = A

theorem EulerOrdinarySobolev.evolutionOfScalarEuler_derivative {T : ℝ} {hT : 0 ≤ T} (A B : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (A t).jetLp n) (hB : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (B t).jetLp n) (hd : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T), HasDerivAt (fun (r : ℝ) => (A (Set.projIcc 0 T hT r)).toLp) (B ⟨t, ⋯⟩).toLp t) (p : ℝ → EulerSmoothLimit.Space → ℝ) (hdiv : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence (A t).field x = 0) (hp : ∀ t ∈ Set.Ioo 0 T, Differentiable ℝ (p t)) (he : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : EulerSmoothLimit.Space), (B ⟨t, ⋯⟩).field x + (fderiv ℝ (A ⟨t, ⋯⟩).field x) ((A ⟨t, ⋯⟩).field x) + gradient (p t) x = 0) (hpos : 0 < T) (t : ↑(Set.Icc 0 T)) : (evolutionOfScalarEuler A B hA hd p hdiv hp he).derivative t = B t

theorem EulerOrdinarySobolev.evolutionOfScalarEuler_pressureForce {T : ℝ} {hT : 0 ≤ T} (A B : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (A t).jetLp n) (hB : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (B t).jetLp n) (hd : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T), HasDerivAt (fun (r : ℝ) => (A (Set.projIcc 0 T hT r)).toLp) (B ⟨t, ⋯⟩).toLp t) (p : ℝ → EulerSmoothLimit.Space → ℝ) (hdiv : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence (A t).field x = 0) (hp : ∀ t ∈ Set.Ioo 0 T, Differentiable ℝ (p t)) (he : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : EulerSmoothLimit.Space), (B ⟨t, ⋯⟩).field x + (fderiv ℝ (A ⟨t, ⋯⟩).field x) ((A ⟨t, ⋯⟩).field x) + gradient (p t) x = 0) (hpos : 0 < T) (t : ↑(Set.Icc 0 T)) : (evolutionOfScalarEuler A B hA hd p hdiv hp he).pressureForce t = scalarEulerForce (A t) (B t)

theorem EulerOrdinarySobolev.evolutionOfScalarEuler_scalarPressure {T : ℝ} {hT : 0 ≤ T} (A B : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (A t).jetLp n) (hB : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (B t).jetLp n) (hd : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T), HasDerivAt (fun (r : ℝ) => (A (Set.projIcc 0 T hT r)).toLp) (B ⟨t, ⋯⟩).toLp t) (p : ℝ → EulerSmoothLimit.Space → ℝ) (hdiv : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence (A t).field x = 0) (hp : ∀ t ∈ Set.Ioo 0 T, Differentiable ℝ (p t)) (he : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : EulerSmoothLimit.Space), (B ⟨t, ⋯⟩).field x + (fderiv ℝ (A ⟨t, ⋯⟩).field x) ((A ⟨t, ⋯⟩).field x) + gradient (p t) x = 0) (hpos : 0 < T) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : EulerSmoothLimit.Space) : (evolutionOfScalarEuler A B hA hd p hdiv hp he).scalarPressure ⟨t, ⋯⟩ x = p t x - p t 0

theorem EulerOrdinarySobolev.l2_timeDerivative_of_sobolev {T : ℝ} {hT : 0 ≤ T} (A B : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (A t).jetLp n) (hB : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (B t).jetLp n) (q : ℕ) (hd : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T), HasDerivAt (EulerVolterraConvolution.extendPath T hT (EulerSmoothFieldSobolevTime.sobolevPath A hA q)) ((EulerSmoothFieldSobolevTime.sobolevPath B hB q) ⟨t, ⋯⟩) t) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (fun (r : ℝ) => (A (Set.projIcc 0 T hT r)).toLp) (B ⟨t, ⋯⟩).toLp t

A strong time derivative in any genuine spatial Sobolev order gives the L² derivative used above. In the source class one can take order two.

def EulerOrdinarySobolev.IsSmoothScalarEuler {T : ℝ} {hT : 0 ≤ T} (A : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : Prop

The scalar-pressure form of the smooth ordinary Euler class. The all-order spatial paths represent C H^m for every finite m. A single strong L² time law and the continuous all-order derivative paths imply the strong time law in every Sobolev order by sobolev_derivative_of_l2. No norm, time regularity, or normalization is imposed on the scalar pressure.

Equations

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

theorem EulerOrdinarySobolev.isSmoothScalarEuler_of_sobolev {T : ℝ} {hT : 0 ≤ T} (A B : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (A t).jetLp n) (hB : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (B t).jetLp n) (q : ℕ) (hd : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T), HasDerivAt (EulerVolterraConvolution.extendPath T hT (EulerSmoothFieldSobolevTime.sobolevPath A hA q)) ((EulerSmoothFieldSobolevTime.sobolevPath B hB q) ⟨t, ⋯⟩) t) (p : ℝ → EulerSmoothLimit.Space → ℝ) (hdiv : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence (A t).field x = 0) (hp : ∀ t ∈ Set.Ioo 0 T, Differentiable ℝ (p t)) (he : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : EulerSmoothLimit.Space), (B ⟨t, ⋯⟩).field x + (fderiv ℝ (A ⟨t, ⋯⟩).field x) ((A ⟨t, ⋯⟩).field x) + gradient (p t) x = 0) : IsSmoothScalarEuler A

theorem EulerOrdinarySobolev.SobolevTower.isSmoothScalarEuler {T : ℝ} {hT : 0 ≤ T} (A B : SobolevTower T) (hd : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T), HasDerivAt (EulerVolterraConvolution.extendPath T hT (A.realization 2)) ((B.realization 2) ⟨t, ⋯⟩) t) (p : ℝ → EulerSmoothLimit.Space → ℝ) (hdiv : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence (A.smoothField t).field x = 0) (hp : ∀ t ∈ Set.Ioo 0 T, Differentiable ℝ (p t)) (he : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (x : EulerSmoothLimit.Space), (B.smoothField ⟨t, ⋯⟩).field x + (fderiv ℝ (A.smoothField ⟨t, ⋯⟩).field x) ((A.smoothField ⟨t, ⋯⟩).field x) + gradient (p t) x = 0) : IsSmoothScalarEuler A.smoothField

Starting from genuine continuous Sobolev realizations requires no preselected smooth representative or pressure-force path. The order-two time law is part of the source's C¹ H^(m-1) condition at m=3; the continuous realizations of the derivative come from its higher orders.

theorem EulerOrdinarySobolev.scalarEuler_iff_projected {T : ℝ} {hT : 0 ≤ T} (A : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : IsSmoothScalarEuler A ↔ IsSmoothProjectedEuler A

theorem EulerOrdinarySobolev.exists_evolution_iff_scalar {T : ℝ} {hT : 0 ≤ T} (hpos : 0 < T) (A : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : (∃ (U : Evolution T hT), U.velocity = A) ↔ IsSmoothScalarEuler A