Actual globally smooth inverse maps and source flow primitives.

theorem AVenhance.Infra.Section4.amnr_flow_inverse_joint_contDiff_infty_global {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) {M : ℝ} (hM : 0 ≤ M) (hstate : ∀ (t : ℝ) (x : Homogenization.Vec 2), ‖Flow.jointSpatialFDeriv b t x‖ ≤ M) (s : ℝ) : ContDiff ℝ ↑⊤ fun (z : ℝ × Homogenization.Vec 2) => X s z.2 z.1

Actual inverse identities extend the global forward joint smoothness to the actual inverse flow, at every target time and point.

theorem AVenhance.Infra.Section4.amnr_smoothPeriodic_global_stateJacobian_bound {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (t : ℝ) (x : Homogenization.Vec 2), ‖Flow.jointSpatialFDeriv b t x‖ ≤ M

Every smooth periodic primitive field has a proved global Jacobian bound, sufficient for the finite subdivision argument.

theorem AVenhance.Infra.Section4.amnr_xFlow_joint_contDiff_infty {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) : ContDiff ℝ ↑⊤ fun (z : AmnrSpace) => I.xFlow hΦ m l z.1 z.2

Qualitative joint smoothness of the actual source forward flow requires only its proved admissible stream smoothness, without any quantitative stream-regularity input.

theorem AVenhance.Infra.Section4.amnr_xFlowInv_joint_contDiff_infty {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) : ContDiff ℝ ↑⊤ fun (z : AmnrSpace) => I.xFlowInv hΦ m l z.1 z.2

The actual source inverse flow is jointly smooth at every time.

theorem AVenhance.Infra.Section4.amnr_flowGrad_joint_contDiff_infty {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (i j : Fin 2) : ContDiff ℝ ↑⊤ fun (z : AmnrSpace) => I.flowGrad hΦ m l z.1 z.2 i j

The actual pulled source Jacobian is jointly smooth globally. Its quantitative cutoff estimates are proved in separate declarations.