Repackaging the reference's ordinary functions as the development's smooth L² fields. The scalar Euler equations and time-regularity hypotheses coincide.

theorem Euler.ComparatorBridge.toL2_field (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : toL2 A.field = A.toLp

theorem Euler.ComparatorBridge.toL2_jet (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (n : ℕ) : toL2 (iteratedFDeriv ℝ n A.field) = A.jetLp n

theorem Euler.ComparatorBridge.sobolevSmoothOn_of_path {I : Set ℝ} (A : ↑I → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : ↑I) => (A t).jetLp n) (v : EulerSmoothLimit.Space → ℝ → EulerSmoothLimit.Space) (hv : ∀ (t : ↑I), (fun (x : EulerSmoothLimit.Space) => v x ↑t) = (A t).field) : SobolevSmoothOn I v

def Euler.SobolevSmoothOn.field {I : Set ℝ} {v : EulerSmoothLimit.Space → ℝ → EulerSmoothLimit.Space} (h : SobolevSmoothOn I v) (t : ↑I) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Field, bundling field, smooth, integrable.

Equations

• h.field t = { field := fun (x : EulerSmoothLimit.Space) => v x ↑t, smooth := ⋯, integrable := ⋯ }

theorem Euler.SobolevSmoothOn.field_toLp {I : Set ℝ} {v : EulerSmoothLimit.Space → ℝ → EulerSmoothLimit.Space} (h : SobolevSmoothOn I v) (t : ↑I) : (h.field t).toLp = toL2 fun (x : EuclideanSpace ℝ (Fin 3)) => v x ↑t

theorem Euler.SobolevSmoothOn.field_jetLp {I : Set ℝ} {v : EulerSmoothLimit.Space → ℝ → EulerSmoothLimit.Space} (h : SobolevSmoothOn I v) (t : ↑I) (n : ℕ) : (h.field t).jetLp n = toL2 (iteratedFDeriv ℝ n fun (x : EuclideanSpace ℝ (Fin 3)) => v x ↑t)

theorem Euler.SobolevSmoothOn.field_continuous {I : Set ℝ} {v : EulerSmoothLimit.Space → ℝ → EulerSmoothLimit.Space} (h : SobolevSmoothOn I v) (n : ℕ) : Continuous fun (t : ↑I) => (h.field t).jetLp n

theorem Euler.ComparatorBridge.hasScalarEulerEvolution_of_sobolev {A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} {T : ℝ} (hT : 0 < T) {v : EulerSmoothLimit.Space → ℝ → EulerSmoothLimit.Space} {p : EulerSmoothLimit.Space → ℝ → ℝ} (h : EulerSobolevExistenceAndSmoothnessR3On (Set.Icc 0 T) A.field v p) : EulerOrdinarySobolev.HasScalarEulerEvolution A T

noncomputable def Euler.ComparatorBridge.evolutionVelocity {T : ℝ} {hT : 0 ≤ T} (U : EulerOrdinarySobolev.Evolution T hT) (x : EulerSmoothLimit.Space) (t : ℝ) : EulerSmoothLimit.Space

Evolution velocity, given by (U.velocity (projIcc 0 T hT t)).field x.

Equations

• Euler.ComparatorBridge.evolutionVelocity U x t = (U.velocity (Set.projIcc 0 T hT t)).field x

noncomputable def Euler.ComparatorBridge.evolutionPressure {T : ℝ} {hT : 0 ≤ T} (U : EulerOrdinarySobolev.Evolution T hT) (x : EulerSmoothLimit.Space) (t : ℝ) : ℝ

Evolution pressure, given by U.scalarPressure (projIcc 0 T hT t) x.

Equations

• Euler.ComparatorBridge.evolutionPressure U x t = U.scalarPressure (Set.projIcc 0 T hT t) x

theorem Euler.ComparatorBridge.evolution_sobolevSolution {T : ℝ} {hT : 0 ≤ T} (U : EulerOrdinarySobolev.Evolution T hT) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hinit : U.velocity ⟨0, ⋯⟩ = A) : EulerSobolevExistenceAndSmoothnessR3On (Set.Icc 0 T) A.field (evolutionVelocity U) (evolutionPressure U)

theorem Euler.ComparatorBridge.exists_sobolevSolution_iff (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (T : ℝ) (hT : 0 < T) : (∃ (v : EuclideanSpace ℝ (Fin 3) → ℝ → EuclideanSpace ℝ (Fin 3)) (p : EuclideanSpace ℝ (Fin 3) → ℝ → ℝ), EulerSobolevExistenceAndSmoothnessR3On (Set.Icc 0 T) A.field v p) ↔ EulerOrdinarySobolev.HasScalarEulerEvolution A T