Source-only coefficient budgets for the joined pressure, potential and corrector.

Explicit polynomial coefficient budgets for the actual transverse potential and slow curl.

def EulerTransversePacketProvider.Data.correctorCoefficientRadius (R Ri : ℝ) : ℝ

Corrector coefficient radius, given by R+4*Ri+1.

Equations

• EulerTransversePacketProvider.Data.correctorCoefficientRadius R Ri = R + 4 * Ri + 1

def EulerTransversePacketProvider.Data.correctorCoefficientAmplitude (C Ri : ℝ) : ℝ

Corrector coefficient amplitude, given by 1+C+3*C^2+3*Ri*C+27*(3*Ri*C)^2*(3*C^2).

Equations

• EulerTransversePacketProvider.Data.correctorCoefficientAmplitude C Ri = 1 + C + 3 * C ^ 2 + 3 * Ri * C + 27 * (3 * Ri * C) ^ 2 * (3 * C ^ 2)

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Data.instTransversePacketCoefficientBounds1 : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerTransversePacketProvider.Data.instTransversePacketCoefficientBounds1 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Data.instTransversePacketCoefficientBounds2 : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerTransversePacketProvider.Data.instTransversePacketCoefficientBounds2 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Data.instTransversePacketCoefficientBounds3 : NormedAddCommGroup EulerSourcePotentialCoefficient.PotentialField

Cache the standard NormedAddCommGroup PotentialField instance to shorten typeclass synthesis.

Equations

• EulerTransversePacketProvider.Data.instTransversePacketCoefficientBounds3 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Data.instTransversePacketCoefficientBounds4 : NormedSpace ℝ EulerSourcePotentialCoefficient.PotentialField

Cache the standard NormedSpace ℝ PotentialField instance to shorten typeclass synthesis.

Equations

• EulerTransversePacketProvider.Data.instTransversePacketCoefficientBounds4 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Data.instTransversePacketCoefficientBounds5 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : NormedAddCommGroup C(↑(Set.Icc 0 D.T), EulerSourcePotentialCoefficient.PotentialField)

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) D.T,PotentialField) instance to shorten typeclass synthesis.

Equations

• D.instTransversePacketCoefficientBounds5 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Data.instTransversePacketCoefficientBounds6 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : NormedSpace ℝ C(↑(Set.Icc 0 D.T), EulerSourcePotentialCoefficient.PotentialField)

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) D.T,PotentialField) instance to shorten typeclass synthesis.

Equations

• D.instTransversePacketCoefficientBounds6 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Data.instTransversePacketCoefficientBounds7 : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] ℝ)

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

Equations

• EulerTransversePacketProvider.Data.instTransversePacketCoefficientBounds7 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Data.instTransversePacketCoefficientBounds8 : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] ℝ)

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

Equations

• EulerTransversePacketProvider.Data.instTransversePacketCoefficientBounds8 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Data.instTransversePacketCoefficientBounds9 : NormedAddCommGroup EulerSourcePotentialCoefficient.NormalField

Cache the standard NormedAddCommGroup NormalField instance to shorten typeclass synthesis.

Equations

• EulerTransversePacketProvider.Data.instTransversePacketCoefficientBounds9 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Data.instTransversePacketCoefficientBounds10 : NormedSpace ℝ EulerSourcePotentialCoefficient.NormalField

Cache the standard NormedSpace ℝ NormalField instance to shorten typeclass synthesis.

Equations

• EulerTransversePacketProvider.Data.instTransversePacketCoefficientBounds10 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Data.instTransversePacketCoefficientBounds11 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : NormedAddCommGroup C(↑(Set.Icc 0 D.T), EulerSourcePotentialCoefficient.NormalField)

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) D.T,NormalField) instance to shorten typeclass synthesis.

Equations

• D.instTransversePacketCoefficientBounds11 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Data.instTransversePacketCoefficientBounds12 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : NormedSpace ℝ C(↑(Set.Icc 0 D.T), EulerSourcePotentialCoefficient.NormalField)

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) D.T,NormalField) instance to shorten typeclass synthesis.

Equations

• D.instTransversePacketCoefficientBounds12 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Data.instTransversePacketCoefficientBounds13 : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space EulerSmoothLimit.Space)

Cache the standard NormedAddCommGroup (Space →ᵇ Space) instance to shorten typeclass synthesis.

Equations

• EulerTransversePacketProvider.Data.instTransversePacketCoefficientBounds13 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Data.instTransversePacketCoefficientBounds14 : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space EulerSmoothLimit.Space)

Cache the standard NormedSpace ℝ (Space →ᵇ Space) instance to shorten typeclass synthesis.

Equations

• EulerTransversePacketProvider.Data.instTransversePacketCoefficientBounds14 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Data.instTransversePacketCoefficientBounds15 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : NormedAddCommGroup C(↑(Set.Icc 0 D.T), BoundedContinuousFunction EulerSmoothLimit.Space EulerSmoothLimit.Space)

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) D.T,Space →ᵇ Space) instance to shorten typeclass synthesis.

Equations

• D.instTransversePacketCoefficientBounds15 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Data.instTransversePacketCoefficientBounds16 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : NormedSpace ℝ C(↑(Set.Icc 0 D.T), BoundedContinuousFunction EulerSmoothLimit.Space EulerSmoothLimit.Space)

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) D.T,Space →ᵇ Space) instance to shorten typeclass synthesis.

Equations

• D.instTransversePacketCoefficientBounds16 = inferInstance

theorem EulerTransversePacketProvider.Data.corrector_coefficient_bounds {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (R C Ri : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hRi : 0 ≤ Ri) (hInv : 2 * EulerTimeLpGramGevrey.gramCost D.normalLower C 1 * (R + 1) ≤ Ri) (hI : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.FInv.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) (hM : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.M.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) : 0 ≤ correctorCoefficientRadius R Ri ∧ 0 ≤ correctorCoefficientAmplitude C Ri ∧ ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.FInv.field) a‖ ≤ correctorCoefficientAmplitude C Ri * EulerGevrey.majorant (correctorCoefficientRadius R Ri) 0 n ∧ ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.inverseDerivative) a‖ ≤ correctorCoefficientAmplitude C Ri * EulerGevrey.majorant (correctorCoefficientRadius R Ri) 0 n ∧ ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.potentialCoefficientPath) a‖ ≤ correctorCoefficientAmplitude C Ri * EulerGevrey.majorant (correctorCoefficientRadius R Ri) 0 n ∧ ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.potentialDerivative) a‖ ≤ correctorCoefficientAmplitude C Ri * EulerGevrey.majorant (correctorCoefficientRadius R Ri) 0 n

All four coefficients used in C and C_t follow from the original F⁻¹ and M bounds.

structure EulerTransversePacketJoin.NormalBudget {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (q : ℕ) (R : ℝ) : Type

Original inverse-deformation and strain jets, with one fixed inverse radius.

• Rc : ℝ

  Rc of NormalBudget, of type ℝ.

• C : ℝ

  Bound coefficient of NormalBudget, of type ℝ.

• Ri : ℝ

  Ri of NormalBudget, of type ℝ.

• Rc_nonneg : 0 ≤ self.Rc
• C_nonneg : 0 ≤ self.C
• inverse_radius : 2 * EulerTimeLpGramGevrey.gramCost D.normalLower self.C 1 * (self.Rc + 1) ≤ self.Ri
• inverse_bound (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (⇑(D.FInv.field t)) x‖ ≤ self.C * EulerGevrey.majorant self.Rc 0 n
• strain_bound (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (⇑(D.M.field t)) x‖ ≤ self.C * EulerGevrey.majorant self.Rc 0 n
• radius : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) (EulerTransversePacketProvider.Data.correctorCoefficientRadius self.Rc self.Ri) ≤ R

theorem EulerTransversePacketJoin.NormalBudget.Ri_nonneg {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {q : ℕ} {R : ℝ} (N : NormalBudget D q R) : 0 ≤ N.Ri

def EulerTransversePacketJoin.NormalBudget.coefficientRadius {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {q : ℕ} {R : ℝ} (N : NormalBudget D q R) : ℝ

Coefficient radius, given by correctorCoefficientRadius N.Rc N.Ri.

Equations

• N.coefficientRadius = EulerTransversePacketProvider.Data.correctorCoefficientRadius N.Rc N.Ri

def EulerTransversePacketJoin.NormalBudget.coefficientAmplitude {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {q : ℕ} {R : ℝ} (N : NormalBudget D q R) : ℝ

Coefficient amplitude, given by correctorCoefficientAmplitude N.C N.Ri.

Equations

• N.coefficientAmplitude = EulerTransversePacketProvider.Data.correctorCoefficientAmplitude N.C N.Ri

def EulerTransversePacketJoin.NormalBudget.blockAmplitude {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {q : ℕ} {R : ℝ} (N : NormalBudget D q R) : ℝ

Block amplitude, given by sobolevCoefficientAmplitude (Fin 4) q N.coefficientRadius N.coefficientAmplitude.

Equations

• N.blockAmplitude = EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) q N.coefficientRadius N.coefficientAmplitude

theorem EulerTransversePacketJoin.NormalBudget.coefficient_bounds {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {q : ℕ} {R : ℝ} (N : NormalBudget D q R) : 0 ≤ N.coefficientRadius ∧ 0 ≤ N.coefficientAmplitude ∧ ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.FInv.field) a‖ ≤ N.coefficientAmplitude * EulerGevrey.majorant N.coefficientRadius 0 n ∧ ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.inverseDerivative) a‖ ≤ N.coefficientAmplitude * EulerGevrey.majorant N.coefficientRadius 0 n ∧ ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.potentialCoefficientPath) a‖ ≤ N.coefficientAmplitude * EulerGevrey.majorant N.coefficientRadius 0 n ∧ ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.potentialDerivative) a‖ ≤ N.coefficientAmplitude * EulerGevrey.majorant N.coefficientRadius 0 n

theorem EulerTransversePacketJoin.NormalBudget.blockAmplitude_nonneg {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {q : ℕ} {R : ℝ} (N : NormalBudget D q R) : 0 ≤ N.blockAmplitude

theorem EulerTransversePacketJoin.NormalBudget.normal_bound {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {q : ℕ} {R : ℝ} (N : NormalBudget D q R) (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (⇑(D.normal.field t)) x‖ ≤ N.C * EulerGevrey.majorant N.Rc 0 n

theorem EulerTransversePacketJoin.NormalBudget.pressure_radius {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {q : ℕ} {R : ℝ} (N : NormalBudget D q R) : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) (4 * N.Ri) ≤ R

theorem EulerTransversePacketJoin.Budget.velocityCost_nonneg {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τ ⋯)} {ι : Type u_2} [Fintype ι] {q : ℕ} (L : Budget D τ hτ hτT B ι q) : 0 ≤ L.velocityCost

theorem EulerTransversePacketJoin.Budget.derivativeCost_nonneg {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τ ⋯)} {ι : Type u_2} [Fintype ι] {q : ℕ} (L : Budget D τ hτ hτT B ι q) : 0 ≤ L.derivativeCost

noncomputable def EulerTransversePacketJoin.Budget.commonCost {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τ ⋯)} {ι : Type u_2} [Fintype ι] {q : ℕ} (L : Budget D τ hτ hτT B ι q) : ℝ

Common cost, given by L.velocityCost+L.derivativeCost.

Equations

• L.commonCost = L.velocityCost + L.derivativeCost

theorem EulerTransversePacketJoin.Budget.commonCost_nonneg {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τ ⋯)} {ι : Type u_2} [Fintype ι] {q : ℕ} (L : Budget D τ hτ hτT B ι q) : 0 ≤ L.commonCost

theorem EulerTransversePacketJoin.Budget.velocityCost_le_common {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τ ⋯)} {ι : Type u_2} [Fintype ι] {q : ℕ} (L : Budget D τ hτ hτT B ι q) : L.velocityCost ≤ L.commonCost

theorem EulerTransversePacketJoin.Budget.derivativeCost_le_common {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τ ⋯)} {ι : Type u_2} [Fintype ι] {q : ℕ} (L : Budget D τ hτ hτT B ι q) : L.derivativeCost ≤ L.commonCost