The actual affine-terminal inverse on the cylinder

The terminal coordinate below is an element of the genuine cylinder L² space. The affine lift and its zero-endpoint correction are constructed by the same coercive form as the forced history inverse. In particular, no spatially constant nonzero vector is silently treated as L² data.

noncomputable def EulerCylinderDirichlet.Coefficients.endpointCorrection {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (P : ℝ) [Fact (0 < P)] {T : ℝ} (D : Coefficients T U E) : ↥(EulerLpCylinderTranslation.CylinderL2 P U) →L[ℝ] ↥(EulerTimeH1FrameTransport.zeroTraceDerivatives T ⋯)

The genuine zero-trace correction to the affine terminal lift.

Equations

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

noncomputable def EulerCylinderDirichlet.Coefficients.endpointSlope {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (P : ℝ) [Fact (0 < P)] {T : ℝ} (D : Coefficients T U E) : ↥(EulerLpCylinderTranslation.CylinderL2 P U) →L[ℝ] ↥(EulerTimeLp.TimeLp T ↥(EulerLpCylinderTranslation.CylinderL2 P U))

The actual coordinate derivative in L² time.

Equations

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

noncomputable def EulerCylinderDirichlet.Coefficients.endpointDisplacement {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (P : ℝ) [Fact (0 < P)] {T : ℝ} (D : Coefficients T U E) : ↥(EulerLpCylinderTranslation.CylinderL2 P U) →L[ℝ] C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P U))

The actual coordinate displacement with prescribed terminal trace.

Equations

• EulerCylinderDirichlet.Coefficients.endpointDisplacement P D = EulerInitialTimePrimitive.initialPrimitive T ⋯ ∘SL EulerCylinderDirichlet.Coefficients.endpointSlope P D

noncomputable def EulerCylinderDirichlet.Coefficients.endpointCoordinate {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (P : ℝ) [Fact (0 < P)] {T : ℝ} (D : Coefficients T U E) : ↥(EulerLpCylinderTranslation.CylinderL2 P U) →L[ℝ] C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P U))

Bounded H¹ reconstruction of the stationary coordinate velocity.

Equations

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

noncomputable def EulerCylinderDirichlet.Coefficients.endpointAcceleration {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (P : ℝ) [Fact (0 < P)] {T : ℝ} (D : Coefficients T U E) : ↥(EulerLpCylinderTranslation.CylinderL2 P U) →L[ℝ] C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P U))

Its acceleration is the actual homogeneous right hand side.

Equations

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

noncomputable def EulerCylinderDirichlet.Coefficients.endpointVelocity {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (P : ℝ) [Fact (0 < P)] {T : ℝ} (D : Coefficients T U E) : ↥(EulerLpCylinderTranslation.CylinderL2 P U) →L[ℝ] C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E))

The physical history velocity, with a genuine L² terminal datum.

Equations

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

noncomputable def EulerCylinderDirichlet.Coefficients.endpointDerivative {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (P : ℝ) [Fact (0 < P)] {T : ℝ} (D : Coefficients T U E) : ↥(EulerLpCylinderTranslation.CylinderL2 P U) →L[ℝ] C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E))

The product-rule expression for the actual physical time derivative.

Equations

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

theorem EulerCylinderDirichlet.Coefficients.endpointDisplacement_initial {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (P : ℝ) [Fact (0 < P)] {T : ℝ} (D : Coefficients T U E) (Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U)) : ((endpointDisplacement P D) Y) ⟨0, ⋯⟩ = 0

theorem EulerCylinderDirichlet.Coefficients.endpointDisplacement_terminal {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (P : ℝ) [Fact (0 < P)] {T : ℝ} (D : Coefficients T U E) (Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U)) : ((endpointDisplacement P D) Y) ⟨T, ⋯⟩ = Y

theorem EulerCylinderDirichlet.Coefficients.endpointCoordinate_eq {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (P : ℝ) [Fact (0 < P)] {T : ℝ} (D : Coefficients T U E) (Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U)) (t : ↑(Set.Icc 0 T)) : ((endpointCoordinate P D) Y) t = EulerTransverseEndpointVelocity.coordinateVelocityPath T ⋯ (frame P D) (frameDerivative P D) D.lower ⋯ ⋯ (hessian P D) ((EulerTransverseFixedEndpoint.fixedEndpointDerivative T ⋯ (frame P D) (frameDerivative P D) (hessian P D) D.lower ⋯ ⋯ ⋯ D.potential ⋯ ⋯ ⋯ (EulerTransverseEndpointParameter.affineTrial T ⋯ (frame P D) (frameDerivative P D))) Y) ↑t

theorem EulerCylinderDirichlet.Coefficients.endpointCoordinate_ae {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (P : ℝ) [Fact (0 < P)] {T : ℝ} (D : Coefficients T U E) (Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U)) : ↑↑((endpointSlope P D) Y) =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T ⋯ ((endpointCoordinate P D) Y)

This reconstruction has the original L² coordinate derivative as its almost-everywhere representative.

theorem EulerCylinderDirichlet.Coefficients.endpointDisplacement_hasDerivWithinAt {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (P : ℝ) [Fact (0 < P)] {T : ℝ} (D : Coefficients T U E) (Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U)) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T ⋯ ((endpointDisplacement P D) Y)) (((endpointCoordinate P D) Y) t) (Set.Icc 0 T) ↑t

theorem EulerCylinderDirichlet.Coefficients.endpointCoordinate_hasDerivWithinAt {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (P : ℝ) [Fact (0 < P)] {T : ℝ} (D : Coefficients T U E) (Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U)) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T ⋯ ((endpointCoordinate P D) Y)) (((endpointAcceleration P D) Y) t) (Set.Icc 0 T) ↑t

Equation (10) holds throughout the closed time interval for the actual affine-terminal solution.

theorem EulerCylinderDirichlet.Coefficients.endpointVelocity_hasDerivWithinAt {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (P : ℝ) [Fact (0 < P)] {T : ℝ} (D : Coefficients T U E) (Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U)) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T ⋯ ((endpointVelocity P D) Y)) (((endpointDerivative P D) Y) t) (Set.Icc 0 T) ↑t

theorem EulerCylinderDirichlet.Coefficients.endpoint_projected_equation {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (P : ℝ) [Fact (0 < P)] {T : ℝ} (D : Coefficients T U E) (Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U)) (t : ↑(Set.Icc 0 T)) : (EulerTransverseGramInverse.gram ((frame P D) t)) (((endpointAcceleration P D) Y) t) = (ContinuousLinearMap.adjoint ((frame P D) t)) (-2 • ((frameDerivative P D) t) (((endpointCoordinate P D) Y) t))

The literal homogeneous projected equation, with no prescribed solution or strong derivative among the data.