The nonlinear packet coefficient budget follows from the original spatial jets of the inverse deformation and strain. The transported unit normal uses the same radius and amplitude.

theorem EulerPacketCylinderField.MatrixCoefficient.path_eq_of_raw_eq {T : ℝ} {raw raw' : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (G : MatrixCoefficient T raw) (H : MatrixCoefficient T raw') (he : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, x, θ) = raw' (↑t, x, θ)) : G.path = H.path

theorem EulerPacketCylinderField.VectorCoefficient.path_eq_of_raw_eq {T : ℝ} {raw raw' : EulerPacketProfileRecursion.VectorField} (G : VectorCoefficient T raw) (H : VectorCoefficient T raw') (he : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, x, θ) = raw' (↑t, x, θ)) : G.path = H.path

def EulerPacketCylinderField.CoefficientBudget.ofRawEq {P T : ℝ} {O O' : EulerPacketProfileRecursion.Operators} {G : CoefficientData P T O} (B : CoefficientBudget G) (H : CoefficientData P T O') (hi : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), O.inverseFrame (↑t, x, θ) = O'.inverseFrame (↑t, x, θ)) (hs : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), O.strain (↑t, x, θ) = O'.strain (↑t, x, θ)) (hn : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), O.normal (↑t, x, θ) = O'.normal (↑t, x, θ)) : CoefficientBudget H

Changing the solver fields of the packet operators does not change the coefficient budget when the three actual coefficients agree on the interval.

Equations

• B.ofRawEq H hi hs hn = { Rc := B.Rc, amplitude := B.amplitude, Rc_nonneg := ⋯, amplitude_nonneg := ⋯, inverse_bound := ⋯, strain_bound := ⋯, normal_bound := ⋯ }

theorem EulerPacketCylinderField.MatrixCoefficient.changeTime_translation_bound {T T' : ℝ} {raw : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (G : MatrixCoefficient T raw) (h : T = T') (n : ℕ) (a : EulerSmoothLimit.Space) (C : ℝ) (hb : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath G.path) a‖ ≤ C) : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath (G.changeTime h).path) a‖ ≤ C

theorem EulerPacketCylinderField.VectorCoefficient.changeTime_translation_bound {T T' : ℝ} {raw : EulerPacketProfileRecursion.VectorField} (G : VectorCoefficient T raw) (h : T = T') (n : ℕ) (a : EulerSmoothLimit.Space) (C : ℝ) (hb : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath G.path) a‖ ≤ C) : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath (G.changeTime h).path) a‖ ≤ C

def EulerPacketCylinderField.sourceCoefficientBudget (P : ℝ) [Fact (0 < P)] (M : EulerMeanPacketProvider.Data) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (I : EulerTransversePacketProvider.InitialData P D) (hT : M.T = D.T) (Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hI : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.FInv.field t)) x‖ ≤ C * EulerGevrey.majorant Rc 0 n) (hM : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.M.field t)) x‖ ≤ C * EulerGevrey.majorant Rc 0 n) : CoefficientBudget (sourceCoefficientData P M D I hT)

Uniform compact-time translation bounds for the literal source coefficients. Only the original inverse-frame and strain jets are inputs; in particular the normal has no independent bound and there is no loss in radius or amplitude.

Equations

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