Concrete source budgets from (21), stated in the actual classical physical-label H⁶ word norms of the displacement, velocity and acceleration. No multiplier bound or inverse-solver estimate is an input.

def EulerPacketParentLabelBounds.HasLabelBound (K : ℝ) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) : Prop

The individual component of the literal three-field bound in (21).

Equations

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

theorem EulerPacketParentLabelBounds.coefficient_gradient_bound {J : Type u_1} [TopologicalSpace J] [CompactSpace J] (F : EulerMeanCoefficients.SmoothCoefficientPath J EulerPacketCofactor.EndSpace) (A : J → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hL : ‖L‖ ≤ 1) (heq : ∀ (t : J) (x : EulerSmoothLimit.Space), (F.field t) x = fderiv ℝ (A t).field (L x)) (K : ℝ) (hK : 0 ≤ K) (hb : ∀ (t : J), HasLabelBound K (A t)) (n : ℕ) (t : J) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (⇑(F.field t)) x‖ ≤ gradientAmplitude K * EulerGevrey.majorant (coefficientRadius K) 0 n

theorem EulerPacketParentLabelBounds.coefficient_deformation_bound {J : Type u_1} [TopologicalSpace J] [CompactSpace J] (F : EulerMeanCoefficients.SmoothCoefficientPath J EulerPacketCofactor.EndSpace) (A : J → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hL : ‖L‖ ≤ 1) (heq : ∀ (t : J) (x : EulerSmoothLimit.Space), (F.field t) x = ContinuousLinearMap.id ℝ EulerSmoothLimit.Space + fderiv ℝ (A t).field (L x)) (K : ℝ) (hK : 0 ≤ K) (hb : ∀ (t : J), HasLabelBound K (A t)) (n : ℕ) (t : J) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (⇑(F.field t)) x‖ ≤ frameAmplitude K * EulerGevrey.majorant (coefficientRadius K) 0 n

noncomputable def EulerPacketParentLabelBudgets.normalBudget {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (q : ℕ) (A V : ↑(Set.Icc 0 D.T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (ℓ K : ℝ) (hℓ : 0 ≤ ℓ) (hℓ1 : ℓ ≤ 1) (hK : 0 ≤ K) (hA : ∀ (t : ↑(Set.Icc 0 D.T)), EulerPacketParentLabelBounds.HasLabelBound K (A t)) (hV : ∀ (t : ↑(Set.Icc 0 D.T)), EulerPacketParentLabelBounds.HasLabelBound K (V t)) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F.field t) x = ContinuousLinearMap.id ℝ EulerSmoothLimit.Space + fderiv ℝ (A t).field (ℓ • x)) (hF₁ : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F₁.field t) x = fderiv ℝ (V t).field (ℓ • x)) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) : EulerTransversePacketJoin.NormalBudget D q (EulerPacketParentNormalBudget.radius (EulerPacketParentLabelBounds.coefficientRadius K) (EulerPacketParentLabelBounds.frameAmplitude K) (EulerPacketParentLabelBounds.gradientAmplitude K))

The full normal/pressure/corrector multiplier budget follows from the actual parent displacement and velocity in physical initial labels.

Equations

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

noncomputable def EulerPacketParentLabelBudgets.meanBudget (D : EulerMeanPacketProvider.Data) (q : ℕ) (A V W : ↑(Set.Icc 0 D.T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (Ti K : ℝ) (hT : D.T ≤ 1) (hTi : D.T⁻¹ ≤ Ti) (hK : 0 ≤ K) (hA : ∀ (t : ↑(Set.Icc 0 D.T)), EulerPacketParentLabelBounds.HasLabelBound K (A t)) (hV : ∀ (t : ↑(Set.Icc 0 D.T)), EulerPacketParentLabelBounds.HasLabelBound K (V t)) (hW : ∀ (t : ↑(Set.Icc 0 D.T)), EulerPacketParentLabelBounds.HasLabelBound K (W t)) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F.field t) x = ContinuousLinearMap.id ℝ EulerSmoothLimit.Space + fderiv ℝ (A t).field (D.ℓ • x)) (hF₁ : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F₁.field t) x = fderiv ℝ (V t).field (D.ℓ • x)) (hF₂ : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F₂.field t) x = fderiv ℝ (W t).field (D.ℓ • x)) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) : EulerMeanPacketProvider.Budget D q (EulerPacketParentMeanBudget.radius q D.T Ti (EulerPacketParentLabelBounds.coefficientRadius K) (EulerPacketParentLabelBounds.frameAmplitude K) (EulerPacketParentLabelBounds.gradientAmplitude K) (EulerPacketParentLabelBounds.gradientAmplitude K) D.L)

The actual mean variational inverse budget is constructed from the three literal parent fields in (21), det F=1, and the inverse time length.

Equations

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