The actual forward transverse initial value problem

The matrix coefficient in source equation (12) is formed using the genuinely constructed Gram inverse. Given the homogeneous evolution assumed in (H3), Duhamel's integral constructs the forced coordinate and physical velocity. The coordinate equation, tangency, initial trace and physical pressure balance are proved at every time, including within-interval endpoint derivatives.

noncomputable def EulerTransverseForwardInverse.generator {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (Q Q₁ : C(↑(Set.Icc 0 T), V →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : V), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) : C(↑(Set.Icc 0 T), V →L[ℝ] V)

The actual ordinary coefficient -2 K⁻¹ Q* Q₁ in equation (12).

Equations

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

noncomputable def EulerTransverseForwardInverse.forcingOperator {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (Q : C(↑(Set.Icc 0 T), V →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : V), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) : C(↑(Set.Icc 0 T), E) →L[ℝ] C(↑(Set.Icc 0 T), V)

The actual projected forcing K⁻¹ Q* f, as a bounded continuous-path map.

Equations

• EulerTransverseForwardInverse.forcingOperator T Q c hc hQ = EulerContinuousTimeIntegral.multiplier (EulerTransverseGramPath.frameLeftInversePath T Q c hc hQ)

noncomputable def EulerTransverseForwardInverse.coordinates {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : C(↑(Set.Icc 0 T), V →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : V), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (U : EulerLinearDuhamel.Evolution T hT (generator T Q Q₁ c hc hQ)) (f : C(↑(Set.Icc 0 T), E)) (a₀ : V) : C(↑(Set.Icc 0 T), V)

The forward coordinate is the actual forced Duhamel path.

Equations

• EulerTransverseForwardInverse.coordinates T hT Q Q₁ c hc hQ U f a₀ = U.solution ((EulerTransverseForwardInverse.forcingOperator T Q c hc hQ) f) a₀

noncomputable def EulerTransverseForwardInverse.coordinateDerivative {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : C(↑(Set.Icc 0 T), V →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : V), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (U : EulerLinearDuhamel.Evolution T hT (generator T Q Q₁ c hc hQ)) (f : C(↑(Set.Icc 0 T), E)) (a₀ : V) : C(↑(Set.Icc 0 T), V)

Its derivative is the literal ordinary right hand side.

Equations

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

noncomputable def EulerTransverseForwardInverse.velocity {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : C(↑(Set.Icc 0 T), V →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : V), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (U : EulerLinearDuhamel.Evolution T hT (generator T Q Q₁ c hc hQ)) (f : C(↑(Set.Icc 0 T), E)) (a₀ : V) : C(↑(Set.Icc 0 T), E)

The physical velocity A=Qa is an actual continuous path.

Equations

• EulerTransverseForwardInverse.velocity T hT Q Q₁ c hc hQ U f a₀ = (EulerContinuousTimeIntegral.multiplier Q) (EulerTransverseForwardInverse.coordinates T hT Q Q₁ c hc hQ U f a₀)

noncomputable def EulerTransverseForwardInverse.velocityDerivative {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : C(↑(Set.Icc 0 T), V →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : V), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (U : EulerLinearDuhamel.Evolution T hT (generator T Q Q₁ c hc hQ)) (f : C(↑(Set.Icc 0 T), E)) (a₀ : V) : C(↑(Set.Icc 0 T), E)

The physical time derivative, with the literal product-rule expression.

Equations

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

@[simp]

theorem EulerTransverseForwardInverse.coordinates_initial {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : C(↑(Set.Icc 0 T), V →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : V), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (U : EulerLinearDuhamel.Evolution T hT (generator T Q Q₁ c hc hQ)) (f : C(↑(Set.Icc 0 T), E)) (a₀ : V) : (coordinates T hT Q Q₁ c hc hQ U f a₀) ⟨0, ⋯⟩ = a₀

The constructed coordinate attains the prescribed initial datum.

@[simp]

theorem EulerTransverseForwardInverse.velocity_initial {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : C(↑(Set.Icc 0 T), V →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : V), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (U : EulerLinearDuhamel.Evolution T hT (generator T Q Q₁ c hc hQ)) (f : C(↑(Set.Icc 0 T), E)) (a₀ : V) : (velocity T hT Q Q₁ c hc hQ U f a₀) ⟨0, ⋯⟩ = (Q ⟨0, ⋯⟩) a₀

The actual initial physical velocity is Q(0)a₀.

theorem EulerTransverseForwardInverse.coordinates_hasDerivWithinAt {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : C(↑(Set.Icc 0 T), V →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : V), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (U : EulerLinearDuhamel.Evolution T hT (generator T Q Q₁ c hc hQ)) (f : C(↑(Set.Icc 0 T), E)) (a₀ : V) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (coordinates T hT Q Q₁ c hc hQ U f a₀)) ((coordinateDerivative T hT Q Q₁ c hc hQ U f a₀) t) (Set.Icc 0 T) ↑t

Every-time coordinate differentiability follows from the actual integral, not from an assumed derivative representative.

theorem EulerTransverseForwardInverse.coordinate_equation {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : C(↑(Set.Icc 0 T), V →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : V), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (U : EulerLinearDuhamel.Evolution T hT (generator T Q Q₁ c hc hQ)) (f : C(↑(Set.Icc 0 T), E)) (a₀ : V) (t : ↑(Set.Icc 0 T)) : (EulerTransverseGramInverse.gram (Q t)) ((coordinateDerivative T hT Q Q₁ c hc hQ U f a₀) t) = (ContinuousLinearMap.adjoint (Q t)) (f t - 2 • (Q₁ t) ((coordinates T hT Q Q₁ c hc hQ U f a₀) t))

The constructed derivative satisfies the literal projected equation (12).

theorem EulerTransverseForwardInverse.velocity_tangent {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : C(↑(Set.Icc 0 T), V →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : V), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (U : EulerLinearDuhamel.Evolution T hT (generator T Q Q₁ c hc hQ)) (m : ↑(Set.Icc 0 T) → E) (hTangent : ∀ (t : ↑(Set.Icc 0 T)) (v : V), inner ℝ (m t) ((Q t) v) = 0) (f : C(↑(Set.Icc 0 T), E)) (a₀ : V) (t : ↑(Set.Icc 0 T)) : inner ℝ (m t) ((velocity T hT Q Q₁ c hc hQ U f a₀) t) = 0

Physical velocity is tangent at every time because it lies in the frame range.

theorem EulerTransverseForwardInverse.velocity_hasDerivWithinAt {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : C(↑(Set.Icc 0 T), V →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : V), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (U : EulerLinearDuhamel.Evolution T hT (generator T Q Q₁ c hc hQ)) (hQd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) (f : C(↑(Set.Icc 0 T), E)) (a₀ : V) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (velocity T hT Q Q₁ c hc hQ U f a₀)) ((velocityDerivative T hT Q Q₁ c hc hQ U f a₀) t) (Set.Icc 0 T) ↑t

The physical product-rule expression is its actual every-time derivative.

noncomputable def EulerTransverseForwardInverse.pressureCoefficient {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : C(↑(Set.Icc 0 T), V →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : V), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (U : EulerLinearDuhamel.Evolution T hT (generator T Q Q₁ c hc hQ)) (M : ↑(Set.Icc 0 T) → E →L[ℝ] E) (m : ↑(Set.Icc 0 T) → E) (f : C(↑(Set.Icc 0 T), E)) (a₀ : V) (t : ↑(Set.Icc 0 T)) : ℝ

The literal normal pressure coefficient in source equation (11).

Equations

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

theorem EulerTransverseForwardInverse.velocity_balance {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : C(↑(Set.Icc 0 T), V →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : V), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (U : EulerLinearDuhamel.Evolution T hT (generator T Q Q₁ c hc hQ)) (M : ↑(Set.Icc 0 T) → E →L[ℝ] E) (m : ↑(Set.Icc 0 T) → E) (hm : ∀ (t : ↑(Set.Icc 0 T)), m t ≠ 0) (hTangent : ∀ (t : ↑(Set.Icc 0 T)) (v : V), inner ℝ (m t) ((Q t) v) = 0) (hRange : ∀ (t : ↑(Set.Icc 0 T)) (η : E), inner ℝ (m t) η = 0 → ∃ (v : V), (Q t) v = η) (hflow : ∀ (t : ↑(Set.Icc 0 T)), Q₁ t = M t ∘SL Q t) (f : C(↑(Set.Icc 0 T), E)) (a₀ : V) (t : ↑(Set.Icc 0 T)) : (velocityDerivative T hT Q Q₁ c hc hQ U f a₀) t + (M t) ((velocity T hT Q Q₁ c hc hQ U f a₀) t) + pressureCoefficient T hT Q Q₁ c hc hQ U M m f a₀ t • m t = f t

The actual forward velocity and explicit normal pressure residual satisfy source equation (11) at every time.

noncomputable def EulerTransverseForwardInverse.coordinatesOperator {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : C(↑(Set.Icc 0 T), V →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : V), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (U : EulerLinearDuhamel.Evolution T hT (generator T Q Q₁ c hc hQ)) : V × C(↑(Set.Icc 0 T), E) →L[ℝ] C(↑(Set.Icc 0 T), V)

The full coordinate solution depends bounded-linearly on initial datum and forcing.

Equations

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

theorem EulerTransverseForwardInverse.coordinatesOperator_apply {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : C(↑(Set.Icc 0 T), V →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : V), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (U : EulerLinearDuhamel.Evolution T hT (generator T Q Q₁ c hc hQ)) (f : C(↑(Set.Icc 0 T), E)) (a₀ : V) : (coordinatesOperator T hT Q Q₁ c hc hQ U) (a₀, f) = coordinates T hT Q Q₁ c hc hQ U f a₀

The bounded linear data map is exactly the constructed coordinate path.

noncomputable def EulerTransverseForwardInverse.velocityOperator {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : C(↑(Set.Icc 0 T), V →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : V), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (U : EulerLinearDuhamel.Evolution T hT (generator T Q Q₁ c hc hQ)) : V × C(↑(Set.Icc 0 T), E) →L[ℝ] C(↑(Set.Icc 0 T), E)

The physical forward inverse is an actual bounded linear map in its data.

Equations

• EulerTransverseForwardInverse.velocityOperator T hT Q Q₁ c hc hQ U = EulerContinuousTimeIntegral.multiplier Q ∘SL EulerTransverseForwardInverse.coordinatesOperator T hT Q Q₁ c hc hQ U

theorem EulerTransverseForwardInverse.velocity_zero {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : C(↑(Set.Icc 0 T), V →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : V), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (U : EulerLinearDuhamel.Evolution T hT (generator T Q Q₁ c hc hQ)) : velocity T hT Q Q₁ c hc hQ U 0 0 = 0

Zero data give the zero path; this is the pointwise support-preservation mechanism.