Fixed-start C¹ smooth dependence for each finite recursive jet flow.

noncomputable def AVenhance.Infra.Flow.spatialJetFlowDerivativeOperator {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlowOn b X) (n : ℕ) (t s : ℝ) (z : SpatialJetState n) : SpatialJetState n →L[ℝ] SpatialJetState n

Reconstruct the full state derivative from the next recursive jet flow.

Equations

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

theorem AVenhance.Infra.Flow.spatialJetFlowDerivativeOperator_continuous {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlowOn b X) (n : ℕ) (s : ℝ) : Continuous fun (p : ℝ × SpatialJetState n) => spatialJetFlowDerivativeOperator hb hX n p.1 s p.2

The reconstructed operator is continuous in the base state.

theorem AVenhance.Infra.Flow.spatialJetFlow_hasFDerivAt_forward {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlowOn b X) (n : ℕ) (s t : ℝ) (hst : s ≤ t) (z : SpatialJetState n) : HasFDerivAt (fun (w : SpatialJetState n) => spatialJetFlow hb X hX n t w s) (spatialJetFlowDerivativeOperator hb hX n t s z) z

theorem AVenhance.Infra.Flow.FiniteSpatialJetC1.isFlowOn_reverseTime {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : ℝ → E → E} {Y : ℝ → E → ℝ → E} (hY : IsFlowOn F Y) : IsFlowOn (fun (t : ℝ) (z : E) => -F (-t) z) fun (t : ℝ) (z : E) (s : ℝ) => Y (-t) z (-s)

theorem AVenhance.Infra.Flow.FiniteSpatialJetC1.spatialJetField_reverseTime {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) (n : ℕ) (t : ℝ) (z : SpatialJetState n) : spatialJetField (regularityReverseTimeField b) n t z = -spatialJetField b n (-t) z

theorem AVenhance.Infra.Flow.spatialJetFlow_reverseTime_eq {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlowOn b X) (n : ℕ) (t : ℝ) (z : SpatialJetState n) (s : ℝ) : spatialJetFlow ⋯ (regularityReverseTimeFlow X) ⋯ n t z s = spatialJetFlow hb X hX n (-t) z (-s)

theorem AVenhance.Infra.Flow.spatialJetFlow_hasFDerivAt {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlowOn b X) (n : ℕ) (s t : ℝ) (z : SpatialJetState n) : HasFDerivAt (fun (w : SpatialJetState n) => spatialJetFlow hb X hX n t w s) (spatialJetFlowDerivativeOperator hb hX n t s z) z

theorem AVenhance.Infra.Flow.spatialJetFlow_spatial_contDiff_one {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlowOn b X) (n : ℕ) (s t : ℝ) : ContDiff ℝ 1 fun (z : SpatialJetState n) => spatialJetFlow hb X hX n t z s

theorem AVenhance.Infra.Flow.spatialJetFlow_fixed_start_contDiff_one {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlowOn b X) (n : ℕ) (s : ℝ) : ContDiff ℝ 1 fun (p : ℝ × SpatialJetState n) => spatialJetFlow hb X hX n p.1 p.2 s

Every finite recursive jet flow is jointly C¹ in target time and its initial state when the start time is fixed.

theorem AVenhance.Infra.Flow.spatialJetFlow_fixed_start_hasFDerivAt {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlowOn b X) (n : ℕ) (s : ℝ) (p : ℝ × SpatialJetState n) : HasFDerivAt (fun (q : ℝ × SpatialJetState n) => spatialJetFlow hb X hX n q.1 q.2 s) ((ContinuousLinearMap.toSpanSingleton ℝ (spatialJetField b n p.1 (spatialJetFlow hb X hX n p.1 p.2 s))).coprod (spatialJetFlowDerivativeOperator hb hX n p.1 s p.2)) p

Explicit total derivative for the fixed-start augmented flow.