The genuine Helmholtz projection preserves ordinary smooth L² fields and continuous paths of all their jets. Euler pressure and time derivatives are recovered from velocity, not supplied as estimates.

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

Solenoidal field, given by smoothL2Field (solenoidalProjection A.toLp) (solenoidal_orbit A).

Equations

• EulerOrdinarySobolev.solenoidalField A = EulerMeanSmoothRepresentative.smoothL2Field (EulerMeanSolenoidal.solenoidalProjection A.toLp) ⋯

@[simp]

theorem EulerOrdinarySobolev.solenoidalField_toLp (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : (solenoidalField A).toLp = EulerMeanSolenoidal.solenoidalProjection A.toLp

theorem EulerOrdinarySobolev.solenoidalField_word (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) {n : ℕ} (w : Fin n → Fin 3) : (wordField (solenoidalField A) w).toLp = EulerMeanSolenoidal.solenoidalProjection (wordField A w).toLp

theorem EulerOrdinarySobolev.jetLp_eq_word_reassembly (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (n : ℕ) : A.jetLp n = (EulerLpFiniteTensor.tensorLpReassembly MeasureTheory.volume n) fun (w : Fin n → Fin 3) => (wordField A w).toLp

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

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

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

Pressure field, given by fieldSub (solenoidalField (advectionField A A)) (advectionField A A).

Equations

• EulerOrdinarySobolev.pressureField A = EulerOrdinarySobolev.fieldSub (EulerOrdinarySobolev.solenoidalField (EulerOrdinarySobolev.advectionField A A)) (EulerOrdinarySobolev.advectionField A A)

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

Projected rhs, given by fieldNeg (solenoidalField (advectionField A A)).

Equations

• EulerOrdinarySobolev.projectedRhs A = EulerOrdinarySobolev.fieldNeg (EulerOrdinarySobolev.solenoidalField (EulerOrdinarySobolev.advectionField A A))

@[simp]

theorem EulerOrdinarySobolev.projectedRhs_toLp (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : (projectedRhs A).toLp = -EulerMeanSolenoidal.solenoidalProjection (advectionField A A).toLp

@[simp]

theorem EulerOrdinarySobolev.pressureField_toLp (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : (pressureField A).toLp = EulerMeanSolenoidal.solenoidalProjection (advectionField A A).toLp - (advectionField A A).toLp

theorem EulerOrdinarySobolev.pressureField_mem_gradient (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : (pressureField A).toLp ∈ EulerMeanSolenoidal.gradientSpace

theorem EulerOrdinarySobolev.projectedRhs_field (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) : (projectedRhs A).field x = -(fderiv ℝ A.field x) (A.field x) - (pressureField A).field x

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

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

theorem EulerOrdinarySobolev.Evolution.velocityPath_extend {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) : EulerVolterraConvolution.extendPath T hT U.velocityPath = fun (r : ℝ) => (U.velocity (Set.projIcc 0 T hT r)).toLp

theorem EulerOrdinarySobolev.Evolution.velocityPath_hasDerivWithinAt {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT U.velocityPath) (U.derivative t).toLp (Set.Icc 0 T) ↑t

theorem EulerOrdinarySobolev.Evolution.derivative_mem_solenoidal {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (hpos : 0 < T) (t : ↑(Set.Icc 0 T)) : (U.derivative t).toLp ∈ EulerMeanSolenoidal.solenoidalSpace

theorem EulerOrdinarySobolev.Evolution.derivative_toLp_projected {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (hpos : 0 < T) (t : ↑(Set.Icc 0 T)) : (U.derivative t).toLp = (projectedRhs (U.velocity t)).toLp

noncomputable def EulerOrdinarySobolev.Evolution.projectedPath {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)

Projected path, given by fieldPath (fun t => projectedRhs (U.velocity t)) (projectedRhs_continuous U.velocity U.velocity_continuous).

Equations

• U.projectedPath = EulerOrdinarySobolev.fieldPath (fun (t : ↑(Set.Icc 0 T)) => EulerOrdinarySobolev.projectedRhs (U.velocity t)) ⋯

theorem EulerOrdinarySobolev.Evolution.velocity_integral_equation {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (hpos : 0 < T) : U.velocityPath = ContinuousMap.const (↑(Set.Icc 0 T)) (U.velocityPath ⟨0, ⋯⟩) + (EulerContinuousTimeIntegral.integral T hT) U.projectedPath