Finite grade convolution of actual raw cylinder fields.

noncomputable def EulerPacketCylinderField.Field.convolution {P T : ℝ} [Fact (0 < P)] (M n : ℕ) (f : ℕ → ℕ → EulerPacketProfileRecursion.VectorField) (G : (i j : ℕ) → Field P T (f i j)) : Field P T fun (z : EulerPacketPointJets.Domain) => ∑ i ∈ Finset.range (M + 1), ∑ j ∈ Finset.range (M + 1), if i + j = n then f i j z else 0

A grade selector and two finite sums preserve genuine raw-field admissibility.

Equations

• One or more equations did not get rendered due to their size.