A common-interval Euler limit constructed from genuine smooth Euler evolutions. The only compactness inputs are actual uniform Sobolev bounds and L² Cauchy convergence. The nonlinear term, pressure, and time equation are all recovered in the proof.

theorem EulerOrdinarySobolev.SmoothLimitData.field_mem_solenoidal {T : ℝ} {hT : 0 ≤ T} {V : ℕ → Evolution T hT} (L : SmoothLimitData (fun (k : ℕ) => (V k).velocity) ⋯) (t : ↑(Set.Icc 0 T)) : (L.field t).toLp ∈ EulerMeanSolenoidal.solenoidalSpace

theorem EulerOrdinarySobolev.SmoothLimitData.field_integral_equation {T : ℝ} {hT : 0 ≤ T} {V : ℕ → Evolution T hT} (L : SmoothLimitData (fun (k : ℕ) => (V k).velocity) ⋯) (hpos : 0 < T) (M : ℝ) (hb : ∀ (k : ℕ) (t : ↑(Set.Icc 0 T)), tensorNorm 3 ((V k).velocity t) ≤ M) (t : ↑(Set.Icc 0 T)) : (L.field t).toLp = (L.field ⟨0, ⋯⟩).toLp + ((EulerContinuousTimeIntegral.integral T hT) (projectedRhsPath L.field ⋯)) t

theorem EulerOrdinarySobolev.SmoothLimitData.field_hasDerivWithinAt {T : ℝ} {hT : 0 ≤ T} {V : ℕ → Evolution T hT} (L : SmoothLimitData (fun (k : ℕ) => (V k).velocity) ⋯) (hpos : 0 < T) (M : ℝ) (hb : ∀ (k : ℕ) (t : ↑(Set.Icc 0 T)), tensorNorm 3 ((V k).velocity t) ≤ M) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (fun (r : ℝ) => (L.field (Set.projIcc 0 T hT r)).toLp) (projectedRhs (L.field t)).toLp (Set.Icc 0 T) ↑t

noncomputable def EulerOrdinarySobolev.SmoothLimitData.toEvolution {T : ℝ} {hT : 0 ≤ T} {V : ℕ → Evolution T hT} (L : SmoothLimitData (fun (k : ℕ) => (V k).velocity) ⋯) (hpos : 0 < T) (M : ℝ) (hb : ∀ (k : ℕ) (t : ↑(Set.Icc 0 T)), tensorNorm 3 ((V k).velocity t) ≤ M) : Evolution T hT

To evolution, 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.

noncomputable def EulerOrdinarySobolev.eulerLimitData {T : ℝ} {hT : 0 ≤ T} (V : ℕ → Evolution T hT) (hb : ∀ (q : ℕ), ∃ (M : ℝ), ∀ (k : ℕ) (t : ↑(Set.Icc 0 T)), tensorNorm q ((V k).velocity t) ≤ M) (h0 : CauchySeq fun (k : ℕ) => fieldPath (V k).velocity ⋯) : SmoothLimitData (fun (k : ℕ) => (V k).velocity) ⋯

Euler limit data, given by smoothLimitData hT (fun k => (V k).velocity) (fun k => (V k).velocity_continuous) hb h0.

Equations

• EulerOrdinarySobolev.eulerLimitData V hb h0 = EulerOrdinarySobolev.smoothLimitData hT (fun (k : ℕ) => (V k).velocity) ⋯ hb h0

noncomputable def EulerOrdinarySobolev.limitEvolution {T : ℝ} {hT : 0 ≤ T} (V : ℕ → Evolution T hT) (hpos : 0 < T) (hb : ∀ (q : ℕ), ∃ (M : ℝ), ∀ (k : ℕ) (t : ↑(Set.Icc 0 T)), tensorNorm q ((V k).velocity t) ≤ M) (h0 : CauchySeq fun (k : ℕ) => fieldPath (V k).velocity ⋯) : Evolution T hT

Limit evolution, given by (eulerLimitData V hb h0).toEvolution hpos (Classical.choose (hb 3)) (Classical.choose_spec (hb 3)).

Equations

• EulerOrdinarySobolev.limitEvolution V hpos hb h0 = (EulerOrdinarySobolev.eulerLimitData V hb h0).toEvolution hpos (Classical.choose ⋯) ⋯

theorem EulerOrdinarySobolev.limitEvolution_jet_convergence {T : ℝ} {hT : 0 ≤ T} (V : ℕ → Evolution T hT) (hpos : 0 < T) (hb : ∀ (q : ℕ), ∃ (M : ℝ), ∀ (k : ℕ) (t : ↑(Set.Icc 0 T)), tensorNorm q ((V k).velocity t) ≤ M) (h0 : CauchySeq fun (k : ℕ) => fieldPath (V k).velocity ⋯) (q : ℕ) : Filter.Tendsto (fun (k : ℕ) => jetPath (V k).velocity ⋯ q) Filter.atTop (nhds (jetPath (limitEvolution V hpos hb h0).velocity ⋯ q))

theorem EulerOrdinarySobolev.limitEvolution_initial {T : ℝ} {hT : 0 ≤ T} (V : ℕ → Evolution T hT) (hpos : 0 < T) (hb : ∀ (q : ℕ), ∃ (M : ℝ), ∀ (k : ℕ) (t : ↑(Set.Icc 0 T)), tensorNorm q ((V k).velocity t) ≤ M) (h0 : CauchySeq fun (k : ℕ) => fieldPath (V k).velocity ⋯) (u0 : ↥EulerMeanSolenoidal.L2) (hu0 : Filter.Tendsto (fun (k : ℕ) => ((V k).velocity ⟨0, ⋯⟩).toLp) Filter.atTop (nhds u0)) : ((limitEvolution V hpos hb h0).velocity ⟨0, ⋯⟩).toLp = u0

theorem EulerOrdinarySobolev.limitEvolution_bound {T : ℝ} {hT : 0 ≤ T} (V : ℕ → Evolution T hT) (hpos : 0 < T) (hb : ∀ (q : ℕ), ∃ (M : ℝ), ∀ (k : ℕ) (t : ↑(Set.Icc 0 T)), tensorNorm q ((V k).velocity t) ≤ M) (h0 : CauchySeq fun (k : ℕ) => fieldPath (V k).velocity ⋯) (q : ℕ) (M : ℝ) (hM : ∀ (k : ℕ) (t : ↑(Set.Icc 0 T)), tensorNorm q ((V k).velocity t) ≤ M) (t : ↑(Set.Icc 0 T)) : tensorNorm q ((limitEvolution V hpos hb h0).velocity t) ≤ M

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

Scalar pressure, given by EulerCanonicalGraphPotential.radialPotential (U.pressureForce t).field.

Equations

• U.scalarPressure t = EulerCanonicalGraphPotential.radialPotential (U.pressureForce t).field

theorem EulerOrdinarySobolev.Evolution.scalarPressure_spec {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (t : ↑(Set.Icc 0 T)) : ContDiff ℝ (↑⊤) (U.scalarPressure t) ∧ U.scalarPressure t 0 = 0 ∧ ∀ (x : EulerSmoothLimit.Space), _root_.gradient (U.scalarPressure t) x = (U.pressureForce t).field x