The actual cylinder endpoint inverse is affine data minus the genuine zero-endpoint inverse of its explicit forcing. These identities transfer the already proved support, translation and same-radius estimates to the nonzero-terminal construction.

The affine endpoint correction as an actual forced Dirichlet solve

For the affine coordinate lift t Y / T, the Jacobi identity cancels the potential term. Its variational correction is exactly the already constructed zero-endpoint inverse applied to 2 Q₁(t) (Y/T).

noncomputable def EulerFixedEndpointForcing.affineVelocity {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (Y : U) : C(↑(Set.Icc 0 T), E)

Affine velocity as an element of C(Icc (0 : ℝ) T,E).

Equations

• EulerFixedEndpointForcing.affineVelocity T Q Q₁ Y = { toFun := fun (t : ↑(Set.Icc 0 T)) => (Q₁ t) (↑t • T⁻¹ • Y) + (Q t) (T⁻¹ • Y), continuous_toFun := ⋯ }

noncomputable def EulerFixedEndpointForcing.affineAcceleration {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (Q₁ Q₂ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (Y : U) : C(↑(Set.Icc 0 T), E)

Affine acceleration as an element of C(Icc (0 : ℝ) T,E).

Equations

• EulerFixedEndpointForcing.affineAcceleration T Q₁ Q₂ Y = { toFun := fun (t : ↑(Set.Icc 0 T)) => (Q₂ t) (↑t • T⁻¹ • Y) + 2 • (Q₁ t) (T⁻¹ • Y), continuous_toFun := ⋯ }

noncomputable def EulerFixedEndpointForcing.affineForcing {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) : U →L[ℝ] C(↑(Set.Icc 0 T), E)

The genuine affine forcing, as a bounded linear function of terminal data.

Equations

• EulerFixedEndpointForcing.affineForcing T Q₁ = 2 • EulerContinuousTimeIntegral.multiplier Q₁ ∘SL ContinuousLinearMap.const ℝ ↑(Set.Icc 0 T) ∘SL (T⁻¹ • ContinuousLinearMap.id ℝ U)

theorem EulerFixedEndpointForcing.affineTrial_eq_pathLp {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (Y : U) : (EulerTransverseEndpointParameter.affineTrial T hT Q Q₁) Y = EulerTimeLp.pathLp T hT (affineVelocity T Q Q₁ Y)

theorem EulerFixedEndpointForcing.affineVelocity_hasDerivWithinAt {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ Q₂ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) (hd₁ : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q₁) (Q₂ t) (Set.Icc 0 T) ↑t) (Y : U) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (affineVelocity T Q Q₁ Y)) ((affineAcceleration T Q₁ Q₂ Y) t) (Set.Icc 0 T) ↑t

theorem EulerFixedEndpointForcing.affineAcceleration_add_potential {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ Q₂ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) (hframe : ∀ (t : ↑(Set.Icc 0 T)), Q₂ t = -H t ∘SL Q t) (Y : U) : EulerTimeLp.pathLp T hT (affineAcceleration T Q₁ Q₂ Y) + (EulerTimeLp.timeMultiplier T hT H) ((EulerInitialTimePrimitive.initialPrimitiveTimeLp T hT) ((EulerTransverseEndpointParameter.affineTrial T hT Q Q₁) Y)) = EulerTimeLp.pathLp T hT ((affineForcing T Q₁) Y)

theorem EulerFixedEndpointForcing.affine_energy_pairing {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ Q₂ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) (hd₁ : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q₁) (Q₂ t) (Set.Icc 0 T) ↑t) (hframe : ∀ (t : ↑(Set.Icc 0 T)), Q₂ t = -H t ∘SL Q t) (Y : U) (v : ↥(EulerTimeH1FrameTransport.zeroTraceDerivatives T hT)) : inner ℝ ((EulerTransverseEndpointEnergy.energyOperator T hT H) ((EulerTransverseEndpointParameter.affineTrial T hT Q Q₁) Y)) ((EulerTransverseFixedSpaceInverse.fixedFrameDerivative T hT Q Q₁) v) = -inner ℝ (EulerTimeLp.pathLp T hT ((affineForcing T Q₁) Y)) ((EulerTransverseFixedSpaceInverse.fixedFramePrimitive T hT Q Q₁) v)

The exact affine energy pairing, obtained by genuine integration by parts.

theorem EulerFixedEndpointForcing.correction_eq_forced {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 ≤ T) (Q Q₁ Q₂ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q) (Q₁ t) (Set.Icc 0 T) ↑t) (hd₁ : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT Q₁) (Q₂ t) (Set.Icc 0 T) ↑t) (hframe : ∀ (t : ↑(Set.Icc 0 T)), Q₂ t = -H t ∘SL Q t) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖(Q t) v‖ ^ 2) (K : ℝ) (hK : 0 ≤ K) (hH : ∀ (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ ((H t) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) (Y : U) : (EulerTransverseFixedEndpoint.fixedEndpointCorrection T hT Q Q₁ H c hc hQ hd K hK hH hsmall (EulerTransverseEndpointParameter.affineTrial T hT Q Q₁)) Y = (EulerTransverseFixedSpaceInverse.fixedFrameSolver T hT Q Q₁ H c hc hQ hd K hK hH hsmall) (EulerTimeLp.pathLp T hT ((affineForcing T Q₁) Y))

The stationary affine correction is exactly the forced inverse applied to the explicit source 2 Q₁ Y/T; no new inverse is assumed.

noncomputable def EulerCylinderDirichlet.Coefficients.endpointForcing {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ 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 exact forcing of the affine endpoint correction.

Equations

• EulerCylinderDirichlet.Coefficients.endpointForcing P D = EulerFixedEndpointForcing.affineForcing T (EulerCylinderDirichlet.Coefficients.frameDerivative P D)

theorem EulerCylinderDirichlet.Coefficients.endpointForcing_apply {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (P : ℝ) [Fact (0 < P)] {T : ℝ} (D : Coefficients T U E) (Y : ↥(EulerLpCylinderTranslation.CylinderL2 P U)) (t : ↑(Set.Icc 0 T)) : ((endpointForcing P D) Y) t = 2 • ((frameDerivative P D) t) (T⁻¹ • Y)

theorem EulerCylinderDirichlet.Coefficients.endpointCorrection_eq_forced {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)) : (endpointCorrection P D) Y = (coordinateSolver P D) (EulerTimeLp.pathLp T ⋯ ((endpointForcing P D) Y))

Equality of the genuinely constructed corrections, not a new solution assumption.

theorem EulerCylinderDirichlet.Coefficients.endpointSlope_eq_const_sub {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 = (EulerInitialTimePrimitive.constantFieldOperator T ⋯) (T⁻¹ • Y) - (velocityLp P D) (EulerTimeLp.pathLp T ⋯ ((endpointForcing P D) Y))

theorem EulerCylinderDirichlet.Coefficients.endpointDisplacement_eq_affine_sub {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)) : ((endpointDisplacement P D) Y) t = ↑t • T⁻¹ • Y - (displacementPath P D (EulerTimeLp.pathLp T ⋯ ((endpointForcing P D) Y))) t

theorem EulerCylinderDirichlet.Coefficients.endpointCoordinate_eq_const_sub {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 = T⁻¹ • Y - ((velocityPath P D) (EulerTimeLp.pathLp T ⋯ ((endpointForcing P D) Y))) t

Equality in continuous time follows from the true displacement derivative, including the endpoint derivatives.

theorem EulerCylinderDirichlet.Coefficients.endpointCoordinate_eq_forced {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)) : (endpointCoordinate P D) Y = ContinuousMap.const (↑(Set.Icc 0 T)) (T⁻¹ • Y) - (velocityPath P D) (EulerTimeLp.pathLp T ⋯ ((endpointForcing P D) Y))

theorem EulerCylinderDirichlet.Coefficients.endpointAcceleration_eq_forced {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)) : (endpointAcceleration P D) Y = -accelerationPath P D ((endpointForcing P D) Y)

theorem EulerCylinderDirichlet.Coefficients.endpointVelocity_eq_forced {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)) : (endpointVelocity P D) Y = (EulerContinuousTimeIntegral.multiplier (frame P D)) (ContinuousMap.const (↑(Set.Icc 0 T)) (T⁻¹ • Y)) - physicalVelocity P D ((endpointForcing P D) Y)

theorem EulerCylinderDirichlet.Coefficients.endpointDerivative_eq_forced {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)) : (endpointDerivative P D) Y = (EulerContinuousTimeIntegral.multiplier (frameDerivative P D)) (ContinuousMap.const (↑(Set.Icc 0 T)) (T⁻¹ • Y)) - physicalDerivative P D ((endpointForcing P D) Y)