Source-budget constructors using the literal parent fields in (21) and the physical tangent growth estimate. H3 for the constructed coordinate propagator, the Hessian jets, and every inverse radius guard are conclusions. The curvature/smallness hypotheses remain in the genuine source data.

Construct the joined transverse budget from the parent deformation, its two actual time derivatives, and the source weighted propagator. Every radius guard is discharged by the fixed polynomial source envelopes; the construction is independent of forcing amplitude and recursive grade.

The Hessian multiplier bound follows from the actual second time derivative of the deformation and the Jacobi equation. Uniqueness of within-interval derivatives includes both endpoints of the interval.

theorem EulerTransversePacketProvider.HistoryData.second_eq_jacobi {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : Data U} (B : HistoryData D) (F₂ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 D.T)) EulerPacketCofactor.EndSpace) (h₂ : ∀ 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 ⋯ F₂.field t) x) (Set.Icc 0 D.T) t) (t : ↑(Set.Icc 0 D.T)) (x v : EulerSmoothLimit.Space) : ((F₂.field t) x) v = -((B.H.field t) x) (((D.F.field t) x) v)

theorem EulerTransversePacketProvider.HistoryData.curvature_bound_of_second {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : Data U} (B : HistoryData D) (F₂ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 D.T)) EulerPacketCofactor.EndSpace) (h₂ : ∀ 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 ⋯ F₂.field t) x) (Set.Icc 0 D.T) t) (R C C₂ : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hC₂ : 0 ≤ C₂) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) (hF₂ : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(F₂.field t)) x‖ ≤ C₂ * EulerGevrey.majorant R 0 n) (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (⇑(B.H.field t)) x‖ ≤ 27 * C ^ 2 * C₂ * EulerGevrey.majorant R 0 n

@[instance_reducible]

noncomputable def EulerPacketParentJoinedBudget.instPacketParentJoinedBudget1 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedRing (U →L[ℝ] U)

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

Equations

• EulerPacketParentJoinedBudget.instPacketParentJoinedBudget1 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketParentJoinedBudget.instPacketParentJoinedBudget2 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedRing (BoundedContinuousFunction EulerSmoothLimit.Space (U →L[ℝ] U))

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

Equations

• EulerPacketParentJoinedBudget.instPacketParentJoinedBudget2 = inferInstance

def EulerPacketParentJoinedBudget.sourceJoinedBudget {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (q : ℕ) (Ti R C C₁ C₂ Cp : ℝ) (hτ1 : τ ≤ 1) (hTi : τ⁻¹ ≤ Ti) (hR : 0 ≤ R) (hC : 0 ≤ C) (hC₁ : 0 ≤ C₁) (hC₂ : 0 ≤ C₂) (hCp : 0 ≤ Cp) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) (hF₁ : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F₁.field t)) x‖ ≤ C₁ * EulerGevrey.majorant R 0 n) (F₂ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 τ)) EulerPacketCofactor.EndSpace) (h₂ : ∀ t ∈ Set.Icc 0 τ, ∀ (x : EulerSmoothLimit.Space), HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath τ ⋯ (D.initial τ hτ ⋯).F₁.field s) x) ((EulerVolterraConvolution.extendPath τ ⋯ F₂.field t) x) (Set.Icc 0 τ) t) (hF₂ : ∀ (n : ℕ) (t : ↑(Set.Icc 0 τ)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(F₂.field t)) x‖ ≤ C₂ * EulerGevrey.majorant R 0 n) (g : C(↑(Set.Icc 0 (D.T - τ)), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 (D.T - τ))), 0 < g t) (hg0 : g ⟨0, ⋯⟩ = 1) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (hΩo : IsOpen Ω) (hsub : D.support ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) (hprop : ∀ (t s : ↑(Set.Icc 0 (D.T - τ))), s ≤ t → ∀ (x : EulerSmoothLimit.Space), ‖x‖ ≤ 1 / 2 → ‖((EulerLinearFundamentalExistence.fundamentalPath (D.T - τ) ⋯ (EulerSourceForwardCoefficient.sourceGenerator (D.tail τ ⋯ hτT).frame (D.tail τ ⋯ hτT).frameDerivative (D.tail τ ⋯ hτT).frameLower ⋯ ⋯)).forward t) x ∘SL ((EulerLinearFundamentalExistence.fundamentalPath (D.T - τ) ⋯ (EulerSourceForwardCoefficient.sourceGenerator (D.tail τ ⋯ hτT).frame (D.tail τ ⋯ hτT).frameDerivative (D.tail τ ⋯ hτT).frameLower ⋯ ⋯)).backward s) x‖ ≤ Cp * g t / g s) : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) q

Source joined budget as an element of Budget D τ hτ hτT B (Fin 4) q.

Equations

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

def EulerPacketParentPhysicalBudgets.halfBall : Set EulerSmoothLimit.Space

Half ball, given by {x | ‖x‖ ≤ (1/2 : ℝ)}.

Equations

• EulerPacketParentPhysicalBudgets.halfBall = {x : EulerSmoothLimit.Space | ‖x‖ ≤ 1 / 2}

noncomputable def EulerPacketParentPhysicalBudgets.physicalCost (K Cp : ℝ) : ℝ

Physical cost, given by 3*(frameAmplitude K)^3*Cp.

Equations

• EulerPacketParentPhysicalBudgets.physicalCost K Cp = 3 * EulerPacketParentLabelBounds.frameAmplitude K ^ 3 * Cp

theorem EulerPacketParentPhysicalBudgets.physicalCost_nonneg (K Cp : ℝ) (hCp : 0 ≤ Cp) : 0 ≤ physicalCost K Cp

noncomputable def EulerPacketParentPhysicalBudgets.forwardBudget {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (q : ℕ) (A V : ↑(Set.Icc 0 D.T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (ℓ K Cp : ℝ) (hℓ : 0 ≤ ℓ) (hℓ1 : ℓ ≤ 1) (hK : 0 ≤ K) (hCp : 0 ≤ Cp) (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) (g : C(↑(Set.Icc 0 D.T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 D.T)), 0 < g t) (hg0 : g ⟨0, ⋯⟩ = 1) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (hΩo : IsOpen Ω) (hsub : D.support ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) (hphysical : EulerPacketSourcePropagator.PhysicalGrowth D halfBall (⇑g) Cp) : EulerTransversePacketForward.Budget D (Fin 4) q

At a zero-history stage the real label bounds and physical propagator construct the complete source forward budget, before any forcing is chosen.

Equations

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

noncomputable def EulerPacketParentPhysicalBudgets.joinedBudget {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < D.T) (B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)) (q : ℕ) (A V : ↑(Set.Icc 0 D.T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (W : ↑(Set.Icc 0 τ) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (F₂ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 τ)) EulerPacketCofactor.EndSpace) (ℓ K Ti Cp : ℝ) (hℓ : 0 ≤ ℓ) (hℓ1 : ℓ ≤ 1) (hK : 0 ≤ K) (hτ1 : τ ≤ 1) (hTi : τ⁻¹ ≤ Ti) (hCp : 0 ≤ Cp) (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 τ)), 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 (ℓ • x)) (hF₁ : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F₁.field t) x = fderiv ℝ (V t).field (ℓ • x)) (hF₂ : ∀ (t : ↑(Set.Icc 0 τ)) (x : EulerSmoothLimit.Space), (F₂.field t) x = fderiv ℝ (W t).field (ℓ • x)) (h₂ : ∀ t ∈ Set.Icc 0 τ, ∀ (x : EulerSmoothLimit.Space), HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath τ ⋯ (D.initial τ hτ ⋯).F₁.field s) x) ((EulerVolterraConvolution.extendPath τ ⋯ F₂.field t) x) (Set.Icc 0 τ) t) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (g : C(↑(Set.Icc 0 (D.T - τ)), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 (D.T - τ))), 0 < g t) (hg0 : g ⟨0, ⋯⟩ = 1) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (hΩo : IsOpen Ω) (hsub : D.support ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) (hphysical : EulerPacketSourcePropagator.PhysicalGrowth (D.tail τ ⋯ hτT) halfBall (⇑g) Cp) : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) q

Positive history uses the actual acceleration in (21) and its true within-time derivative identity. Jacobi and determinant one then supply the Hessian multiplier bound needed by the joined variational inverse.

Equations

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