Bounds for the actual composition, scalar multiple and spatial derivative of packet matrix-coefficient witnesses. The derivative radius enlargement occurs only in this fixed coefficient budget.

@[instance_reducible]

noncomputable def EulerPacketCylinderField.MatrixCoefficient.instPacketMatrixCoefficientGevrey1 : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerPacketCylinderField.MatrixCoefficient.instPacketMatrixCoefficientGevrey1 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCylinderField.MatrixCoefficient.instPacketMatrixCoefficientGevrey2 : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerPacketCylinderField.MatrixCoefficient.instPacketMatrixCoefficientGevrey2 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCylinderField.MatrixCoefficient.instPacketMatrixCoefficientGevrey3 : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerPacketCylinderField.MatrixCoefficient.instPacketMatrixCoefficientGevrey3 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCylinderField.MatrixCoefficient.instPacketMatrixCoefficientGevrey4 : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerPacketCylinderField.MatrixCoefficient.instPacketMatrixCoefficientGevrey4 = inferInstance

theorem EulerPacketCylinderField.MatrixCoefficient.comp_bound {T : ℝ} {a b : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (A : MatrixCoefficient T a) (B : MatrixCoefficient T b) (R C D : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hD : 0 ≤ D) (hbA : ∀ (n : ℕ) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath A.path) x‖ ≤ C * EulerGevrey.majorant R 0 n) (hbB : ∀ (n : ℕ) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath B.path) x‖ ≤ D * EulerGevrey.majorant R 0 n) (n : ℕ) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath (A.comp B).path) x‖ ≤ 3 * C * D * EulerGevrey.majorant R 0 n

theorem EulerPacketCylinderField.MatrixCoefficient.smul_bound {T : ℝ} {a : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (A : MatrixCoefficient T a) (c R C : ℝ) (hb : ∀ (n : ℕ) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath A.path) x‖ ≤ C * EulerGevrey.majorant R 0 n) (n : ℕ) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath (A.smul c).path) x‖ ≤ |c| * C * EulerGevrey.majorant R 0 n

theorem EulerPacketCylinderField.MatrixCoefficient.spatialDerivative_norm_le {T : ℝ} {a : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (A : MatrixCoefficient T a) (v : EulerSmoothLimit.Space) (n : ℕ) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath (A.spatialDerivative v).path) x‖ ≤ ‖v‖ * ‖iteratedFDeriv ℝ (n + 1) (EulerMeanCoefficients.translateCoefficientPath A.path) x‖

theorem EulerPacketCylinderField.MatrixCoefficient.spatialDerivative_bound {T : ℝ} {a : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (A : MatrixCoefficient T a) (v : EulerSmoothLimit.Space) (hv : ‖v‖ ≤ 1) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hb : ∀ (n : ℕ) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath A.path) x‖ ≤ C * EulerGevrey.majorant R 0 n) (n : ℕ) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath (A.spatialDerivative v).path) x‖ ≤ C * R * EulerGevrey.majorant (4 * R) 0 n

theorem EulerPacketCylinderField.MatrixCoefficient.bound_mono_radius {T : ℝ} {a : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (A : MatrixCoefficient T a) (R S C : ℝ) (hR : 0 ≤ R) (hRS : R ≤ S) (hC : 0 ≤ C) (hb : ∀ (n : ℕ) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath A.path) x‖ ≤ C * EulerGevrey.majorant R 0 n) (n : ℕ) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath A.path) x‖ ≤ C * EulerGevrey.majorant S 0 n