Passing the actual nonlinear advection and Helmholtz pressure to a strong ordinary Sobolev limit. Only a uniform H³ bound is used in the product estimate; pressure convergence is a consequence.

theorem EulerOrdinarySobolev.jetLp_fieldSub (A B : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (n : ℕ) : (fieldSub A B).jetLp n = A.jetLp n - B.jetLp n

theorem EulerOrdinarySobolev.advection_difference (A B : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : fieldSub (advectionField A A) (advectionField B B) = (advectionField (fieldSub A B) A).addField (advectionField B (fieldSub A B))

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

theorem EulerOrdinarySobolev.advection_sub_norm (A B : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (G K : ℝ) (hG : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ A.field x‖ ≤ G) (hK : ∀ (x : EulerSmoothLimit.Space), ‖B.field x‖ ≤ K) : ‖(advectionField A A).toLp - (advectionField B B).toLp‖ ≤ G * ‖A.toLp - B.toLp‖ + K * ‖A.jetLp 1 - B.jetLp 1‖

noncomputable def EulerOrdinarySobolev.advectionPath {T : ℝ} (A : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (A t).jetLp n) : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)

Advection path, given by fieldPath (fun t => advectionField (A t) (A t)) (advectionField_continuous A hA).

Equations

• EulerOrdinarySobolev.advectionPath A hA = EulerOrdinarySobolev.fieldPath (fun (t : ↑(Set.Icc 0 T)) => EulerOrdinarySobolev.advectionField (A t) (A t)) ⋯

noncomputable def EulerOrdinarySobolev.projectedRhsPath {T : ℝ} (A : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (A t).jetLp n) : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)

Projected rhs path, given by fieldPath (fun t => projectedRhs (A t)) (projectedRhs_continuous A hA).

Equations

• EulerOrdinarySobolev.projectedRhsPath A hA = EulerOrdinarySobolev.fieldPath (fun (t : ↑(Set.Icc 0 T)) => EulerOrdinarySobolev.projectedRhs (A t)) ⋯

noncomputable def EulerOrdinarySobolev.pressurePath {T : ℝ} (A : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (A t).jetLp n) : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)

Pressure path, given by fieldPath (fun t => pressureField (A t)) (pressureField_continuous A hA).

Equations

• EulerOrdinarySobolev.pressurePath A hA = EulerOrdinarySobolev.fieldPath (fun (t : ↑(Set.Icc 0 T)) => EulerOrdinarySobolev.pressureField (A t)) ⋯

theorem EulerOrdinarySobolev.projectedRhsPath_eq {T : ℝ} (A : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (A t).jetLp n) : projectedRhsPath A hA = (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (-EulerMeanSolenoidal.solenoidalProjection)) (advectionPath A hA)

theorem EulerOrdinarySobolev.pressurePath_eq {T : ℝ} (A : ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (A t).jetLp n) : pressurePath A hA = (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerMeanSolenoidal.solenoidalProjection - ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2)) (advectionPath A hA)

theorem EulerOrdinarySobolev.advectionPath_sub_norm {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) (G K : ℝ) (hG0 : 0 ≤ G) (hK0 : 0 ≤ K) (hG : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (A t).field x‖ ≤ G) (hK : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖(B t).field x‖ ≤ K) : ‖advectionPath A hA - advectionPath B hB‖ ≤ G * ‖fieldPath A hA - fieldPath B hB‖ + K * ‖jetPath A hA 1 - jetPath B hB 1‖

theorem EulerOrdinarySobolev.SmoothLimitData.advectionPath_convergence {T : ℝ} {A : ℕ → ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} {hA : ∀ (k n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (A k t).jetLp n} (L : SmoothLimitData A hA) (hT : 0 ≤ T) (M : ℝ) (hb : ∀ (k : ℕ) (t : ↑(Set.Icc 0 T)), tensorNorm 3 (A k t) ≤ M) : Filter.Tendsto (fun (k : ℕ) => advectionPath (A k) ⋯) Filter.atTop (nhds (advectionPath L.field ⋯))

theorem EulerOrdinarySobolev.SmoothLimitData.projectedRhsPath_convergence {T : ℝ} {A : ℕ → ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} {hA : ∀ (k n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (A k t).jetLp n} (L : SmoothLimitData A hA) (hT : 0 ≤ T) (M : ℝ) (hb : ∀ (k : ℕ) (t : ↑(Set.Icc 0 T)), tensorNorm 3 (A k t) ≤ M) : Filter.Tendsto (fun (k : ℕ) => projectedRhsPath (A k) ⋯) Filter.atTop (nhds (projectedRhsPath L.field ⋯))

theorem EulerOrdinarySobolev.SmoothLimitData.pressurePath_convergence {T : ℝ} {A : ℕ → ↑(Set.Icc 0 T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space} {hA : ∀ (k n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (A k t).jetLp n} (L : SmoothLimitData A hA) (hT : 0 ≤ T) (M : ℝ) (hb : ∀ (k : ℕ) (t : ↑(Set.Icc 0 T)), tensorNorm 3 (A k t) ≤ M) : Filter.Tendsto (fun (k : ℕ) => pressurePath (A k) ⋯) Filter.atTop (nhds (pressurePath L.field ⋯))