The literal finite packet and its genuine time derivative are actual cylinder fields.

noncomputable def EulerPacketCylinderField.rawTimeDerivative (T : ℝ) (raw : EulerPacketProfileRecursion.VectorField) : EulerPacketProfileRecursion.VectorField

Raw time derivative, defined pointwise by derivWithin (fun t => raw (t,z.2)) (Icc (0 : ℝ) T) z.1.

Equations

• EulerPacketCylinderField.rawTimeDerivative T raw z = derivWithin (fun (t : ℝ) => raw (t, z.2)) (Set.Icc 0 T) z.1

noncomputable def EulerPacketCylinderField.Field.timeDerivativeField {P T : ℝ} [Fact (0 < P)] {raw raw_t : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (hT : 0 < T) (H : Field P T raw_t) (ht : TimeDerivative ⋯ G H) : Field P T (rawTimeDerivative T raw)

Time derivative field, given by H.congr (fun t x θ => (G.raw_hasDerivWithinAt hT.le H ht t x θ).derivWithin ((uniqueDiffOn_Icc hT) _ t.property)).

Equations

• G.timeDerivativeField hT H ht = H.congr ⋯

theorem EulerPacketCylinderField.Field.timeDerivativeField_time {P T : ℝ} [Fact (0 < P)] {raw raw_t : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (hT : 0 < T) (H : Field P T raw_t) (ht : TimeDerivative ⋯ G H) : TimeDerivative ⋯ G (G.timeDerivativeField hT H ht)

noncomputable def EulerPacketCylinderField.ProfileRegularity.velocityGradeField {P T : ℝ} [Fact (0 < P)] {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} {support : Set EulerSmoothLimit.Space} (hT : 0 < T) (G : (i : ℕ) → i ≤ N → ProfileRegularity P T ⋯ support (a i)) (i : ℕ) : Field P T (EulerPacketProfileRecursion.assembledVelocity N a i)

Velocity grade field, constructed using Field.assembleFamily.

Equations

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

noncomputable def EulerPacketCylinderField.ProfileRegularity.velocityTimeCoefficients {T : ℝ} {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} : ℕ → EulerPacketProfileRecursion.VectorField

Velocity time coefficients, given by assemble N (fun i => rawTimeDerivative T ((a i).high+(a i).mean)) (fun i => rawTimeDerivative T (a i).corrector).

Equations

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

noncomputable def EulerPacketCylinderField.ProfileRegularity.velocityGradeDerivativeField {P T : ℝ} [Fact (0 < P)] {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} {support : Set EulerSmoothLimit.Space} (hT : 0 < T) (G : (i : ℕ) → i ≤ N → ProfileRegularity P T ⋯ support (a i)) (i : ℕ) : Field P T (velocityTimeCoefficients i)

Velocity grade derivative field, constructed using Field.assembleFamily.

Equations

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

theorem EulerPacketCylinderField.ProfileRegularity.velocityGrade_time {P T : ℝ} [Fact (0 < P)] {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} {support : Set EulerSmoothLimit.Space} (hT : 0 < T) (G : (i : ℕ) → i ≤ N → ProfileRegularity P T ⋯ support (a i)) (i : ℕ) : TimeDerivative ⋯ (velocityGradeField hT G i) (velocityGradeDerivativeField hT G i)

noncomputable def EulerPacketCylinderField.ProfileRegularity.velocityField {P T : ℝ} [Fact (0 < P)] {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} {support : Set EulerSmoothLimit.Space} (hT : 0 < T) (G : (i : ℕ) → i ≤ N → ProfileRegularity P T ⋯ support (a i)) (κ : ℝ) : Field P T (EulerPacketPointJets.fieldSum (N + 1) κ (EulerPacketProfileRecursion.assembledVelocity N a))

Velocity field, given by Field.evaluateFamily (N+1) κ _ (velocityGradeField hT G).

Equations

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

noncomputable def EulerPacketCylinderField.ProfileRegularity.velocityDerivativeField {P T : ℝ} [Fact (0 < P)] {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} {support : Set EulerSmoothLimit.Space} (hT : 0 < T) (G : (i : ℕ) → i ≤ N → ProfileRegularity P T ⋯ support (a i)) (κ : ℝ) : Field P T (EulerPacketPointJets.fieldSum (N + 1) κ velocityTimeCoefficients)

Velocity derivative field, given by Field.evaluateFamily (N+1) κ _ (velocityGradeDerivativeField hT G).

Equations

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

theorem EulerPacketCylinderField.ProfileRegularity.velocityField_time {P T : ℝ} [Fact (0 < P)] {N : ℕ} {a : ℕ → EulerPacketProfileRecursion.Profile} {support : Set EulerSmoothLimit.Space} (hT : 0 < T) (G : (i : ℕ) → i ≤ N → ProfileRegularity P T ⋯ support (a i)) (κ : ℝ) : TimeDerivative ⋯ (velocityField hT G κ) (velocityDerivativeField hT G κ)