Global recursive jet flows, built by solving each new derivative level as a linear equation along the preceding jet trajectory.

noncomputable def AVenhance.Infra.Flow.FiniteSpatialJetGlobal.spatialJetLinearCoefficient (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (n : ℕ) (Y : ℝ → SpatialJetState n → ℝ → SpatialJetState n) (z : SpatialJetState n) (s t : ℝ) : SpatialJetState n →L[ℝ] SpatialJetState n

Linear coefficient governing the next spatial jet along the lower-order jet flow.

Equations

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

theorem AVenhance.Infra.Flow.FiniteSpatialJetGlobal.spatialJetLinearCoefficient_continuous {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {n : ℕ} {Y : ℝ → SpatialJetState n → ℝ → SpatialJetState n} (hY : IsFlowOn (spatialJetField b n) Y) (z : SpatialJetState n) (s : ℝ) : Continuous (spatialJetLinearCoefficient b n Y z s)

noncomputable def AVenhance.Infra.Flow.FiniteSpatialJetGlobal.chosenLinearFlow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (A : ℝ → E →L[ℝ] E) (hA : Continuous A) : ℝ → E → ℝ → E

Choose the unique global flow of a continuous linear differential equation.

Equations

• AVenhance.Infra.Flow.FiniteSpatialJetGlobal.chosenLinearFlow A hA = Classical.choose ⋯

theorem AVenhance.Infra.Flow.FiniteSpatialJetGlobal.chosenLinearFlow_isFlow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (A : ℝ → E →L[ℝ] E) (hA : Continuous A) : IsFlowOn (fun (t : ℝ) (z : E) => (A t) z) (chosenLinearFlow A hA)

noncomputable def AVenhance.Infra.Flow.FiniteSpatialJetGlobal.spatialJetLinearFlow {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {n : ℕ} (Y : ℝ → SpatialJetState n → ℝ → SpatialJetState n) (hY : IsFlowOn (spatialJetField b n) Y) (z : SpatialJetState n) (s : ℝ) : ℝ → SpatialJetState n → ℝ → SpatialJetState n

Linear flow used to extend a given spatial jet by one derivative order.

Equations

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

theorem AVenhance.Infra.Flow.FiniteSpatialJetGlobal.spatialJetLinearFlow_isFlow {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {n : ℕ} (Y : ℝ → SpatialJetState n → ℝ → SpatialJetState n) (hY : IsFlowOn (spatialJetField b n) Y) (z : SpatialJetState n) (s : ℝ) : IsFlowOn (fun (t : ℝ) (v : SpatialJetState n) => (spatialJetLinearCoefficient b n Y z s t) v) (spatialJetLinearFlow hb Y hY z s)

noncomputable def AVenhance.Infra.Flow.FiniteSpatialJetGlobal.spatialJetFlowNext {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {n : ℕ} (Y : ℝ → SpatialJetState n → ℝ → SpatialJetState n) (hY : IsFlowOn (spatialJetField b n) Y) : ℝ → SpatialJetState (n + 1) → ℝ → SpatialJetState (n + 1)

One recursive jet extension over an already constructed lower flow.

Equations

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

theorem AVenhance.Infra.Flow.FiniteSpatialJetGlobal.spatialJetFlowNext_isFlow {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {n : ℕ} (Y : ℝ → SpatialJetState n → ℝ → SpatialJetState n) (hY : IsFlowOn (spatialJetField b n) Y) : IsFlowOn (spatialJetField b (n + 1)) (spatialJetFlowNext hb Y hY)

noncomputable def AVenhance.Infra.Flow.FiniteSpatialJetGlobal.spatialJetFlowData {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) (X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2) (hX : IsFlowOn b X) (n : ℕ) : { Y : ℝ → SpatialJetState n → ℝ → SpatialJetState n // IsFlowOn (spatialJetField b n) Y }

Compatible spatial jet flows constructed inductively from the underlying flow.

Equations

• One or more equations did not get rendered due to their size.
• AVenhance.Infra.Flow.FiniteSpatialJetGlobal.spatialJetFlowData hb X hX 0 = ⟨X, hX⟩

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

The initial value of each recursive jet flow is the corresponding jet of the identity map: position is x, the first derivative is the identity, and every higher derivative is zero.

Equations

• One or more equations did not get rendered due to their size.
• AVenhance.Infra.Flow.spatialJetIdentitySeed 0 = id

theorem AVenhance.Infra.Flow.spatialJetIdentitySeed_smooth (n : ℕ) : ContDiff ℝ (↑⊤) (spatialJetIdentitySeed n)

Every identity-jet seed is smooth.

theorem AVenhance.Infra.Flow.spatialJetIdentitySeed_one (x : Homogenization.Vec 2) : spatialJetIdentitySeed 1 x = (x, fun (i : Fin 2) => Pi.single i 1)

The first identity jet consists of the point and its two coordinate directions.

noncomputable def AVenhance.Infra.Flow.spatialJetFlow {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) (X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2) (hX : IsFlowOn b X) (n : ℕ) : ℝ → SpatialJetState n → ℝ → SpatialJetState n

A recursively augmented jet flow. Each new column is obtained from the global linear variational equation along the preceding jet trajectory.

Equations

• AVenhance.Infra.Flow.spatialJetFlow hb X hX n = ↑(AVenhance.Infra.Flow.FiniteSpatialJetGlobal.spatialJetFlowData hb X hX n)

theorem AVenhance.Infra.Flow.spatialJetFlow_isFlow {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlowOn b X) (n : ℕ) : IsFlowOn (spatialJetField b n) (spatialJetFlow hb X hX n)

Every recursive finite jet equation has a global flow. Existence at each new level follows from global existence for its linear variational columns.