Source Hessian data construct the transverse history inverse

The additional inputs are the manuscript's literal Jacobi identity F_tt = -H F and upper Hessian bound. The full-cylinder Dirichlet inverse, its true time derivatives, and all endpoint conditions are constructed by the previously proved coercive solve. No solution is an input.

structure EulerTransversePacketProvider.HistoryData {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : Type

The original Hessian law and upper bound, before the actual solve.

• H : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 D.T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

  H of HistoryData, of type SmoothCoefficientPath (Icc (0 : ℝ) D.T) (Space →L[ℝ] Space).

• jacobi (t : ℝ) : t ∈ Set.Icc 0 D.T → ∀ (x : EulerSmoothLimit.Space), HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath D.T ⋯ D.F₁.field s) x) (-(EulerVolterraConvolution.extendPath D.T ⋯ self.H.field t) x ∘SL (EulerVolterraConvolution.extendPath D.T ⋯ D.F.field t) x) (Set.Icc 0 D.T) t
• potential : ℝ

  Potential of HistoryData, of type ℝ.

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

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.HistoryData.instTransversePacketHistoryData1 : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

Cache the standard NormedAddCommGroup (Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerTransversePacketProvider.HistoryData.instTransversePacketHistoryData1 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.HistoryData.instTransversePacketHistoryData2 : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

Cache the standard NormedSpace ℝ (Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerTransversePacketProvider.HistoryData.instTransversePacketHistoryData2 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.HistoryData.instTransversePacketHistoryData3 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedAddCommGroup (U →L[ℝ] EulerSmoothLimit.Space)

Cache the standard NormedAddCommGroup (U →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerTransversePacketProvider.HistoryData.instTransversePacketHistoryData3 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.HistoryData.instTransversePacketHistoryData4 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedSpace ℝ (U →L[ℝ] EulerSmoothLimit.Space)

Cache the standard NormedSpace ℝ (U →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerTransversePacketProvider.HistoryData.instTransversePacketHistoryData4 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.HistoryData.instTransversePacketHistoryData5 : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedAddCommGroup (Space →ᵇ Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerTransversePacketProvider.HistoryData.instTransversePacketHistoryData5 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.HistoryData.instTransversePacketHistoryData6 : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedSpace ℝ (Space →ᵇ Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerTransversePacketProvider.HistoryData.instTransversePacketHistoryData6 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.HistoryData.instTransversePacketHistoryData7 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (U →L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedAddCommGroup (Space →ᵇ U →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerTransversePacketProvider.HistoryData.instTransversePacketHistoryData7 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.HistoryData.instTransversePacketHistoryData8 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space (U →L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedSpace ℝ (Space →ᵇ U →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerTransversePacketProvider.HistoryData.instTransversePacketHistoryData8 = inferInstance

noncomputable def EulerTransversePacketProvider.HistoryData.frameSecond {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : Data U} (B : HistoryData D) : C(↑(Set.Icc 0 D.T), BoundedContinuousFunction EulerSmoothLimit.Space (U →L[ℝ] EulerSmoothLimit.Space))

The second frame derivative is the prescribed Hessian product.

Equations

• B.frameSecond = -(EulerBoundedFieldCalculus.pathCompositionMap B.H.field) D.frame.field

@[simp]

theorem EulerTransversePacketProvider.HistoryData.frameSecond_apply {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : Data U} (B : HistoryData D) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (v : U) : ((B.frameSecond t) x) v = -((B.H.field t) x) (((D.frame.field t) x) v)

theorem EulerTransversePacketProvider.HistoryData.frameSecond_derivative {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : Data U} (B : HistoryData D) (t : ℝ) (ht : t ∈ Set.Icc 0 D.T) (x : EulerSmoothLimit.Space) : HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath D.T ⋯ D.frameDerivative.field s) x) ((EulerVolterraConvolution.extendPath D.T ⋯ B.frameSecond t) x) (Set.Icc 0 D.T) t

noncomputable def EulerTransversePacketProvider.HistoryData.coefficients {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : Data U} (B : HistoryData D) : EulerCylinderDirichlet.Coefficients D.T U EulerSmoothLimit.Space

The genuine spatial-angular L² inverse data, with uniform coercivity derived from the actual inverse deformation.

Equations

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

theorem EulerTransversePacketProvider.HistoryData.coefficient_frame {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : Data U} (B : HistoryData D) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (v : U) : ((B.coefficients.Q t) x) v = ((D.F.field t) x) ↑(D.R v)

theorem EulerTransversePacketProvider.HistoryData.coefficient_hessian {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : Data U} (B : HistoryData D) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : (B.coefficients.H t) x = (B.H.field t) x