Joint smoothness from fixed-start smoothness and the global flow law.

def AVenhance.Infra.Flow.JointSmoothFromFixedStart.flowGraphForward (X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2) : ℝ × Homogenization.Vec 2 → ℝ × Homogenization.Vec 2

Graph map advancing each spatial point from time zero to its time coordinate.

Equations

• AVenhance.Infra.Flow.JointSmoothFromFixedStart.flowGraphForward X p = (p.1, X p.1 p.2 0)

def AVenhance.Infra.Flow.JointSmoothFromFixedStart.flowGraphBackward (X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2) : ℝ × Homogenization.Vec 2 → ℝ × Homogenization.Vec 2

Graph map returning each spatial point from its time coordinate to time zero.

Equations

• AVenhance.Infra.Flow.JointSmoothFromFixedStart.flowGraphBackward X p = (p.1, X 0 p.2 p.1)

theorem AVenhance.Infra.Flow.JointSmoothFromFixedStart.flow_graph_maps_are_inverse {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) : Function.LeftInverse (flowGraphBackward X) (flowGraphForward X) ∧ Function.RightInverse (flowGraphBackward X) (flowGraphForward X)

theorem AVenhance.Infra.Flow.JointSmoothFromFixedStart.flowGraphForward_contDiff {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) : ContDiff ℝ (↑⊤) (flowGraphForward X)

theorem AVenhance.Infra.Flow.JointSmoothFromFixedStart.flowGraphBackward_contDiff_one {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) : ContDiff ℝ 1 (flowGraphBackward X)

theorem AVenhance.Infra.Flow.JointSmoothFromFixedStart.flowGraphBackward_contDiff_infty {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) : ContDiff ℝ (↑⊤) (flowGraphBackward X)

theorem AVenhance.Infra.Flow.JointSmoothFromFixedStart.flowZeroStartPosition_contDiff_infty {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => X 0 p.2 p.1

theorem AVenhance.Infra.Flow.flow_joint_contDiff_infty {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2 × ℝ) => X p.1 p.2.1 p.2.2

The nonautonomous flow is smooth jointly in target time, initial position, and start time. The proof first bootstraps all fixed-start augmented flows, then applies the inverse function theorem to the global graph map (s,x) ↦ (s, X(s,x,0)).

theorem AVenhance.Infra.Flow.flow_inverse_joint_contDiff_infty {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2 × ℝ) => X p.2.2 p.2.1 p.1

The reversed-time-variable flow map is jointly smooth as well.