Source bounds for the actual pressure metric, linear coefficient and three quadratic coefficients. Their common coefficient radius and amplitudes are independent of the correction order, cutoff and frequency.

theorem EulerPacketCorrectionCoefficients.frameCoefficient_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 (frameCoefficient D).path) a‖ ≤ C0 * EulerGevrey.majorant R 0 n

theorem EulerPacketCorrectionCoefficients.frameTimeCoefficient_bound {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (R C1 : ℝ) (hR : 0 ≤ R) (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) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath (frameTimeCoefficient D).path) a‖ ≤ C1 * EulerGevrey.majorant R 0 n

theorem EulerPacketCorrectionCoefficients.inverseCoefficient_bound {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (R CI : ℝ) (hR : 0 ≤ R) (hCI : 0 ≤ CI) (hFI : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.FInv.field t)) x‖ ≤ CI * EulerGevrey.majorant R 0 n) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath (inverseCoefficient D).path) a‖ ≤ CI * EulerGevrey.majorant R 0 n

theorem EulerPacketCorrectionCoefficients.metricCoefficient_bound {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (R CI : ℝ) (hR : 0 ≤ R) (hCI : 0 ≤ CI) (hFI : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.FInv.field t)) x‖ ≤ CI * EulerGevrey.majorant R 0 n) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath (metricCoefficient D).path) a‖ ≤ 3 * CI * CI * EulerGevrey.majorant (4 * R) 0 n

theorem EulerPacketCorrectionCoefficients.linearCoefficient_bound {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (R C1 CI : ℝ) (hR : 0 ≤ R) (hC1 : 0 ≤ C1) (hCI : 0 ≤ CI) (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) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath (linearCoefficient D).path) a‖ ≤ 6 * CI * C1 * EulerGevrey.majorant (4 * R) 0 n

theorem EulerPacketCorrectionCoefficients.quadraticCoefficient_bound {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (R C0 CI : ℝ) (hR : 0 ≤ R) (hC0 : 0 ≤ C0) (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) (hFI : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.FInv.field t)) x‖ ≤ CI * EulerGevrey.majorant R 0 n) (κ : ℝ) (hκ : |κ| ≤ 1) (i : Fin 3) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath (quadraticCoefficient D κ i).path) a‖ ≤ 3 * CI * (C0 * R) * EulerGevrey.majorant (4 * R) 0 n