Bounds for literal high projection and for the zero fields in masked grade families.

@[simp]

theorem EulerPacketCylinderField.Field.highPart_path {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) : G.highPart.path = G.path - (EulerCylinderAngleAverage.pathAverage P) G.path

theorem EulerPacketCylinderField.Field.wordBound_of_zero {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (hz : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, x, θ) = 0) (q : ℕ) (R : ℝ) (d : ℕ) : G.WordBound q R 0 d

theorem EulerPacketCylinderField.Field.wordBound_normalized_of_zero {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (hz : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, x, θ) = 0) (hT : 0 ≤ T) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (q : ℕ) (R : ℝ) (d : ℕ) : (G.normalized hT g hg).WordBound q R 0 d

theorem EulerPacketCylinderField.Field.WordBound.highPart {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.highPart.WordBound q R (2 * A) d

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