The actual source forward equation on cylinder L²

The coordinate path is the constructed Duhamel integral with the genuine Gram-projected forcing. Its physical velocity has the true within-time derivative. The projected equation and normal pressure balance are derived on the actual L² representatives, not assumed as properties of a solver.

@[instance_reducible]

noncomputable def EulerSourceCylinderEquation.instSourceCylinderEquation1 (period : ℝ) [Fact (0 < period)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedAddCommGroup ↥(EulerLpCylinderPaths.Supported period U S hS)

Cache the standard NormedAddCommGroup (Supported period U S hS) instance to shorten typeclass synthesis.

Equations

• EulerSourceCylinderEquation.instSourceCylinderEquation1 period S hS = inferInstance

@[instance_reducible]

noncomputable def EulerSourceCylinderEquation.instSourceCylinderEquation2 (period : ℝ) [Fact (0 < period)] {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedSpace ℝ ↥(EulerLpCylinderPaths.Supported period U S hS)

Cache the standard NormedSpace ℝ (Supported period U S hS) instance to shorten typeclass synthesis.

Equations

• EulerSourceCylinderEquation.instSourceCylinderEquation2 period S hS = inferInstance

@[instance_reducible]

noncomputable def EulerSourceCylinderEquation.instSourceCylinderEquation3 (period : ℝ) [Fact (0 < period)] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedAddCommGroup ↥(EulerLpCylinderPaths.Supported period E S hS)

Cache the standard NormedAddCommGroup (Supported period E S hS) instance to shorten typeclass synthesis.

Equations

• EulerSourceCylinderEquation.instSourceCylinderEquation3 period S hS = inferInstance

@[instance_reducible]

noncomputable def EulerSourceCylinderEquation.instSourceCylinderEquation4 (period : ℝ) [Fact (0 < period)] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) : NormedSpace ℝ ↥(EulerLpCylinderPaths.Supported period E S hS)

Cache the standard NormedSpace ℝ (Supported period E S hS) instance to shorten typeclass synthesis.

Equations

• EulerSourceCylinderEquation.instSourceCylinderEquation4 period S hS = inferInstance

noncomputable def EulerSourceCylinderEquation.coordinates (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) (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)) : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period U S hS))

The actual unnormalized coordinate solution; no regularity of a profile g is needed.

Equations

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

noncomputable def EulerSourceCylinderEquation.coordinateDerivative (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) (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)) : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period U S hS))

Its actual ordinary right side.

Equations

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

noncomputable def EulerSourceCylinderEquation.velocity (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) (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)) : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period E S hS))

The physical transverse velocity A=Q a.

Equations

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

noncomputable def EulerSourceCylinderEquation.velocityDerivative (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) (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)) : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderPaths.Supported period E S hS))

Its literal product-rule expression, proved below to be the time derivative.

Equations

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

@[simp]

theorem EulerSourceCylinderEquation.coordinates_initial (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) (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)) : (coordinates period S hS T hT Q Q₁ c hc hQ f a₀) ⟨0, ⋯⟩ = a₀

theorem EulerSourceCylinderEquation.coordinates_hasDerivWithinAt (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) (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)) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (coordinates period S hS T hT Q Q₁ c hc hQ f a₀)) ((coordinateDerivative period S hS T hT Q Q₁ c hc hQ f a₀) t) (Set.Icc 0 T) ↑t

The coordinate equation has its true derivative on the closed time interval.

theorem EulerSourceCylinderEquation.velocity_hasDerivWithinAt (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) (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)) (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 (velocity period S hS T hT Q Q₁ c hc hQ f a₀)) ((velocityDerivative period S hS T hT Q Q₁ c hc hQ f a₀) t) (Set.Icc 0 T) ↑t

Literal coefficient time derivatives induce the genuine physical time derivative.

theorem EulerSourceCylinderEquation.coordinate_equation_ae (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) (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)) (t : ↑(Set.Icc 0 T)) : ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain period) ∂EulerLiftedGradientSpace.liftMeasure period, (EulerTransverseGramInverse.gram ((Q.field t) x.1)) (↑↑↑((coordinateDerivative period S hS T hT Q Q₁ c hc hQ f a₀) t) x) = (ContinuousLinearMap.adjoint ((Q.field t) x.1)) (↑↑↑(f t) x - 2 • ((Q₁.field t) x.1) (↑↑↑((coordinates period S hS T hT Q Q₁ c hc hQ f a₀) t) x))

The genuine L² representatives satisfy the projected source equation (12).

theorem EulerSourceCylinderEquation.velocity_ae (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) (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)) (t : ↑(Set.Icc 0 T)) : ↑↑↑((velocity period S hS T hT Q Q₁ c hc hQ f a₀) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] fun (x : EulerLiftedGradientSpace.LiftDomain period) => ((Q.field t) x.1) (↑↑↑((coordinates period S hS T hT Q Q₁ c hc hQ f a₀) t) x)

The physical velocity's representative is exactly Q times the solved coordinate.

theorem EulerSourceCylinderEquation.velocityDerivative_ae (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) (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)) (t : ↑(Set.Icc 0 T)) : ↑↑↑((velocityDerivative period S hS T hT Q Q₁ c hc hQ f a₀) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] fun (x : EulerLiftedGradientSpace.LiftDomain period) => ((Q₁.field t) x.1) (↑↑↑((coordinates period S hS T hT Q Q₁ c hc hQ f a₀) t) x) + ((Q.field t) x.1) (↑↑↑((coordinateDerivative period S hS T hT Q Q₁ c hc hQ f a₀) t) x)

theorem EulerSourceCylinderEquation.velocity_balance_ae (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) (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)) (M : ↑(Set.Icc 0 T) → EulerSmoothLimit.Space → E →L[ℝ] E) (m : ↑(Set.Icc 0 T) → EulerSmoothLimit.Space → E) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), m t x ≠ 0) (hTangent : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U), inner ℝ (m t x) (((Q.field t) x) v) = 0) (hRange : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (η : E), inner ℝ (m t x) η = 0 → ∃ (v : U), ((Q.field t) x) v = η) (hFlow : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), (Q₁.field t) x = M t x ∘SL (Q.field t) x) (t : ↑(Set.Icc 0 T)) : ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain period) ∂EulerLiftedGradientSpace.liftMeasure period, ↑↑↑((velocityDerivative period S hS T hT Q Q₁ c hc hQ f a₀) t) x + (M t x.1) (↑↑↑((velocity period S hS T hT Q Q₁ c hc hQ f a₀) t) x) + ((inner ℝ (m t x.1) (↑↑↑(f t) x) - 2 * inner ℝ (m t x.1) ((M t x.1) (↑↑↑((velocity period S hS T hT Q Q₁ c hc hQ f a₀) t) x))) / ‖m t x.1‖ ^ 2) • m t x.1 = ↑↑↑(f t) x

Equation (11)'s literal normal residual follows from the actual coordinate solve.