Recursive finite spatial-jet state spaces and their smooth augmented ODE fields.

def AVenhance.Infra.Flow.SpatialJetState : ℕ → Type

The state of the nth spatial-jet system: at each stage append the derivative of the preceding jet with respect to the original base point.

Equations

• AVenhance.Infra.Flow.SpatialJetState 0 = Homogenization.Vec 2
• AVenhance.Infra.Flow.SpatialJetState n.succ = (AVenhance.Infra.Flow.SpatialJetState n × (Fin 2 → AVenhance.Infra.Flow.SpatialJetState n))

@[instance_reducible]

instance AVenhance.Infra.Flow.instNormedAddCommGroupSpatialJetState (n : ℕ) : NormedAddCommGroup (SpatialJetState n)

Equations

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

@[instance_reducible]

noncomputable instance AVenhance.Infra.Flow.instNormedSpaceRealSpatialJetState (n : ℕ) : NormedSpace ℝ (SpatialJetState n)

Equations

• AVenhance.Infra.Flow.instNormedSpaceRealSpatialJetState n = Nat.recAux (id inferInstance) (fun (n : ℕ) (ih : NormedSpace ℝ (AVenhance.Infra.Flow.SpatialJetState n)) => id inferInstance) n

instance AVenhance.Infra.Flow.instCompleteSpaceSpatialJetState (n : ℕ) : CompleteSpace (SpatialJetState n)

instance AVenhance.Infra.Flow.instFiniteDimensionalRealSpatialJetState (n : ℕ) : FiniteDimensional ℝ (SpatialJetState n)

instance AVenhance.Infra.Flow.instNontrivialSpatialJetState (n : ℕ) : Nontrivial (SpatialJetState n)

noncomputable def AVenhance.Infra.Flow.spatialJetField (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (n : ℕ) : ℝ → SpatialJetState n → SpatialJetState n

The recursive augmented field. Its new component is the state derivative of the preceding augmented field, composed with the appended jet direction.

Equations

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

theorem AVenhance.Infra.Flow.spatialJetField_smooth {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) (n : ℕ) : ContDiff ℝ (↑⊤) (Function.uncurry (spatialJetField b n))

Every finite augmented spatial-jet field is smooth when the original field is smooth. The induction uses smoothness of Fréchet derivatives and evaluation.

theorem AVenhance.Infra.Flow.spatialJetField_lipschitzOnWith_on_window {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) (n : ℕ) (a d : ℝ) (z₀ : SpatialJetState n) (R : ℝ) : ∃ (K : NNReal), ∀ t ∈ Set.Icc a d, LipschitzOnWith K (spatialJetField b n t) (Metric.closedBall z₀ R)

On a compact time window and a closed ball of jet states, one common spatial Lipschitz constant controls the recursive jet field. The constant is obtained by bounding the state derivative on the compact product.

theorem AVenhance.Infra.Flow.spatialJetField_flow_unique_on_window {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) (n : ℕ) {Y Z : ℝ → SpatialJetState n → ℝ → SpatialJetState n} (hY : IsFlowOn (spatialJetField b n) Y) (hZ : IsFlowOn (spatialJetField b n) Z) (a d s : ℝ) (hs : s ∈ Set.Icc a d) (z : SpatialJetState n) (t : ℝ) : t ∈ Set.Icc a d → Y t z s = Z t z s

Any two global solutions of a finite jet equation agree on a finite time window when they start from the same state. The proof uses boundedness of each continuous trajectory on the window, then the common ball Lipschitz estimate.

theorem AVenhance.Infra.Flow.spatialJetField_one_eq_firstJetField {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} : spatialJetField b 1 = firstJetField b

The first recursive jet field agrees with the established position and Jacobian augmented field.