The polynomial primitive envelope applies to the constructed correction coefficients, using only the original deformation and inverse-deformation jets.

Quantitative bounds for the actual inverse metric and its first spatial and time derivatives, from the prescribed deformation jets.

theorem EulerPacketCorrectionCoefficients.inverseMetricCoefficient_bound {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (R C0 : ℝ) (hR : 0 ≤ R) (hC0 : 0 ≤ C0) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C0 * EulerGevrey.majorant R 0 n) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath (inverseMetricCoefficient D).path) a‖ ≤ 3 * C0 * C0 * EulerGevrey.majorant R 0 n

theorem EulerPacketCorrectionCoefficients.inverseMetricFirstBound_le_source {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (R C0 : ℝ) (hR : 0 ≤ R) (hC0 : 0 ≤ C0) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C0 * EulerGevrey.majorant R 0 n) : inverseMetricFirstBound D ≤ 3 * C0 * C0 * R

theorem EulerPacketCorrectionCoefficients.framePath_norm_le_source {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (R C0 : ℝ) (hC0 : 0 ≤ C0) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C0 * EulerGevrey.majorant R 0 n) : ‖D.F.field‖ ≤ C0

theorem EulerPacketCorrectionCoefficients.frameTimePath_norm_le_source {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (R C1 : ℝ) (hC1 : 0 ≤ C1) (hF1 : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F₁.field t)) x‖ ≤ C1 * EulerGevrey.majorant R 0 n) : ‖D.F₁.field‖ ≤ C1

theorem EulerPacketCorrectionCoefficients.inverseMetricBound_le_source {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (R C0 : ℝ) (hC0 : 0 ≤ C0) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C0 * EulerGevrey.majorant R 0 n) : inverseMetricBound D ≤ C0 ^ 2

theorem EulerPacketCorrectionCoefficients.inverseMetricTimeBound_le_source {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (R C0 C1 : ℝ) (hC0 : 0 ≤ C0) (hC1 : 0 ≤ C1) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C0 * EulerGevrey.majorant R 0 n) (hF1 : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F₁.field t)) x‖ ≤ C1 * EulerGevrey.majorant R 0 n) : inverseMetricTimeBound D ≤ 2 * C0 * C1

theorem EulerPacketCorrectionCoefficients.sourceMetricBudget_first_le_source {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (R C0 : ℝ) (hR : 0 ≤ R) (hC0 : 0 ≤ C0) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C0 * EulerGevrey.majorant R 0 n) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (hκ : |κ| ≤ 1) (Z G : EulerAllOrderCorrectionData.FieldTower P D.T) (q : ℕ) : (sourceMetricBudget D P κ hκ Z G q).first ≤ 3 * C0 * C0 * R

theorem EulerPacketCorrectionPrimitive.correction_envelopes (c R C0 C1 CI X : ℝ) (hc : 0 < c) (hR : 0 ≤ R) (hC0 : 0 ≤ C0) (hC1 : 0 ≤ C1) (hCI : 0 ≤ CI) (hRX : R ≤ X) (hC0X : C0 ≤ X) (hC1X : C1 ≤ X) (hCIX : CI ≤ X) (hci : c⁻¹ ≤ (1 + X) ^ 2) : EulerPacketCorrectionCoefficients.correctionCoefficientRadius R CI ≤ radiusEnvelope X ∧ EulerPacketCorrectionCoefficients.correctionPressureEnvelope c R CI ≤ pressureEnvelope X ∧ EulerPacketCorrectionCoefficients.correctionMetricEnvelope R CI ≤ metricEnvelope X ∧ EulerPacketCorrectionCoefficients.correctionLinearEnvelope R C1 CI ≤ linearEnvelope X ∧ EulerPacketCorrectionCoefficients.correctionQuadraticEnvelope R C0 CI ≤ quadraticEnvelope X

structure EulerPacketCorrectionPrimitive.CorrectionBounds {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (Kc : EulerPacketCorrectionCoefficients.CorrectionCoefficientBudget D P) (X : ℝ) : Prop

Correction bounds data, collecting inverse, metric, first, time, radius, pressure and their compatibility conditions.

• inverse : D.inverseBound ≤ X
• metric : EulerPacketCorrectionCoefficients.inverseMetricBound D ≤ X
• first : EulerPacketCorrectionCoefficients.inverseMetricFirstBound D ≤ X
• time : EulerPacketCorrectionCoefficients.inverseMetricTimeBound D ≤ X
• radius : Kc.Rc ≤ X
• pressure : Kc.M ≤ X
• base : Kc.B ≤ X
• linear : Kc.A0 ≤ X
• quadratic : Kc.A2 ≤ X

theorem EulerPacketCorrectionPrimitive.CorrectionBounds.mono {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] {Kc : EulerPacketCorrectionCoefficients.CorrectionCoefficientBudget D P} {X Y : ℝ} (h : CorrectionBounds D P Kc X) (hXY : X ≤ Y) : CorrectionBounds D P Kc Y

theorem EulerPacketCorrectionPrimitive.correctionBudget_bounds {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (R C0 C1 CI : ℝ) (hR : 0 ≤ R) (hC0 : 0 ≤ C0) (hC1 : 0 ≤ C1) (hCI : 0 ≤ CI) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C0 * EulerGevrey.majorant R 0 n) (hF1 : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F₁.field t)) x‖ ≤ C1 * EulerGevrey.majorant R 0 n) (hFI : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.FInv.field t)) x‖ ≤ CI * EulerGevrey.majorant R 0 n) (X : ℝ) (hX : 1 ≤ X) (hRX : R ≤ X) (hC0X : C0 ≤ X) (hC1X : C1 ≤ X) (hCIX : CI ≤ X) : CorrectionBounds D P (EulerPacketCorrectionCoefficients.correctionCoefficientBudget D P R C0 C1 CI hR hC0 hC1 hCI hF hF1 hFI) (primitiveEnvelope P X)

theorem EulerPacketCylinderField.CoefficientBudget.primitive_bound {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (B : CoefficientBudget C) (X : ℝ) (hX : 0 ≤ X) (hR : B.Rc ≤ X) (hC : B.amplitude ≤ X) : B.multiplierCost ≤ EulerPacketCorrectionPrimitive.primitiveEnvelope P X ∧ B.termCost ≤ EulerPacketCorrectionPrimitive.primitiveEnvelope P X