The actual normalized pressure in the transverse forward equation

The scalar L² primitive and the literal periodic integral are identified. Its angular derivative closes equation (11) for the constructed physical field. The pressure is smooth in the cylinder variables, has zero angular mean, and retains the same spatial support.

Genuine mixed regularity of the solved physical forward fields

The actual coordinate solve and its ordinary right side have smooth mixed translation orbits. Applying the physical frame then gives this same regularity for the velocity and its true time derivative. These statements are proved from the data, not included in the solution interface.

Actual unnormalized forward solutions have smooth mixed translation orbits.

theorem EulerLpCylinderRegularForward.unweighted_solution_contDiff (period : ℝ) [Fact (0 < period)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (T : ℝ) (hT : 0 ≤ T) (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (B : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (V →L[ℝ] V))) (hB : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath B)) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period V S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported period V S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) ↑a₀) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) ((EulerLpCylinderCoefficients.constructedEvolution period S hS T hT B).solution f a₀))

The constructed unnormalized path is genuinely smooth in all covering parameters. This qualitative statement needs no propagator bound or smoothness of a time profile.

theorem EulerSourceCylinderEquation.coordinates_contDiff (period : ℝ) [Fact (0 < period)] {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period E S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported period U S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) ↑a₀) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) (coordinates period S hS T hT Q Q₁ c hc hQ f a₀))

theorem EulerSourceCylinderEquation.coordinateDerivative_contDiff (period : ℝ) [Fact (0 < period)] {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period E S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported period U S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) ↑a₀) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) (coordinateDerivative period S hS T hT Q Q₁ c hc hQ f a₀))

theorem EulerSourceCylinderEquation.velocity_contDiff (period : ℝ) [Fact (0 < period)] {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period E S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported period U S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) ↑a₀) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) (velocity period S hS T hT Q Q₁ c hc hQ f a₀))

theorem EulerSourceCylinderEquation.velocityDerivative_contDiff (period : ℝ) [Fact (0 < period)] {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period E S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported period U S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) ↑a₀) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) (velocityDerivative period S hS T hT Q Q₁ c hc hQ f a₀))

The actual pointwise forward equation

The L² coordinate equation and normal balance hold for the reconstructed smooth field at every cylinder point. The scalar normal residual is the literal source expression; its angular primitive will supply the pressure.

The solved forward field as an actual smooth cylinder field

The representative is recovered by bounded H3 evaluation of the genuine L² solution. It is jointly continuous, spatially and angularly smooth, compactly supported, and has the true pointwise within-time derivative.

noncomputable def EulerSourceCylinderClassical.field (period : ℝ) [Fact (0 < period)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported period U S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) ↑a₀) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerSmoothLimit.Space

The actual physical field, reconstructed from the solved L² class.

Equations

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

noncomputable def EulerSourceCylinderClassical.derivativeField (period : ℝ) [Fact (0 < period)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported period U S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) ↑a₀) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerSmoothLimit.Space

The reconstructed actual product-rule time derivative.

Equations

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

theorem EulerSourceCylinderClassical.field_joint_continuous (period : ℝ) [Fact (0 < period)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported period U S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) ↑a₀) : Continuous fun (z : ↑(Set.Icc 0 T) × EulerLiftedGradientSpace.LiftDomain period) => field period S hS hSc T hT Q Q₁ c hc hQ f a₀ hf ha₀ z.1 z.2

theorem EulerSourceCylinderClassical.field_smooth (period : ℝ) [Fact (0 < period)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported period U S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) ↑a₀) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (field period S hS hSc T hT Q Q₁ c hc hQ f a₀ hf ha₀ t) x)

theorem EulerSourceCylinderClassical.derivativeField_smooth (period : ℝ) [Fact (0 < period)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported period U S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) ↑a₀) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (derivativeField period S hS hSc T hT Q Q₁ c hc hQ f a₀ hf ha₀ t) x)

theorem EulerSourceCylinderClassical.field_ae (period : ℝ) [Fact (0 < period)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported period U S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) ↑a₀) (t : ↑(Set.Icc 0 T)) : ↑↑↑((EulerSourceCylinderEquation.velocity period S hS T hT Q Q₁ c hc hQ f a₀) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] field period S hS hSc T hT Q Q₁ c hc hQ f a₀ hf ha₀ t

theorem EulerSourceCylinderClassical.derivativeField_ae (period : ℝ) [Fact (0 < period)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported period U S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) ↑a₀) (t : ↑(Set.Icc 0 T)) : ↑↑↑((EulerSourceCylinderEquation.velocityDerivative period S hS T hT Q Q₁ c hc hQ f a₀) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] derivativeField period S hS hSc T hT Q Q₁ c hc hQ f a₀ hf ha₀ t

theorem EulerSourceCylinderClassical.field_tsupport_subset (period : ℝ) [Fact (0 < period)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported period U S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) ↑a₀) (t : ↑(Set.Icc 0 T)) : tsupport (field period S hS hSc T hT Q Q₁ c hc hQ f a₀ hf ha₀ t) ⊆ EulerLpCylinderTranslation.spatialSet period S

theorem EulerSourceCylinderClassical.field_hasCompactSupport (period : ℝ) [Fact (0 < period)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported period U S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) ↑a₀) (t : ↑(Set.Icc 0 T)) : HasCompactSupport (field period S hS hSc T hT Q Q₁ c hc hQ f a₀ hf ha₀ t)

theorem EulerSourceCylinderClassical.fullVelocity_hasDerivWithinAt (period : ℝ) [Fact (0 < period)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported period U S hS)) (hQt : ∀ t ∈ Set.Icc 0 T, ∀ (x : EulerSmoothLimit.Space), HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath T hT Q.field s) x) ((EulerVolterraConvolution.extendPath T hT Q₁.field t) x) (Set.Icc 0 T) t) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT ((EulerLpCylinderPaths.includePath period S hS) (EulerSourceCylinderEquation.velocity period S hS T hT Q Q₁ c hc hQ f a₀))) (((EulerLpCylinderPaths.includePath period S hS) (EulerSourceCylinderEquation.velocityDerivative period S hS T hT Q Q₁ c hc hQ f a₀)) t) (Set.Icc 0 T) ↑t

Inclusion in full cylinder L² preserves the already proved time derivative.

theorem EulerSourceCylinderClassical.field_hasDerivWithinAt (period : ℝ) [Fact (0 < period)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported period U S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) ↑a₀) (hQt : ∀ t ∈ Set.Icc 0 T, ∀ (x : EulerSmoothLimit.Space), HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath T hT Q.field s) x) ((EulerVolterraConvolution.extendPath T hT Q₁.field t) x) (Set.Icc 0 T) t) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) : HasDerivWithinAt (fun (s : ℝ) => field period S hS hSc T hT Q Q₁ c hc hQ f a₀ hf ha₀ (Set.projIcc 0 T hT s) x) (derivativeField period S hS hSc T hT Q Q₁ c hc hQ f a₀ hf ha₀ t x) (Set.Icc 0 T) ↑t

No global time extension is assumed: the true time derivative holds within the closed source interval, at every cylinder point.

noncomputable def EulerSourceCylinderClassical.normalResidual (period : ℝ) [Fact (0 < period)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported period U S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) ↑a₀) (M : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) : ℝ

The source's literal scalar normal pressure residual.

Equations

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

theorem EulerSourceCylinderClassical.normalResidual_continuous (period : ℝ) [Fact (0 < period)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported period U S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) ↑a₀) (M : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (m.field t) x ≠ 0) (t : ↑(Set.Icc 0 T)) : Continuous (normalResidual period S hS hSc T hT Q Q₁ c hc hQ f a₀ hf ha₀ M m t)

theorem EulerSourceCylinderClassical.normalResidual_smooth (period : ℝ) [Fact (0 < period)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported period U S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) ↑a₀) (M : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (m.field t) x ≠ 0) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (normalResidual period S hS hSc T hT Q Q₁ c hc hQ f a₀ hf ha₀ M m t) x)

The literal scalar pressure source is smooth in every spatial and angular variable.

theorem EulerSourceCylinderClassical.field_tangent (period : ℝ) [Fact (0 < period)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported period U S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) ↑a₀) (m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space) (hTangent : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), inner ℝ ((m.field t) x) (((Q.field t) x) v) = 0) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) : inner ℝ ((m.field t) x.1) (field period S hS hSc T hT Q Q₁ c hc hQ f a₀ hf ha₀ t x) = 0

Pointwise tangency follows from the actual frame representation and continuity.

theorem EulerSourceCylinderClassical.field_balance (period : ℝ) [Fact (0 < period)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported period U S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) ↑a₀) (M : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (m.field t) x ≠ 0) (hTangent : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), inner ℝ ((m.field t) x) (((Q.field t) x) v) = 0) (hRange : ∀ (t : ↑(Set.Icc 0 T)) (x η : EulerSmoothLimit.Space), inner ℝ ((m.field t) x) η = 0 → ∃ (v : U), ((Q.field t) x) v = η) (hFlow : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (Q₁.field t) x = (M.field t) x ∘SL (Q.field t) x) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) : derivativeField period S hS hSc T hT Q Q₁ c hc hQ f a₀ hf ha₀ t x + ((M.field t) x.1) (field period S hS hSc T hT Q Q₁ c hc hQ f a₀ hf ha₀ t x) + normalResidual period S hS hSc T hT Q Q₁ c hc hQ f a₀ hf ha₀ M m t x • (m.field t) x.1 = EulerCylinderSmoothOrbit.pointField period ((EulerLpCylinderPaths.includePath period S hS) f) hf t x

Equation (11) before angular integration holds at every cylinder point.

The solved normal pressure source has zero angular mean

The zero mode is proved for the actual Duhamel solution and then transferred to its continuous scalar representative. No zero-mean condition on the solution or on its pressure residual is assumed.

The actual scalar pressure source on cylinder L²

The normal functional is constructed from the positive one-column Gram matrix. Applying it to f−2MA gives a genuine scalar L² path, with the literal normal residual as representative and genuine smooth mixed translation orbit.

noncomputable def EulerSourceCylinderEquation.pressureSource (period : ℝ) [Fact (0 < period)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported period U S hS)) (M : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space) (cm : ℝ) (hcm : 0 < cm) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), cm ≤ ‖(m.field t) x‖ ^ 2) : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period ℝ S hS))

A genuine supported scalar path representing the right side of ∂θπ in (11).

Equations

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

theorem EulerSourceCylinderEquation.pressureSource_ae (period : ℝ) [Fact (0 < period)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported period U S hS)) (M : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space) (cm : ℝ) (hcm : 0 < cm) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), cm ≤ ‖(m.field t) x‖ ^ 2) (t : ↑(Set.Icc 0 T)) : ↑↑↑((pressureSource period S hS T hT Q Q₁ c hc hQ f a₀ M m cm hcm hm) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] fun (x : EulerLiftedGradientSpace.LiftDomain period) => (inner ℝ ((m.field t) x.1) (↑↑↑(f t) x) - 2 * inner ℝ ((m.field t) x.1) (((M.field t) x.1) (↑↑↑((velocity period S hS T hT Q Q₁ c hc hQ f a₀) t) x))) / ‖(m.field t) x.1‖ ^ 2

The pressure source is precisely the manuscript's scalar quotient.

theorem EulerSourceCylinderEquation.pressureSource_contDiff (period : ℝ) [Fact (0 < period)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported period U S hS)) (M : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space) (cm : ℝ) (hcm : 0 < cm) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), cm ≤ ‖(m.field t) x‖ ^ 2) (hSc : IsCompact S) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) ↑a₀) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate period a) ((EulerLpCylinderPaths.includePath period S hS) (pressureSource period S hS T hT Q Q₁ c hc hQ f a₀ M m cm hcm hm))

The actual scalar pressure source inherits genuine mixed regularity from the solve.

theorem EulerSourceCylinderEquation.pressureSource_average_zero (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (M : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space) (cm : ℝ) (hcm : 0 < cm) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), cm ≤ ‖(m.field t) x‖ ^ 2) (hf₀ : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderAngleAverage.average P) ↑(f t) = 0) (ha₀ : (EulerCylinderAngleAverage.average P) ↑a₀ = 0) (t : ↑(Set.Icc 0 T)) : (EulerCylinderAngleAverage.average P) ↑((pressureSource P S hS T hT Q Q₁ c hc hQ f a₀ M m cm hcm hm) t) = 0

theorem EulerSourceCylinderEquation.pressureSource_slice_contDiff (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (M : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space) (cm : ℝ) (hcm : 0 < cm) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), cm ≤ ‖(m.field t) x‖ ^ 2) (hSc : IsCompact S) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerLpCylinderPaths.includePath P S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑a₀) (t : ↑(Set.Icc 0 T)) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑((pressureSource P S hS T hT Q Q₁ c hc hQ f a₀ M m cm hcm hm) t)

theorem EulerSourceCylinderClassical.normal_ne_zero_of_lower (T : ℝ) (m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space) (cm : ℝ) (hcm : 0 < cm) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), cm ≤ ‖(m.field t) x‖ ^ 2) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : (m.field t) x ≠ 0

theorem EulerSourceCylinderClassical.pressureSource_ae_normalResidual (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerLpCylinderPaths.includePath P S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑a₀) (M : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space) (cm : ℝ) (hcm : 0 < cm) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), cm ≤ ‖(m.field t) x‖ ^ 2) (t : ↑(Set.Icc 0 T)) : ↑↑↑((EulerSourceCylinderEquation.pressureSource P S hS T hT Q Q₁ c hc hQ f a₀ M m cm hcm hm) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] normalResidual P S hS hSc T hT Q Q₁ c hc hQ f a₀ hf ha₀ M m t

The actual scalar L² class represents the literal normal quotient.

theorem EulerSourceCylinderClassical.normalResidual_mean_zero (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerLpCylinderPaths.includePath P S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑a₀) (M : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space) (cm : ℝ) (hcm : 0 < cm) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), cm ≤ ‖(m.field t) x‖ ^ 2) (hf₀ : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderAngleAverage.average P) ↑(f t) = 0) (ha₀zero : (EulerCylinderAngleAverage.average P) ↑a₀ = 0) (t : ↑(Set.Icc 0 T)) (y : EulerSmoothLimit.Space) : ∫ (s : ℝ) in 0..P, normalResidual P S hS hSc T hT Q Q₁ c hc hQ f a₀ hf ha₀ M m t (y, ↑s) = 0

Zero mean of the forcing and initial coordinate implies zero mean of the literal pressure source of the constructed solution.

noncomputable def EulerSourceCylinderEquation.pressurePath (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (M : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space) (cm : ℝ) (hcm : 0 < cm) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), cm ≤ ‖(m.field t) x‖ ^ 2) : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ))

The actual bounded angular inverse applied to the solved scalar source.

Equations

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

theorem EulerSourceCylinderEquation.pressurePath_contDiff (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (M : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space) (cm : ℝ) (hcm : 0 < cm) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), cm ≤ ‖(m.field t) x‖ ^ 2) (hSc : IsCompact S) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerLpCylinderPaths.includePath P S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑a₀) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (pressurePath P S hS T hT Q Q₁ c hc hQ f a₀ M m cm hcm hm)

noncomputable def EulerSourceCylinderClassical.pressureField (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerLpCylinderPaths.includePath P S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑a₀) (M : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space) (cm : ℝ) (hcm : 0 < cm) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), cm ≤ ‖(m.field t) x‖ ^ 2) (hf₀ : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderAngleAverage.average P) ↑(f t) = 0) (ha₀zero : (EulerCylinderAngleAverage.average P) ↑a₀ = 0) (t : ↑(Set.Icc 0 T)) : EulerLiftedGradientSpace.LiftDomain P → ℝ

The literal normalized periodic pressure for the actual forward solution.

Equations

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

theorem EulerSourceCylinderClassical.pressureField_ae (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerLpCylinderPaths.includePath P S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑a₀) (M : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space) (cm : ℝ) (hcm : 0 < cm) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), cm ≤ ‖(m.field t) x‖ ^ 2) (hf₀ : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderAngleAverage.average P) ↑(f t) = 0) (ha₀zero : (EulerCylinderAngleAverage.average P) ↑a₀ = 0) (t : ↑(Set.Icc 0 T)) : ↑↑((EulerSourceCylinderEquation.pressurePath P S hS T hT Q Q₁ c hc hQ f a₀ M m cm hcm hm) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] pressureField P S hS hSc T hT Q Q₁ c hc hQ f a₀ hf ha₀ M m cm hcm hm hf₀ ha₀zero t

theorem EulerSourceCylinderClassical.pressureField_angle (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerLpCylinderPaths.includePath P S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑a₀) (M : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space) (cm : ℝ) (hcm : 0 < cm) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), cm ≤ ‖(m.field t) x‖ ^ 2) (hf₀ : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderAngleAverage.average P) ↑(f t) = 0) (ha₀zero : (EulerCylinderAngleAverage.average P) ↑a₀ = 0) (t : ↑(Set.Icc 0 T)) (y : EulerSmoothLimit.Space) (θ : ℝ) : HasDerivAt (fun (s : ℝ) => pressureField P S hS hSc T hT Q Q₁ c hc hQ f a₀ hf ha₀ M m cm hcm hm hf₀ ha₀zero t (y, ↑s)) (normalResidual P S hS hSc T hT Q Q₁ c hc hQ f a₀ hf ha₀ M m t (y, ↑θ)) θ

The derivative is genuine at every real angle, including period endpoints.

theorem EulerSourceCylinderClassical.pressureField_mean_zero (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerLpCylinderPaths.includePath P S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑a₀) (M : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space) (cm : ℝ) (hcm : 0 < cm) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), cm ≤ ‖(m.field t) x‖ ^ 2) (hf₀ : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderAngleAverage.average P) ↑(f t) = 0) (ha₀zero : (EulerCylinderAngleAverage.average P) ↑a₀ = 0) (t : ↑(Set.Icc 0 T)) (y : EulerSmoothLimit.Space) : ∫ (θ : ℝ) in 0..P, pressureField P S hS hSc T hT Q Q₁ c hc hQ f a₀ hf ha₀ M m cm hcm hm hf₀ ha₀zero t (y, ↑θ) = 0

theorem EulerSourceCylinderClassical.pressureField_smooth (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerLpCylinderPaths.includePath P S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑a₀) (M : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space) (cm : ℝ) (hcm : 0 < cm) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), cm ≤ ‖(m.field t) x‖ ^ 2) (hf₀ : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderAngleAverage.average P) ↑(f t) = 0) (ha₀zero : (EulerCylinderAngleAverage.average P) ↑a₀ = 0) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain P) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (pressureField P S hS hSc T hT Q Q₁ c hc hQ f a₀ hf ha₀ M m cm hcm hm hf₀ ha₀zero t) x)

theorem EulerSourceCylinderClassical.pressureField_continuous (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerLpCylinderPaths.includePath P S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑a₀) (M : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space) (cm : ℝ) (hcm : 0 < cm) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), cm ≤ ‖(m.field t) x‖ ^ 2) (hf₀ : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderAngleAverage.average P) ↑(f t) = 0) (ha₀zero : (EulerCylinderAngleAverage.average P) ↑a₀ = 0) (t : ↑(Set.Icc 0 T)) : Continuous (pressureField P S hS hSc T hT Q Q₁ c hc hQ f a₀ hf ha₀ M m cm hcm hm hf₀ ha₀zero t)

theorem EulerSourceCylinderClassical.normalResidual_zero_outside (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerLpCylinderPaths.includePath P S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑a₀) (M : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space) (t : ↑(Set.Icc 0 T)) (y : EulerSmoothLimit.Space) (hy : y ∉ S) (θ : AddCircle P) : normalResidual P S hS hSc T hT Q Q₁ c hc hQ f a₀ hf ha₀ M m t (y, θ) = 0

theorem EulerSourceCylinderClassical.pressureField_zero_outside (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerLpCylinderPaths.includePath P S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑a₀) (M : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space) (cm : ℝ) (hcm : 0 < cm) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), cm ≤ ‖(m.field t) x‖ ^ 2) (hf₀ : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderAngleAverage.average P) ↑(f t) = 0) (ha₀zero : (EulerCylinderAngleAverage.average P) ↑a₀ = 0) (t : ↑(Set.Icc 0 T)) (y : EulerSmoothLimit.Space) (hy : y ∉ S) (θ : AddCircle P) : pressureField P S hS hSc T hT Q Q₁ c hc hQ f a₀ hf ha₀ M m cm hcm hm hf₀ ha₀zero t (y, θ) = 0

theorem EulerSourceCylinderClassical.pressureField_tsupport_subset (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerLpCylinderPaths.includePath P S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑a₀) (M : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space) (cm : ℝ) (hcm : 0 < cm) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), cm ≤ ‖(m.field t) x‖ ^ 2) (hf₀ : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderAngleAverage.average P) ↑(f t) = 0) (ha₀zero : (EulerCylinderAngleAverage.average P) ↑a₀ = 0) (t : ↑(Set.Icc 0 T)) : tsupport (pressureField P S hS hSc T hT Q Q₁ c hc hQ f a₀ hf ha₀ M m cm hcm hm hf₀ ha₀zero t) ⊆ EulerLpCylinderTranslation.spatialSet P S

theorem EulerSourceCylinderClassical.pressureField_hasCompactSupport (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerLpCylinderPaths.includePath P S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑a₀) (M : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space) (cm : ℝ) (hcm : 0 < cm) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), cm ≤ ‖(m.field t) x‖ ^ 2) (hf₀ : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderAngleAverage.average P) ↑(f t) = 0) (ha₀zero : (EulerCylinderAngleAverage.average P) ↑a₀ = 0) (t : ↑(Set.Icc 0 T)) : HasCompactSupport (pressureField P S hS hSc T hT Q Q₁ c hc hQ f a₀ hf ha₀ M m cm hcm hm hf₀ ha₀zero t)

theorem EulerSourceCylinderClassical.field_pressure_equation (P : ℝ) [Fact (0 < P)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSc : IsCompact S) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (U →L[ℝ] EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q.field t) x) v‖ ^ 2) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported P EulerSmoothLimit.Space S hS))) (a₀ : ↥(EulerLpCylinderPaths.Supported P U S hS)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerLpCylinderPaths.includePath P S hS) f)) (ha₀ : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑a₀) (M : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space) (cm : ℝ) (hcm : 0 < cm) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), cm ≤ ‖(m.field t) x‖ ^ 2) (hf₀ : ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderAngleAverage.average P) ↑(f t) = 0) (ha₀zero : (EulerCylinderAngleAverage.average P) ↑a₀ = 0) (hTangent : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), inner ℝ ((m.field t) x) (((Q.field t) x) v) = 0) (hRange : ∀ (t : ↑(Set.Icc 0 T)) (x η : EulerSmoothLimit.Space), inner ℝ ((m.field t) x) η = 0 → ∃ (v : U), ((Q.field t) x) v = η) (hFlow : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (Q₁.field t) x = (M.field t) x ∘SL (Q.field t) x) (t : ↑(Set.Icc 0 T)) (y : EulerSmoothLimit.Space) (θ : ℝ) : derivativeField P S hS hSc T hT Q Q₁ c hc hQ f a₀ hf ha₀ t (y, ↑θ) + ((M.field t) y) (field P S hS hSc T hT Q Q₁ c hc hQ f a₀ hf ha₀ t (y, ↑θ)) + deriv (fun (s : ℝ) => pressureField P S hS hSc T hT Q Q₁ c hc hQ f a₀ hf ha₀ M m cm hcm hm hf₀ ha₀zero t (y, ↑s)) θ • (m.field t) y = EulerCylinderSmoothOrbit.pointField P ((EulerLpCylinderPaths.includePath P S hS) f) hf t (y, ↑θ)

Equation (11) with the actual angular derivative of the normalized pressure.