Source deformation data for the concrete transverse packet provider

Only the prescribed deformation, its inverse, and their actual time identity are inputs. The transverse frame, normal, both coercivity constants, and all geometry needed by the forward solve are derived below.

Source geometry for the bounded frame and normal

The literal fields Q=F R⊥ and m=F⁻ᵀm₀ satisfy the tangency, range, strain, and quantitative normal lower bounds used by the actual transverse solver. Only the original deformation and its genuine pointwise inverse are inputs.

The literal source frame as a uniformly smooth bounded coefficient path

The reference-plane restriction is a fixed linear contraction. The actual source fields F and F_t therefore construct the full bounded frame fields, with their genuine jets and time derivative. A pointwise bound on F⁻¹ proves the uniform frame coercivity used by the constructed Gram inverse.

theorem EulerTransverseBoundedFrame.restriction_norm {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m₀ : EulerSmoothLimit.Space) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m₀)) : ‖EulerTransverseSourceCoefficientPath.referenceRestriction m₀ R‖ ≤ 1

Restricting a matrix to the orthonormal reference plane is a contraction.

noncomputable def EulerTransverseBoundedFrame.coefficient {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m₀ : EulerSmoothLimit.Space) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m₀)) {K : Type u_2} [TopologicalSpace K] [CompactSpace K] (F : EulerMeanCoefficients.SmoothCoefficientPath K (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) : EulerMeanCoefficients.SmoothCoefficientPath K (U →L[ℝ] EulerSmoothLimit.Space)

The actual source F R⊥, including all its uniformly continuous spatial jets.

Equations

• EulerTransverseBoundedFrame.coefficient m₀ R F = EulerMeanCoefficients.SmoothCoefficientPath.map (EulerTransverseSourceCoefficientPath.referenceRestriction m₀ R) F

@[simp]

theorem EulerTransverseBoundedFrame.coefficient_apply {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m₀ : EulerSmoothLimit.Space) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m₀)) {K : Type u_2} [TopologicalSpace K] [CompactSpace K] (F : EulerMeanCoefficients.SmoothCoefficientPath K (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (t : K) (x : EulerSmoothLimit.Space) (v : U) : (((coefficient m₀ R F).field t) x) v = ((F.field t) x) ↑(R v)

theorem EulerTransverseBoundedFrame.coefficient_derivative_bound {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m₀ : EulerSmoothLimit.Space) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m₀)) {K : Type u_2} [TopologicalSpace K] [CompactSpace K] (F : EulerMeanCoefficients.SmoothCoefficientPath K (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (n : ℕ) (C : ℝ) (hF : ∀ (t : K) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(F.field t)) x‖ ≤ C) (t : K) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (⇑((coefficient m₀ R F).field t)) x‖ ≤ C

The original pointwise source coefficient derivative bound survives without loss.

theorem EulerTransverseBoundedFrame.coefficient_lower {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m₀ : EulerSmoothLimit.Space) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m₀)) {K : Type u_2} [TopologicalSpace K] [CompactSpace K] (F : EulerMeanCoefficients.SmoothCoefficientPath K (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (FInv : K → EulerSmoothLimit.Space → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (B : ℝ) (hB : 0 < B) (hInv : ∀ (t : K) (x v : EulerSmoothLimit.Space), (FInv t x) (((F.field t) x) v) = v) (hNorm : ∀ (t : K) (x : EulerSmoothLimit.Space), ‖FInv t x‖ ≤ B) (t : K) (x : EulerSmoothLimit.Space) (v : U) : B⁻¹ ^ 2 * ‖v‖ ^ 2 ≤ ‖(((coefficient m₀ R F).field t) x) v‖ ^ 2

The uniform inverse-frame bound gives the precise squared lower frame bound.

theorem EulerTransverseBoundedFrame.coefficient_hasDerivWithinAt {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m₀ : EulerSmoothLimit.Space) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m₀)) (T : ℝ) (hT : 0 ≤ T) (F F₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (hF : ∀ t ∈ Set.Icc 0 T, ∀ (x : EulerSmoothLimit.Space), HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath T hT F.field s) x) ((EulerVolterraConvolution.extendPath T hT F₁.field t) x) (Set.Icc 0 T) t) (t : ℝ) (ht : t ∈ Set.Icc 0 T) (x : EulerSmoothLimit.Space) : HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath T hT (coefficient m₀ R F).field s) x) ((EulerVolterraConvolution.extendPath T hT (coefficient m₀ R F₁).field t) x) (Set.Icc 0 T) t

The actual source time derivative also commutes with the reference restriction.

noncomputable def EulerTransverseBoundedFrame.normalMap (m₀ : EulerSmoothLimit.Space) : (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) →L[ℝ] EulerSmoothLimit.Space

The fixed linear operation sending F⁻¹ to F⁻ᵀm₀.

Equations

• EulerTransverseBoundedFrame.normalMap m₀ = (ContinuousLinearMap.apply ℝ EulerSmoothLimit.Space) m₀ ∘SL ↑↑ContinuousLinearMap.adjoint

@[simp]

theorem EulerTransverseBoundedFrame.normalMap_apply (m₀ : EulerSmoothLimit.Space) (A : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : (normalMap m₀) A = (ContinuousLinearMap.adjoint A) m₀

theorem EulerTransverseBoundedFrame.normalMap_norm (m₀ : EulerSmoothLimit.Space) (hm₀ : ‖m₀‖ = 1) : ‖normalMap m₀‖ ≤ 1

noncomputable def EulerTransverseBoundedFrame.normalCoefficient (m₀ : EulerSmoothLimit.Space) {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (FInv : EulerMeanCoefficients.SmoothCoefficientPath K (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) : EulerMeanCoefficients.SmoothCoefficientPath K EulerSmoothLimit.Space

The normal has the genuine spatial jets inherited from the inverse deformation.

Equations

• EulerTransverseBoundedFrame.normalCoefficient m₀ FInv = EulerMeanCoefficients.SmoothCoefficientPath.map (EulerTransverseBoundedFrame.normalMap m₀) FInv

@[simp]

theorem EulerTransverseBoundedFrame.normalCoefficient_apply (m₀ : EulerSmoothLimit.Space) {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (FInv : EulerMeanCoefficients.SmoothCoefficientPath K (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (t : K) (x : EulerSmoothLimit.Space) : ((normalCoefficient m₀ FInv).field t) x = (ContinuousLinearMap.adjoint ((FInv.field t) x)) m₀

theorem EulerTransverseBoundedFrame.normalCoefficient_derivative_bound (m₀ : EulerSmoothLimit.Space) {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (FInv : EulerMeanCoefficients.SmoothCoefficientPath K (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (hm₀ : ‖m₀‖ = 1) (n : ℕ) (C : ℝ) (hF : ∀ (t : K) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(FInv.field t)) x‖ ≤ C) (t : K) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (⇑((normalCoefficient m₀ FInv).field t)) x‖ ≤ C

theorem EulerTransverseBoundedFrame.coefficient_tangent (m₀ : EulerSmoothLimit.Space) {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {U : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m₀)) (F FInv : EulerMeanCoefficients.SmoothCoefficientPath K (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (hInv : ∀ (t : K) (x v : EulerSmoothLimit.Space), ((FInv.field t) x) (((F.field t) x) v) = v) (t : K) (x : EulerSmoothLimit.Space) (v : U) : inner ℝ (((normalCoefficient m₀ FInv).field t) x) ((((coefficient m₀ R F).field t) x) v) = 0

theorem EulerTransverseBoundedFrame.coefficient_range (m₀ : EulerSmoothLimit.Space) {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {U : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m₀)) (F FInv : EulerMeanCoefficients.SmoothCoefficientPath K (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (hInv : ∀ (t : K) (x v : EulerSmoothLimit.Space), ((F.field t) x) (((FInv.field t) x) v) = v) (t : K) (x η : EulerSmoothLimit.Space) (hη : inner ℝ (((normalCoefficient m₀ FInv).field t) x) η = 0) : ∃ (v : U), (((coefficient m₀ R F).field t) x) v = η

theorem EulerTransverseBoundedFrame.coefficient_strain (m₀ : EulerSmoothLimit.Space) {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {U : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m₀)) (F F₁ M : EulerMeanCoefficients.SmoothCoefficientPath K (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (hFlow : ∀ (t : K) (x v : EulerSmoothLimit.Space), ((F₁.field t) x) v = ((M.field t) x) (((F.field t) x) v)) (t : K) (x : EulerSmoothLimit.Space) : ((coefficient m₀ R F₁).field t) x = (M.field t) x ∘SL ((coefficient m₀ R F).field t) x

theorem EulerTransverseBoundedFrame.normalCoefficient_lower (m₀ : EulerSmoothLimit.Space) {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (F FInv : EulerMeanCoefficients.SmoothCoefficientPath K (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (hm₀ : ‖m₀‖ = 1) (hInv : ∀ (t : K) (x v : EulerSmoothLimit.Space), ((FInv.field t) x) (((F.field t) x) v) = v) (B : ℝ) (hB : 0 < B) (hFnorm : ∀ (t : K) (x : EulerSmoothLimit.Space), ‖(F.field t) x‖ ≤ B) (t : K) (x : EulerSmoothLimit.Space) : B⁻¹ ^ 2 ≤ ‖((normalCoefficient m₀ FInv).field t) x‖ ^ 2

The source inverse identity also prevents degeneration of the normal.

structure EulerTransversePacketProvider.Data (U : Type u_1) [NormedAddCommGroup U] [InnerProductSpace ℝ U] : Type u_1

Data, collecting T, T_pos, support, support_compact, m₀, m₀_unit and their compatibility conditions.

• T : ℝ

  Time horizon of Data, of type ℝ.

• T_pos : 0 < self.T
• support : Set EulerSmoothLimit.Space

  Support set of Data, of type Set Space.

• support_compact : IsCompact self.support
• m₀ : EulerSmoothLimit.Space

  M₀ of Data, of type Space.

• m₀_unit : ‖self.m₀‖ = 1
• R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane self.m₀)

  Radius parameter of Data, of type U ≃ₗᵢ[ℝ] referencePlane m₀.

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

  F of Data, of type SmoothCoefficientPath (Icc (0 : ℝ) T) (Space →L[ℝ] Space).

• F₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 self.T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

  F₁ of Data, of type SmoothCoefficientPath (Icc (0 : ℝ) T) (Space →L[ℝ] Space).

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

  F inv of Data, of type SmoothCoefficientPath (Icc (0 : ℝ) T) (Space →L[ℝ] Space).

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

  M of Data, of type SmoothCoefficientPath (Icc (0 : ℝ) T) (Space →L[ℝ] Space).

• inverse_left (t : ↑(Set.Icc 0 self.T)) (x v : EulerSmoothLimit.Space) : ((self.FInv.field t) x) (((self.F.field t) x) v) = v
• inverse_right (t : ↑(Set.Icc 0 self.T)) (x v : EulerSmoothLimit.Space) : ((self.F.field t) x) (((self.FInv.field t) x) v) = v
• frame_time (t : ℝ) : t ∈ Set.Icc 0 self.T → ∀ (x : EulerSmoothLimit.Space), HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath self.T ⋯ self.F.field s) x) ((EulerVolterraConvolution.extendPath self.T ⋯ self.F₁.field t) x) (Set.Icc 0 self.T) t
• strain_equation (t : ↑(Set.Icc 0 self.T)) (x v : EulerSmoothLimit.Space) : ((self.F₁.field t) x) v = ((self.M.field t) x) (((self.F.field t) x) v)

theorem EulerTransversePacketProvider.Data.support_measurable {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : MeasurableSet D.support

@[reducible, inline]

noncomputable abbrev EulerTransversePacketProvider.Data.frame {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 D.T)) (U →L[ℝ] EulerSmoothLimit.Space)

Frame: an abbreviation for coefficient D.m₀ D.R D.F.

Equations

• D.frame = EulerTransverseBoundedFrame.coefficient D.m₀ D.R D.F

@[reducible, inline]

noncomputable abbrev EulerTransversePacketProvider.Data.frameDerivative {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 D.T)) (U →L[ℝ] EulerSmoothLimit.Space)

Frame derivative: an abbreviation for coefficient D.m₀ D.R D.F₁.

Equations

• D.frameDerivative = EulerTransverseBoundedFrame.coefficient D.m₀ D.R D.F₁

@[reducible, inline]

noncomputable abbrev EulerTransversePacketProvider.Data.normal {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 D.T)) EulerSmoothLimit.Space

Normal: an abbreviation for normalCoefficient D.m₀ D.FInv.

Equations

• D.normal = EulerTransverseBoundedFrame.normalCoefficient D.m₀ D.FInv

noncomputable def EulerTransversePacketProvider.Data.inverseBound {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : ℝ

Inverse bound, given by 1+‖D.FInv.field‖.

Equations

• D.inverseBound = 1 + ‖D.FInv.field‖

noncomputable def EulerTransversePacketProvider.Data.frameBound {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : ℝ

Frame bound, given by 1+‖D.F.field‖.

Equations

• D.frameBound = 1 + ‖D.F.field‖

noncomputable def EulerTransversePacketProvider.Data.frameLower {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : ℝ

Frame lower, given by D.inverseBound⁻¹^2.

Equations

• D.frameLower = D.inverseBound⁻¹ ^ 2

noncomputable def EulerTransversePacketProvider.Data.normalLower {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : ℝ

Normal lower, given by D.frameBound⁻¹^2.

Equations

• D.normalLower = D.frameBound⁻¹ ^ 2

theorem EulerTransversePacketProvider.Data.inverseBound_pos {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : 0 < D.inverseBound

theorem EulerTransversePacketProvider.Data.frameBound_pos {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : 0 < D.frameBound

theorem EulerTransversePacketProvider.Data.frameLower_pos {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : 0 < D.frameLower

theorem EulerTransversePacketProvider.Data.normalLower_pos {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : 0 < D.normalLower

theorem EulerTransversePacketProvider.Data.inverse_norm {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ‖(D.FInv.field t) x‖ ≤ D.inverseBound

theorem EulerTransversePacketProvider.Data.frame_norm {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ‖(D.F.field t) x‖ ≤ D.frameBound

theorem EulerTransversePacketProvider.Data.frame_lower {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (v : U) : D.frameLower * ‖v‖ ^ 2 ≤ ‖((D.frame.field t) x) v‖ ^ 2

Uniform coercivity follows from the actual inverse deformation.

theorem EulerTransversePacketProvider.Data.normal_lower {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : D.normalLower ≤ ‖(D.normal.field t) x‖ ^ 2

The scalar pressure inverse is nondegenerate by the same source identity.

theorem EulerTransversePacketProvider.Data.frame_tangent {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (v : U) : inner ℝ ((D.normal.field t) x) (((D.frame.field t) x) v) = 0

theorem EulerTransversePacketProvider.Data.frame_range {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (t : ↑(Set.Icc 0 D.T)) (x η : EulerSmoothLimit.Space) (hη : inner ℝ ((D.normal.field t) x) η = 0) : ∃ (v : U), ((D.frame.field t) x) v = η

theorem EulerTransversePacketProvider.Data.frame_strain {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : (D.frameDerivative.field t) x = (D.M.field t) x ∘SL (D.frame.field t) x

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