Norm-one coefficient constructions used by the actual slow and fast packet terms.

theorem EulerPacketCylinderField.normalComponentMap_norm : ‖normalComponentMap‖ ≤ 1

noncomputable def EulerPacketCylinderField.VectorCoefficient.normalMatrix {T : ℝ} {raw : EulerPacketProfileRecursion.VectorField} (N : VectorCoefficient T raw) : MatrixCoefficient T fun (z : EulerPacketPointJets.Domain) => normalComponentMap (raw z)

Normal matrix, bundling path, orbit, raw_eq.

Equations

• N.normalMatrix = { path := EulerPacketCylinderField.normalComponentPath N.path, orbit := ⋯, raw_eq := ⋯ }

theorem EulerPacketCylinderField.VectorCoefficient.normalMatrix_bound {T : ℝ} {raw : EulerPacketProfileRecursion.VectorField} (N : VectorCoefficient T raw) (Rc C : ℝ) (hN : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath N.path) a‖ ≤ C * EulerGevrey.majorant Rc 0 n) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath N.normalMatrix.path) a‖ ≤ C * EulerGevrey.majorant Rc 0 n

theorem EulerPacketCylinderField.MatrixCoefficient.adjoint_bound {T : ℝ} {raw : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (K : MatrixCoefficient T raw) (Rc C : ℝ) (hK : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath K.path) a‖ ≤ C * EulerGevrey.majorant Rc 0 n) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath K.adjoint.path) a‖ ≤ C * EulerGevrey.majorant Rc 0 n