Linear operations and spatial derivatives of actual profile-normalized packet fields.

theorem EulerPacketCylinderField.Field.WordBound.of_path_eq {P T : ℝ} [Fact (0 < P)] {raw raw' : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q d : ℕ} {R A : ℝ} (hG : G.WordBound q R A d) (H : Field P T raw') (he : H.path = G.path) : H.WordBound q R A d

theorem EulerPacketCylinderField.Field.normalized_add_path {P T : ℝ} [Fact (0 < P)] {raw raw' : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (H : Field P T raw') (hT : 0 ≤ T) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) : ((G.add H).normalized hT g hg).path = ((G.normalized hT g hg).add (H.normalized hT g hg)).path

theorem EulerPacketCylinderField.Field.normalized_sub_path {P T : ℝ} [Fact (0 < P)] {raw raw' : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (H : Field P T raw') (hT : 0 ≤ T) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) : ((G.sub H).normalized hT g hg).path = ((G.normalized hT g hg).sub (H.normalized hT g hg)).path

theorem EulerPacketCylinderField.Field.normalized_neg_path {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (hT : 0 ≤ T) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) : (G.neg.normalized hT g hg).path = (G.normalized hT g hg).neg.path

theorem EulerPacketCylinderField.Field.normalized_multiply_path {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (hT : 0 ≤ T) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) {coef : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (K : MatrixCoefficient T coef) : ((K.multiply G).normalized hT g hg).path = (K.multiply (G.normalized hT g hg)).path

theorem EulerPacketCylinderField.Field.normalized_finsetSum_path {P T : ℝ} [Fact (0 < P)] (hT : 0 ≤ T) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) {ι : Type u_1} (s : Finset ι) (f : ι → EulerPacketProfileRecursion.VectorField) (W : (i : ι) → Field P T (f i)) : ((finsetSum s f W).normalized hT g hg).path = (finsetSum s (fun (i : ι) (z : EulerPacketPointJets.Domain) => (g (Set.projIcc 0 T hT z.1))⁻¹ • f i z) fun (i : ι) => (W i).normalized hT g hg).path

theorem EulerPacketCylinderField.Field.WordBound.normalized_add {P T : ℝ} [Fact (0 < P)] {raw raw' : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {H : Field P T raw'} (hT : 0 ≤ T) {g : C(↑(Set.Icc 0 T), ℝ)} {hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t} {q d : ℕ} {R A B : ℝ} (hG : (G.normalized hT g hg).WordBound q R A d) (hH : (H.normalized hT g hg).WordBound q R B d) : ((G.add H).normalized hT g hg).WordBound q R (A + B) d

theorem EulerPacketCylinderField.Field.WordBound.normalized_sub {P T : ℝ} [Fact (0 < P)] {raw raw' : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {H : Field P T raw'} (hT : 0 ≤ T) {g : C(↑(Set.Icc 0 T), ℝ)} {hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t} {q d : ℕ} {R A B : ℝ} (hG : (G.normalized hT g hg).WordBound q R A d) (hH : (H.normalized hT g hg).WordBound q R B d) : ((G.sub H).normalized hT g hg).WordBound q R (A + B) d

theorem EulerPacketCylinderField.Field.WordBound.normalized_neg {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} (hT : 0 ≤ T) {g : C(↑(Set.Icc 0 T), ℝ)} {hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t} {q d : ℕ} {R A : ℝ} (hG : (G.normalized hT g hg).WordBound q R A d) : (G.neg.normalized hT g hg).WordBound q R A d

theorem EulerPacketCylinderField.Field.WordBound.normalized_derivative {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} (hT : 0 ≤ T) {g : C(↑(Set.Icc 0 T), ℝ)} {hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t} {q d : ℕ} {R A : ℝ} (hG : (G.normalized hT g hg).WordBound q R A d) (i : Fin 4) : ((G.derivative i).normalized hT g hg).WordBound q R A (d + 1)

theorem EulerPacketCylinderField.Field.WordBound.normalized_multiply {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} (hT : 0 ≤ T) {g : C(↑(Set.Icc 0 T), ℝ)} {hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t} {q d : ℕ} {R A : ℝ} (hG : (G.normalized hT g hg).WordBound q R A d) {coef : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (K : MatrixCoefficient T coef) (Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hA : 0 ≤ A) (hR : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) Rc ≤ R) (hK : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath K.path) a‖ ≤ C * EulerGevrey.majorant Rc 0 n) : ((K.multiply G).normalized hT g hg).WordBound q R (3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) q Rc C * A) d

theorem EulerPacketCylinderField.Field.wordBound_normalized_finsetSum {P T : ℝ} [Fact (0 < P)] (hT : 0 ≤ T) {g : C(↑(Set.Icc 0 T), ℝ)} {hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t} {ι : Type u_1} (s : Finset ι) (f : ι → EulerPacketProfileRecursion.VectorField) (W : (i : ι) → Field P T (f i)) (q : ℕ) (R : ℝ) (d : ℕ) (A : ι → ℝ) (hW : ∀ i ∈ s, ((W i).normalized hT g hg).WordBound q R (A i) d) : ((finsetSum s f W).normalized hT g hg).WordBound q R (∑ i ∈ s, A i) d

theorem EulerPacketCylinderField.Field.WordBound.angleMean {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q d : ℕ} {R A : ℝ} (hG : G.WordBound q R A d) : G.angleMean.WordBound q R A d

theorem EulerPacketCylinderField.Field.normalized_angleMean_path {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (hT : 0 ≤ T) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) : (G.angleMean.normalized hT g hg).path = (G.normalized hT g hg).angleMean.path

theorem EulerPacketCylinderField.Field.WordBound.normalized_angleMean {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} (hT : 0 ≤ T) {g : C(↑(Set.Icc 0 T), ℝ)} {hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t} {q d : ℕ} {R A : ℝ} (hG : (G.normalized hT g hg).WordBound q R A d) : (G.angleMean.normalized hT g hg).WordBound q R A d