A concrete raw-field provider for the mean packet equation

A raw forcing is supplied only through its literal smooth L² slices. The returned velocity and normalized scalar pressure are constructed by the actual source variational solve and its genuine classical representatives. The function is total on raw fields; its PDE contract is proved precisely on the admissible domain, without a smooth time extension across endpoints.

A normalized scalar pressure for the actual mean solution

The radial integral is applied to the real F-adjoint pressure force, whose closed-gradient-space membership was proved from the actual Gram equation. The resulting scalar is spatially smooth, normalized at zero, and gives the pointwise physical equation. No scalar potential or pressure time derivative is assumed.

noncomputable def EulerMeanScalarPressure.pathRepresentative (T : ℝ) (p : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hp : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) p) (t : ↑(Set.Icc 0 T)) : EulerSmoothLimit.Space → EulerSmoothLimit.Space

The canonical smooth spatial representative of an actual continuous L² path.

Equations

• EulerMeanScalarPressure.pathRepresentative T p hp t = EulerMeanSmoothRepresentative.representative (p t) ⋯

theorem EulerMeanScalarPressure.pathRepresentative_smooth (T : ℝ) (p : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hp : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) p) (t : ↑(Set.Icc 0 T)) : ContDiff ℝ (↑⊤) (pathRepresentative T p hp t)

theorem EulerMeanScalarPressure.pathRepresentative_ae (T : ℝ) (p : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hp : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) p) (t : ↑(Set.Icc 0 T)) : ↑↑(p t) =ᵐ[MeasureTheory.volume] pathRepresentative T p hp t

theorem EulerMeanScalarPressure.pathRepresentative_continuous (T : ℝ) (p : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hp : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) p) : Continuous fun (z : ↑(Set.Icc 0 T) × EulerSmoothLimit.Space) => pathRepresentative T p hp z.1 z.2

theorem EulerMeanScalarPressure.representative_equation (B D R f : ↥EulerMeanSolenoidal.L2) (hB : EulerMeanSmoothRepresentative.SmoothOrbit B) (hD : EulerMeanSmoothRepresentative.SmoothOrbit D) (hR : EulerMeanSmoothRepresentative.SmoothOrbit R) (hf : EulerMeanSmoothRepresentative.SmoothOrbit f) (M : EulerMeanCoefficients.Field) (heq : D + (EulerMeanCoefficients.multiplier M) B + R = f) (x : EulerSmoothLimit.Space) : EulerMeanSmoothRepresentative.representative D hD x + (M x) (EulerMeanSmoothRepresentative.representative B hB x) + EulerMeanSmoothRepresentative.representative R hR x = EulerMeanSmoothRepresentative.representative f hf x

An actual L² equation between continuous spatial representatives holds everywhere.

theorem EulerMeanScalarPressure.pathRepresentative_equation (T : ℝ) (B D R f : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hB : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) B) (hD : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) D) (hR : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) R) (hf : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) f) (M : C(↑(Set.Icc 0 T), EulerMeanCoefficients.Field)) (heq : ∀ (t : ↑(Set.Icc 0 T)), D t + (EulerMeanCoefficients.multiplier (M t)) (B t) + R t = f t) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : pathRepresentative T D hD t x + ((M t) x) (pathRepresentative T B hB t x) + pathRepresentative T R hR t x = pathRepresentative T f hf t x

noncomputable def EulerMeanScalarPressure.pressureScalar (T : ℝ) (hT : 0 ≤ T) (F F₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) {A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2} {L : ℝ} {u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)} (s : EulerMeanVariationalInverse.StrongMeanEvolution T hT FInv (EulerMeanCoefficients.operatorPath T F.field) (EulerMeanCoefficients.operatorPath T F₁.field) A L u f) (c : ℝ) (hc : 0 < c) (hLower : ∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((EulerMeanVariationalInverse.solenoidalFrame T (EulerMeanCoefficients.operatorPath T F.field)) t) v‖ ^ 2) (fC : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hR : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) (s.pressurePath c hc hLower fC)) (t : ↑(Set.Icc 0 T)) : EulerSmoothLimit.Space → ℝ

The concrete normalized scalar mean pressure, constructed by a radial integral.

Equations

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

theorem EulerMeanScalarPressure.pressureScalar_spec (T : ℝ) (hT : 0 ≤ T) (F F₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) {A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2} {L : ℝ} {u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)} (s : EulerMeanVariationalInverse.StrongMeanEvolution T hT FInv (EulerMeanCoefficients.operatorPath T F.field) (EulerMeanCoefficients.operatorPath T F₁.field) A L u f) (c : ℝ) (hc : 0 < c) (hLower : ∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((EulerMeanVariationalInverse.solenoidalFrame T (EulerMeanCoefficients.operatorPath T F.field)) t) v‖ ^ 2) (fC : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hR : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) (s.pressurePath c hc hLower fC)) (t : ↑(Set.Icc 0 T)) : ContDiff ℝ (↑⊤) (pressureScalar T hT F F₁ FInv s c hc hLower fC hR t) ∧ pressureScalar T hT F F₁ FInv s c hc hLower fC hR t 0 = 0 ∧ ∀ (x : EulerSmoothLimit.Space), gradient (pressureScalar T hT F F₁ FInv s c hc hLower fC hR t) x = (ContinuousLinearMap.adjoint ((F.field t) x)) (pathRepresentative T (s.pressurePath c hc hLower fC) hR t x)

Spatial smoothness, normalization, and exact gradient of the constructed pressure.

noncomputable def EulerMeanScalarPressure.pressureProfile (T : ℝ) (hT : 0 ≤ T) (F F₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) {A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2} {L : ℝ} {u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)} (s : EulerMeanVariationalInverse.StrongMeanEvolution T hT FInv (EulerMeanCoefficients.operatorPath T F.field) (EulerMeanCoefficients.operatorPath T F₁.field) A L u f) (c : ℝ) (hc : 0 < c) (hLower : ∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((EulerMeanVariationalInverse.solenoidalFrame T (EulerMeanCoefficients.operatorPath T F.field)) t) v‖ ^ 2) (fC : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hR : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) (s.pressurePath c hc hLower fC)) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (_θ : ℝ) : ℝ

The source mean pressure has no angular dependence.

Equations

• EulerMeanScalarPressure.pressureProfile T hT F F₁ FInv s c hc hLower fC hR t x _θ = EulerMeanScalarPressure.pressureScalar T hT F F₁ FInv s c hc hLower fC hR t x

theorem EulerMeanScalarPressure.pressureProfile_angle_derivative (T : ℝ) (hT : 0 ≤ T) (F F₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) {A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2} {L : ℝ} {u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)} (s : EulerMeanVariationalInverse.StrongMeanEvolution T hT FInv (EulerMeanCoefficients.operatorPath T F.field) (EulerMeanCoefficients.operatorPath T F₁.field) A L u f) (c : ℝ) (hc : 0 < c) (hLower : ∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((EulerMeanVariationalInverse.solenoidalFrame T (EulerMeanCoefficients.operatorPath T F.field)) t) v‖ ^ 2) (fC : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hR : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) (s.pressurePath c hc hLower fC)) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : HasDerivAt (pressureProfile T hT F F₁ FInv s c hc hLower fC hR t x) 0 θ

theorem EulerMeanScalarPressure.pressureScalar_physicalGradient (T : ℝ) (hT : 0 ≤ T) (F F₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) {A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2} {L : ℝ} {u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)} (s : EulerMeanVariationalInverse.StrongMeanEvolution T hT FInv (EulerMeanCoefficients.operatorPath T F.field) (EulerMeanCoefficients.operatorPath T F₁.field) A L u f) (c : ℝ) (hc : 0 < c) (hLower : ∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((EulerMeanVariationalInverse.solenoidalFrame T (EulerMeanCoefficients.operatorPath T F.field)) t) v‖ ^ 2) (fC : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hR : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) (s.pressurePath c hc hLower fC)) (Finv : C(↑(Set.Icc 0 T), EulerMeanCoefficients.Field)) (hFinv : ∀ (t : ↑(Set.Icc 0 T)) (x v : EulerSmoothLimit.Space), ((F.field t) x) (((Finv t) x) v) = v) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : (ContinuousLinearMap.adjoint ((Finv t) x)) (gradient (pressureScalar T hT F F₁ FInv s c hc hLower fC hR t) x) = pathRepresentative T (s.pressurePath c hc hLower fC) hR t x

The physical pressure force is exactly the actual residual, because the inverse-transpose cancels the transpose of the given frame.

theorem EulerMeanScalarPressure.pressureScalar_equation (T : ℝ) (hT : 0 ≤ T) (F F₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) {A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2} {L : ℝ} {u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)} (s : EulerMeanVariationalInverse.StrongMeanEvolution T hT FInv (EulerMeanCoefficients.operatorPath T F.field) (EulerMeanCoefficients.operatorPath T F₁.field) A L u f) (c : ℝ) (hc : 0 < c) (hLower : ∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((EulerMeanVariationalInverse.solenoidalFrame T (EulerMeanCoefficients.operatorPath T F.field)) t) v‖ ^ 2) (fC : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2)) (hR : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) (s.pressurePath c hc hLower fC)) (hTpos : 0 < T) (hFTime : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (EulerMeanCoefficients.operatorPath T F.field)) ((EulerMeanCoefficients.operatorPath T F₁.field) t) (Set.Icc 0 T) ↑t) (M : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (hMF : ∀ (t : ↑(Set.Icc 0 T)) (x v : EulerSmoothLimit.Space), ((F₁.field t) x) v = ((M.field t) x) (((F.field t) x) v)) (Finv : C(↑(Set.Icc 0 T), EulerMeanCoefficients.Field)) (hFinv : ∀ (t : ↑(Set.Icc 0 T)) (x v : EulerSmoothLimit.Space), ((F.field t) x) (((Finv t) x) v) = v) (hB : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) s.continuousVelocity) (hD : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) (s.classicalPhysicalDerivative c hc hLower fC)) (hfC : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) fC) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : pathRepresentative T (s.classicalPhysicalDerivative c hc hLower fC) hD t x + ((M.field t) x) (pathRepresentative T s.continuousVelocity hB t x) + (ContinuousLinearMap.adjoint ((Finv t) x)) (gradient (pressureScalar T hT F F₁ FInv s c hc hLower fC hR t) x) = pathRepresentative T fC hfC t x

The constructed pressure gives the literal pointwise source equation.

noncomputable def EulerMeanPacketProvider.Data.clamp (D : Data) (t : ℝ) : ↑(Set.Icc 0 D.T)

A continuous closed-interval retraction, used only to define the raw field outside its domain.

Equations

• D.clamp t = Set.projIcc 0 D.T ⋯ t

@[simp]

theorem EulerMeanPacketProvider.Data.clamp_coe (D : Data) (t : ↑(Set.Icc 0 D.T)) : D.clamp ↑t = t

noncomputable def EulerMeanPacketProvider.Data.inverseFrame (D : Data) (z : EulerPacketPointJets.Domain) : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space

Inverse Frame, given by D.FInv (D.clamp z.1) z.2.1.

Equations

• D.inverseFrame z = (D.FInv (D.clamp z.1)) z.2.1

noncomputable def EulerMeanPacketProvider.Data.strain (D : Data) (z : EulerPacketPointJets.Domain) : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space

Strain, given by D.M.field (D.clamp z.1) z.2.1.

Equations

• D.strain z = (D.M.field (D.clamp z.1)) z.2.1

noncomputable def EulerMeanPacketProvider.Forcing.vector {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) : EulerPacketProfileRecursion.VectorField

Literal velocity returned by the genuine mean inverse.

Equations

• G.vector z = EulerMeanScalarPressure.pathRepresentative D.T G.velocityPath ⋯ (D.clamp z.1) z.2.1

noncomputable def EulerMeanPacketProvider.Forcing.vectorDerivative {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) : EulerPacketProfileRecursion.VectorField

Literal continuous time derivative of the velocity on the source interval.

Equations

• G.vectorDerivative z = EulerMeanScalarPressure.pathRepresentative D.T G.derivativePath ⋯ (D.clamp z.1) z.2.1

noncomputable def EulerMeanPacketProvider.Forcing.scalar {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) : EulerPacketProfileRecursion.ScalarField

The normalized scalar pressure returned by the actual radial construction.

Equations

• G.scalar z = EulerMeanScalarPressure.pressureScalar D.T ⋯ D.F D.F₁ D.opInv G.solution D.frameLower ⋯ ⋯ G.path ⋯ (D.clamp z.1) z.2.1

theorem EulerMeanPacketProvider.Forcing.forcingRepresentative_eq {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : EulerMeanScalarPressure.pathRepresentative D.T G.path ⋯ t x = raw (↑t, x, θ)

The representative of the prescribed forcing is the original raw field, pointwise.

theorem EulerMeanPacketProvider.Forcing.vector_angle_independent {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (t : ℝ) (x : EulerSmoothLimit.Space) (θ η : ℝ) : G.vector (t, x, θ) = G.vector (t, x, η)

theorem EulerMeanPacketProvider.Forcing.scalar_angle_independent {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (t : ℝ) (x : EulerSmoothLimit.Space) (θ η : ℝ) : G.scalar (t, x, θ) = G.scalar (t, x, η)

theorem EulerMeanPacketProvider.Forcing.scalar_normalized {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (t θ : ℝ) : G.scalar (t, 0, θ) = 0

theorem EulerMeanPacketProvider.Forcing.vector_spatial_smooth {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (t : ℝ) : ContDiff ℝ ↑⊤ fun (y : EulerSmoothLimit.Space × ℝ) => G.vector (t, y)

Actual spatial and angular regularity at every time.

theorem EulerMeanPacketProvider.Forcing.vectorDerivative_spatial_smooth {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (t : ℝ) : ContDiff ℝ ↑⊤ fun (y : EulerSmoothLimit.Space × ℝ) => G.vectorDerivative (t, y)

theorem EulerMeanPacketProvider.Forcing.scalar_spatial_smooth {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (t : ℝ) : ContDiff ℝ ↑⊤ fun (y : EulerSmoothLimit.Space × ℝ) => G.scalar (t, y)

theorem EulerMeanPacketProvider.Forcing.vector_hasDerivWithinAt {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : HasDerivWithinAt (fun (r : ℝ) => G.vector (r, x, θ)) (G.vectorDerivative (↑t, x, θ)) (Set.Icc 0 D.T) ↑t

The returned velocity has the genuine within-time derivative at both endpoints too.

theorem EulerMeanPacketProvider.Forcing.equation {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : G.vectorDerivative (↑t, x, θ) + (D.strain (↑t, x, θ)) (G.vector (↑t, x, θ)) + (ContinuousLinearMap.adjoint (D.inverseFrame (↑t, x, θ))) (gradient (fun (y : EulerSmoothLimit.Space) => G.scalar (↑t, y, θ)) x) = raw (↑t, x, θ)

The genuine raw mean equation, with the normalized actual scalar pressure.

noncomputable def EulerMeanPacketProvider.meanSolve (D : Data) (raw : EulerPacketProfileRecursion.VectorField) : EulerPacketProfileRecursion.VectorField × EulerPacketProfileRecursion.ScalarField

A total raw-field operator whose correctness is required on the proved admissible domain.

Equations

• EulerMeanPacketProvider.meanSolve D raw = if h : Nonempty (EulerMeanPacketProvider.Forcing D raw) then have G := Classical.choice h; (G.vector, G.scalar) else (0, 0)

theorem EulerMeanPacketProvider.meanSolve_of_admissible (D : Data) (raw : EulerPacketProfileRecursion.VectorField) (h : Nonempty (Forcing D raw)) : meanSolve D raw = ((Classical.choice h).vector, (Classical.choice h).scalar)

theorem EulerMeanPacketProvider.meanSolve_contract (D : Data) (raw : EulerPacketProfileRecursion.VectorField) (h : Nonempty (Forcing D raw)) : ∃ (bt : EulerPacketProfileRecursion.VectorField), (∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), HasDerivWithinAt (fun (r : ℝ) => (meanSolve D raw).1 (r, x, θ)) (bt (↑t, x, θ)) (Set.Icc 0 D.T) ↑t) ∧ (∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ), bt (↑t, x, θ) + (D.strain (↑t, x, θ)) ((meanSolve D raw).1 (↑t, x, θ)) + (ContinuousLinearMap.adjoint (D.inverseFrame (↑t, x, θ))) (gradient (fun (y : EulerSmoothLimit.Space) => (meanSolve D raw).2 (↑t, y, θ)) x) = raw (↑t, x, θ)) ∧ (∀ (t : ℝ), ContDiff ℝ ↑⊤ fun (y : EulerSmoothLimit.Space × ℝ) => (meanSolve D raw).1 (t, y)) ∧ (∀ (t : ℝ), ContDiff ℝ ↑⊤ fun (y : EulerSmoothLimit.Space × ℝ) => (meanSolve D raw).2 (t, y)) ∧ ∀ (t θ : ℝ), (meanSolve D raw).2 (t, 0, θ) = 0

The total provider is backed by an actual source solve on every admissible input.