The actual history inverse on the spatial-angular cylinder

The data below are pointwise coefficient hypotheses: a lower frame bound, the two time derivatives of the frame, its Jacobi equation and the Hessian upper bound. They construct the Dirichlet inverse on genuine cylinder L². Pointwise tangency is encoded by the frame range, not by orthogonality to one vector in L². No solution or operator inverse is part of the input data.

structure EulerCylinderDirichlet.Coefficients (T : ℝ) (U : Type u_3) (E : Type u_4) [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] : Type (max u_3 u_4)

Pointwise moving-frame data for the genuine history problem.

• time_pos : 0 < T
• Q : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (U →L[ℝ] E))

  Scale parameter of Coefficients, of type C(Icc (0 : ℝ) T,Space →ᵇ U →L[ℝ] E).

• Q₁ : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (U →L[ℝ] E))

  Q₁ of Coefficients, of type C(Icc (0 : ℝ) T,Space →ᵇ U →L[ℝ] E).

• Q₂ : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (U →L[ℝ] E))

  Q₂ of Coefficients, of type C(Icc (0 : ℝ) T,Space →ᵇ U →L[ℝ] E).

• H : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] E))

  H of Coefficients, of type C(Icc (0 : ℝ) T,Space →ᵇ E →L[ℝ] E).

• lower : ℝ

  Lower of Coefficients, of type ℝ.

• lower_pos : 0 < self.lower
• lower_bound (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U) : self.lower * ‖v‖ ^ 2 ≤ ‖((self.Q t) x) v‖ ^ 2
• derivative (t : ℝ) : t ∈ Set.Icc 0 T → ∀ (x : EulerSmoothLimit.Space), HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath T ⋯ self.Q s) x) ((EulerVolterraConvolution.extendPath T ⋯ self.Q₁ t) x) (Set.Icc 0 T) t
• second_derivative (t : ℝ) : t ∈ Set.Icc 0 T → ∀ (x : EulerSmoothLimit.Space), HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath T ⋯ self.Q₁ s) x) ((EulerVolterraConvolution.extendPath T ⋯ self.Q₂ t) x) (Set.Icc 0 T) t
• jacobi (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : U) : ((self.Q₂ t) x) v = -((self.H t) x) (((self.Q t) x) v)
• potential : ℝ

  Potential of Coefficients, of type ℝ.

• potential_nonneg : 0 ≤ self.potential
• potential_bound (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (v : E) : inner ℝ (((self.H t) x) v) v ≤ self.potential * ‖v‖ ^ 2
• small : self.potential * (T ^ 2 / 2) ≤ 1 / 2

noncomputable def EulerCylinderDirichlet.Coefficients.frame {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) : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P U) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P E))

Frame, given by fullPathMap P D.Q.

Equations

• EulerCylinderDirichlet.Coefficients.frame P D = (EulerLpCylinderRectangular.fullPathMap P) D.Q

noncomputable def EulerCylinderDirichlet.Coefficients.frameDerivative {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) : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P U) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P E))

Frame derivative, given by fullPathMap P D.Q₁.

Equations

• EulerCylinderDirichlet.Coefficients.frameDerivative P D = (EulerLpCylinderRectangular.fullPathMap P) D.Q₁

noncomputable def EulerCylinderDirichlet.Coefficients.frameSecond {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) : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P U) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P E))

Frame second, given by fullPathMap P D.Q₂.

Equations

• EulerCylinderDirichlet.Coefficients.frameSecond P D = (EulerLpCylinderRectangular.fullPathMap P) D.Q₂

noncomputable def EulerCylinderDirichlet.Coefficients.hessian {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) : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E) →L[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P E))

Hessian, given by fullPathMap P D.H.

Equations

• EulerCylinderDirichlet.Coefficients.hessian P D = (EulerLpCylinderRectangular.fullPathMap P) D.H

theorem EulerCylinderDirichlet.Coefficients.frame_lower {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) (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P U)) : D.lower * ‖u‖ ^ 2 ≤ ‖((frame P D) t) u‖ ^ 2

theorem EulerCylinderDirichlet.Coefficients.frame_derivative {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (P : ℝ) [Fact (0 < P)] {T : ℝ} (D : Coefficients T U E) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T ⋯ (frame P D)) ((frameDerivative P D) t) (Set.Icc 0 T) ↑t

theorem EulerCylinderDirichlet.Coefficients.frame_second_derivative {U : Type u_1} {E : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (P : ℝ) [Fact (0 < P)] {T : ℝ} (D : Coefficients T U E) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T ⋯ (frameDerivative P D)) ((frameSecond P D) t) (Set.Icc 0 T) ↑t

theorem EulerCylinderDirichlet.Coefficients.frame_equation {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) (t : ↑(Set.Icc 0 T)) : (frameSecond P D) t = -(hessian P D) t ∘SL (frame P D) t

theorem EulerCylinderDirichlet.Coefficients.hessian_upper {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) (t : ↑(Set.Icc 0 T)) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P E)) : inner ℝ (((hessian P D) t) u) u ≤ D.potential * ‖u‖ ^ 2

noncomputable def EulerCylinderDirichlet.Coefficients.coordinateSolver {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) : ↥(EulerTimeLp.TimeLp T ↥(EulerLpCylinderTranslation.CylinderL2 P E)) →L[ℝ] ↥(EulerTimeH1FrameTransport.zeroTraceDerivatives T ⋯)

The fixed-space coercive construction, with every L² hypothesis derived from the actual pointwise fields.

Equations

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

noncomputable def EulerCylinderDirichlet.Coefficients.velocityLp {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) : ↥(EulerTimeLp.TimeLp T ↥(EulerLpCylinderTranslation.CylinderL2 P E)) →L[ℝ] ↥(EulerTimeLp.TimeLp T ↥(EulerLpCylinderTranslation.CylinderL2 P U))

Velocity Lᵖ, constructed using EulerTransverseFixedEvolution.velocityLp.

Equations

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

noncomputable def EulerCylinderDirichlet.Coefficients.accelerationLp {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) : ↥(EulerTimeLp.TimeLp T ↥(EulerLpCylinderTranslation.CylinderL2 P E)) →L[ℝ] ↥(EulerTimeLp.TimeLp T ↥(EulerLpCylinderTranslation.CylinderL2 P U))

Acceleration Lᵖ, constructed using EulerTransverseFixedEvolution.accelerationLp.

Equations

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

noncomputable def EulerCylinderDirichlet.Coefficients.velocityPath {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) : ↥(EulerTimeLp.TimeLp T ↥(EulerLpCylinderTranslation.CylinderL2 P E)) →L[ℝ] C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P U))

Velocity path, constructed using EulerTransverseFixedEvolution.velocityPath.

Equations

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

noncomputable def EulerCylinderDirichlet.Coefficients.accelerationPath {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) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E))) : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P U))

Acceleration path, constructed using EulerTransverseFixedEvolution.classicalAcceleration.

Equations

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

noncomputable def EulerCylinderDirichlet.Coefficients.displacementPath {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) (f : ↥(EulerTimeLp.TimeLp T ↥(EulerLpCylinderTranslation.CylinderL2 P E))) : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P U))

Displacement path, constructed using EulerTransverseFixedEvolution.displacementPath.

Equations

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

noncomputable def EulerCylinderDirichlet.Coefficients.physicalVelocity {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) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E))) : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E))

Physical velocity, constructed using EulerTransverseFixedEvolution.physicalVelocityPath.

Equations

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

noncomputable def EulerCylinderDirichlet.Coefficients.physicalDerivative {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) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E))) : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E))

Physical derivative, constructed using EulerTransverseFixedEvolution.physicalDerivativePath.

Equations

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

theorem EulerCylinderDirichlet.Coefficients.displacement_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) (f : ↥(EulerTimeLp.TimeLp T ↥(EulerLpCylinderTranslation.CylinderL2 P E))) : (displacementPath P D f) ⟨0, ⋯⟩ = 0

theorem EulerCylinderDirichlet.Coefficients.displacement_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) (f : ↥(EulerTimeLp.TimeLp T ↥(EulerLpCylinderTranslation.CylinderL2 P E))) : (displacementPath P D f) ⟨T, ⋯⟩ = 0

theorem EulerCylinderDirichlet.Coefficients.velocity_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) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E))) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T ⋯ ((velocityPath P D) (EulerTimeLp.pathLp T ⋯ f))) ((accelerationPath P D f) t) (Set.Icc 0 T) ↑t

theorem EulerCylinderDirichlet.Coefficients.displacement_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) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E))) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T ⋯ (displacementPath P D (EulerTimeLp.pathLp T ⋯ f))) (((velocityPath P D) (EulerTimeLp.pathLp T ⋯ f)) t) (Set.Icc 0 T) ↑t

theorem EulerCylinderDirichlet.Coefficients.physicalVelocity_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) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E))) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T ⋯ (physicalVelocity P D f)) ((physicalDerivative P D f) t) (Set.Icc 0 T) ↑t

theorem EulerCylinderDirichlet.Coefficients.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) (f : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P E))) (t : ↑(Set.Icc 0 T)) : (EulerTransverseGramInverse.gram ((frame P D) t)) ((accelerationPath P D f) t) = (ContinuousLinearMap.adjoint ((frame P D) t)) (f t - 2 • ((frameDerivative P D) t) (((velocityPath P D) (EulerTimeLp.pathLp T ⋯ f)) t))

The exact projected equation (10), now as an equality of actual spatial - angular L² fields at every time.