The exact nonlinear energy constant is a fixed source quantity, independent of the Sobolev order, truncation and oscillation frequency.
noncomputable def
EulerPacketCorrectionCoefficients.growthCoefficient
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(D : EulerTransversePacketProvider.Data U)
(P : ℝ)
[Fact (0 < P)]
(Kc : CorrectionCoefficientBudget D P)
(B0 B1 : ℝ)
:
Growth coefficient as an element of ℝ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketCorrectionCoefficients.growthCoefficient_eq
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(D : EulerTransversePacketProvider.Data U)
(P : ℝ)
[Fact (0 < P)]
(Kc : CorrectionCoefficientBudget D P)
(B0 B1 κ : ℝ)
(hκ : |κ| ≤ 1)
(Z G : EulerAllOrderCorrectionData.FieldTower P D.T)
(q : ℕ)
:
growthCoefficient D P Kc B0 B1 = EulerNonlinearEnergyConstants.energyConstant P
(EulerCorrectionEnergyData.MetricBudget.growth0 P (sourceMetricBudget D P κ hκ Z G q) B0)
(EulerCorrectionEnergyData.MetricBudget.growth1 P (sourceMetricBudget D P κ hκ Z G q))
(EulerCorrectionEnergyData.MetricBudget.multiplier P (sourceMetricBudget D P κ hκ Z G q)) Kc.B Kc.M B0 B1 Kc.A0
Kc.A2 (sourceMetricBudget D P κ hκ Z G q).c
theorem
EulerPacketCorrectionCoefficients.growthCoefficient_pos
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(D : EulerTransversePacketProvider.Data U)
(P : ℝ)
[Fact (0 < P)]
(Kc : CorrectionCoefficientBudget D P)
(B0 B1 : ℝ)
(hB0 : 0 ≤ B0)
(hB1 : 0 ≤ B1)
: