The actual parent label fields construct both source-provider data records. Their coefficient agreement, inverses and time identities are conclusions. Only the manuscript's scalar low-order guards remain inputs.

The ordinary three-dimensional coefficient interface is a literal restriction of the generic smooth time-field interface.

def SmoothTimeField.toSmoothCoefficientPath {K V : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothTimeField K EulerSmoothLimit.Space V) : EulerMeanCoefficients.SmoothCoefficientPath K V

To smooth coefficient path, given by ⟨A.field,A.smooth,A.jet,A.jet_eq⟩.

Equations

• A.toSmoothCoefficientPath = { field := A.field, smooth := ⋯, jet := A.jet, jet_eq := ⋯ }

@[simp]

theorem SmoothTimeField.toSmoothCoefficientPath_field {K V : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothTimeField K EulerSmoothLimit.Space V) : A.toSmoothCoefficientPath.field = A.field

@[simp]

theorem SmoothTimeField.toSmoothCoefficientPath_jet {K V : Type} [TopologicalSpace K] [CompactSpace K] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothTimeField K EulerSmoothLimit.Space V) (n : ℕ) : A.toSmoothCoefficientPath.jet n = A.jet n

structure EulerParentPacketFrames.LowBounds (G : Parent) : Type

Low bounds data, collecting Be, Bc, L, r, K, Be_nonneg and their compatibility conditions.

• Be : ℝ

  Be of LowBounds, of type ℝ.

• Bc : ℝ

  Bc of LowBounds, of type ℝ.

• L : ℝ

  L of LowBounds, of type ℝ.

• r : ℝ

  R of LowBounds, of type ℝ.

• K : ℝ

  K of LowBounds, of type ℝ.

• Be_nonneg : 0 ≤ self.Be
• Bc_nonneg : 0 ≤ self.Bc
• L_lower : EulerMeanHarmonic.boundaryLocalizationC1 * self.Bc ≤ self.L
• r_nonneg : 0 ≤ self.r
• r_le_quarter : self.r ≤ 1 / 4
• K_nonneg : 0 ≤ self.K
• exterior_lower (x : EulerSmoothLimit.Space) : self.r ≤ ‖G.ell • x‖ → ∀ (v : EulerSmoothLimit.Space), -self.Be * ‖v‖ ^ 2 ≤ inner ℝ ((G.initialStrain.field x) v) v
• core_lower (x : EulerSmoothLimit.Space) : ‖G.ell • x‖ < self.r → ∀ (v : EulerSmoothLimit.Space), -self.Bc * ‖v‖ ^ 2 ≤ inner ℝ ((G.initialStrain.field x) v) v
• curvature_upper (t : ↑(Set.Icc 0 G.T)) (x v : EulerSmoothLimit.Space) : inner ℝ (((G.curvature.field t) x) v) v ≤ self.K * ‖v‖ ^ 2
• small : self.K * (G.T ^ 2 / 2) + self.Be * G.T + EulerMeanHarmonic.boundaryLocalizationC2 * self.Bc * self.r ^ 3 * G.T ≤ 1 / 2

theorem EulerParentPacketFrames.Parent.frame_within (G : Parent) (t : ℝ) (ht : t ∈ Set.Icc 0 G.T) (x : EulerSmoothLimit.Space) : HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath G.T ⋯ G.frame.field s) x) ((EulerVolterraConvolution.extendPath G.T ⋯ G.first.field t) x) (Set.Icc 0 G.T) t

theorem EulerParentPacketFrames.Parent.first_within (G : Parent) (t : ℝ) (ht : t ∈ Set.Icc 0 G.T) (x : EulerSmoothLimit.Space) : HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath G.T ⋯ G.first.field s) x) ((EulerVolterraConvolution.extendPath G.T ⋯ G.second.field t) x) (Set.Icc 0 G.T) t

noncomputable def EulerParentPacketFrames.Parent.meanData (G : Parent) (H : LowBounds G) : EulerMeanPacketProvider.Data

Mean data, bundling T, T_pos, ℓ, ℓ_pos and the required compatibility proofs.

Equations

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

noncomputable def EulerParentPacketFrames.Parent.transverseData (G : Parent) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) : EulerTransversePacketProvider.Data U

Transverse data, bundling T, T_pos, support, support_compact and the required compatibility proofs.

Equations

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

theorem EulerParentPacketFrames.Parent.sourceAgreement (G : Parent) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (H : LowBounds G) : EulerPacketCylinderField.SourceCoefficientAgreement (G.meanData H) (G.transverseData m hm R S hS)

theorem EulerParentPacketFrames.Parent.history_small (G : Parent) (H : LowBounds G) : H.K * (G.T ^ 2 / 2) ≤ 1 / 2

noncomputable def EulerParentPacketFrames.Parent.historyData (G : Parent) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (H : LowBounds G) : EulerTransversePacketProvider.HistoryData (G.transverseData m hm R S hS)

History data, bundling H, jacobi, have, potential and the required compatibility proofs.

Equations

• G.historyData m hm R S hS H = { H := G.curvature.toSmoothCoefficientPath, jacobi := ⋯, potential := H.K, potential_nonneg := ⋯, potential_bound := ⋯, small := ⋯ }