Genuine within-interval time derivatives commute with the finite packet algebra.
theorem
EulerPacketCylinderField.TimeDerivative.zero
{P T : ℝ}
[Fact (0 < P)]
{hT : 0 ≤ T}
:
TimeDerivative hT (Field.zero P T) (Field.zero P T)
theorem
EulerPacketCylinderField.TimeDerivative.add
{P T : ℝ}
[Fact (0 < P)]
{hT : 0 ≤ T}
{raw raw' next next' : EulerPacketProfileRecursion.VectorField}
{G : Field P T raw}
{G' : Field P T raw'}
{H : Field P T next}
{H' : Field P T next'}
(hG : TimeDerivative hT G G')
(hH : TimeDerivative hT H H')
:
TimeDerivative hT (G.add H) (G'.add H')
theorem
EulerPacketCylinderField.TimeDerivative.smul
{P T : ℝ}
[Fact (0 < P)]
{hT : 0 ≤ T}
{raw raw' : EulerPacketProfileRecursion.VectorField}
{G : Field P T raw}
{G' : Field P T raw'}
(hG : TimeDerivative hT G G')
(c : ℝ)
:
TimeDerivative hT (G.smul c) (G'.smul c)
theorem
EulerPacketCylinderField.TimeDerivative.finsetSum
{P T : ℝ}
[Fact (0 < P)]
{hT : 0 ≤ T}
{ι : Type u_1}
(s : Finset ι)
(f f' : ι → EulerPacketProfileRecursion.VectorField)
(G : (i : ι) → Field P T (f i))
(G' : (i : ι) → Field P T (f' i))
(hG : ∀ i ∈ s, TimeDerivative hT (G i) (G' i))
:
TimeDerivative hT (Field.finsetSum s f G) (Field.finsetSum s f' G')
theorem
EulerPacketCylinderField.TimeDerivative.of_path_eq
{P T : ℝ}
[Fact (0 < P)]
{hT : 0 ≤ T}
{raw raw' next next' : EulerPacketProfileRecursion.VectorField}
{G : Field P T raw}
{G' : Field P T raw'}
{H : Field P T next}
{H' : Field P T next'}
(hG : TimeDerivative hT G G')
(h : H.path = G.path)
(h' : H'.path = G'.path)
:
TimeDerivative hT H H'