All finite recursive jet flows are smooth at each fixed start time.
theorem
AVenhance.Infra.Flow.spatialJetFlowDerivativeOperator_contDiff_of_next
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
(hb : SmoothPeriodicField b)
{X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2}
(hX : IsFlowOn b X)
(n k : ℕ)
(s : ℝ)
(hnext : ContDiff ℝ ↑k fun (p : ℝ × SpatialJetState (n + 1)) => spatialJetFlow hb X hX (n + 1) p.1 p.2 s)
:
ContDiff ℝ ↑k fun (p : ℝ × SpatialJetState n) => spatialJetFlowDerivativeOperator hb hX n p.1 s p.2
The next jet flow makes the reconstructed state derivative smooth.
theorem
AVenhance.Infra.Flow.FiniteSpatialJetSmooth.spatialJetFlow_fixed_start_contDiff_nat_all
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
(hb : SmoothPeriodicField b)
{X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2}
(hX : IsFlowOn b X)
(s : ℝ)
(k n : ℕ)
:
ContDiff ℝ ↑k fun (p : ℝ × SpatialJetState n) => spatialJetFlow hb X hX n p.1 p.2 s
theorem
AVenhance.Infra.Flow.spatialJetFlow_fixed_start_contDiff_infty
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
(hb : SmoothPeriodicField b)
{X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2}
(hX : IsFlowOn b X)
(n : ℕ)
(s : ℝ)
:
ContDiff ℝ ↑⊤ fun (p : ℝ × SpatialJetState n) => spatialJetFlow hb X hX n p.1 p.2 s
Every finite recursively augmented flow is jointly C∞ in target time and its initial state when the start time is fixed.
theorem
AVenhance.Infra.Flow.flow_target_initial_contDiff_infty_fixed_start
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
(hb : SmoothPeriodicField b)
{X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2}
(hX : IsFlowOn b X)
(s : ℝ)
:
The original flow is smooth jointly in target time and initial position for every fixed start time.