The zero-history forward budget has an explicit polynomial source radius. Cofactor bounds discharge the Gram inverse cost. The sole growth estimate supplied here is the genuine weighted homogeneous propagator H3.

def EulerPacketParentForwardBudget.radius (q : ℕ) (T R C C₁ Cp : ℝ) : ℝ

Radius as an element of ℝ.

Equations

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

theorem EulerPacketParentForwardBudget.radius_guards (q : ℕ) (T R C C₁ Cp : ℝ) (hT : 0 ≤ T) (hR : 0 ≤ R) (hC : 0 ≤ C) (hC₁ : 0 ≤ C₁) (hCp : 0 ≤ Cp) : 1 ≤ radius q T R C C₁ Cp ∧ EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) R ≤ radius q T R C C₁ Cp ∧ EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) (4 * EulerPacketParentTransverseCosts.inverseRadius R C) ≤ radius q T R C C₁ Cp ∧ 2 * EulerPacketParentTransverseCosts.forwardCost q T 0 R C C₁ Cp * (EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) (4 * EulerPacketParentTransverseCosts.inverseRadius R C) + 1) ≤ radius q T R C C₁ Cp

@[instance_reducible]

noncomputable def EulerPacketParentForwardBudget.instPacketParentForwardBudget1 {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

• EulerPacketParentForwardBudget.instPacketParentForwardBudget1 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketParentForwardBudget.instPacketParentForwardBudget2 {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

• EulerPacketParentForwardBudget.instPacketParentForwardBudget2 = inferInstance

def EulerPacketParentForwardBudget.sourceForwardBudget {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (q : ℕ) (R C C₁ Cp : ℝ) (hR : 0 ≤ R) (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) (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.frame D.frameDerivative D.frameLower ⋯ ⋯)).forward t) x ∘SL ((EulerLinearFundamentalExistence.fundamentalPath D.T ⋯ (EulerSourceForwardCoefficient.sourceGenerator D.frame D.frameDerivative D.frameLower ⋯ ⋯)).backward s) x‖ ≤ Cp * g t / g s) : EulerTransversePacketForward.Budget D (Fin 4) q

Source forward budget as an element of EulerTransversePacketForward.Budget D (Fin 4) q.

Equations

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