Smoothness of actual inverses from proved C¹ inverse identities.

theorem AVenhance.Infra.Section4.amnr_contDiffAt_inverse_of_differentiable_inverses {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {P Q : E → E} {x : E} (hP : ContDiffAt ℝ (↑⊤) P (Q x)) (hQ : DifferentiableAt ℝ Q x) (hleft : ∀ (y : E), Q (P y) = y) (hright : ∀ (y : E), P (Q y) = y) : ContDiffAt ℝ (↑⊤) Q x

A C¹ inverse of a locally smooth map is locally smooth. Invertibility of the derivative is obtained by differentiating the actual two inverse identities, rather than supplied as an additional premise.

theorem AVenhance.Infra.Section4.amnr_flow_inverse_contDiffAt_joint_of_short {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 t : ℝ) (x : Homogenization.Vec 2) (hshort : |t - s| * M ≤ 1 / 4) : ContDiffAt ℝ (↑⊤) (fun (z : ℝ × Homogenization.Vec 2) => X s z.2 z.1) (t, x)

The actual inverse flow is jointly smooth wherever the actual forward flow is smooth on the short interval. Its C¹ inverse identities are already proved from the characterized ODE.