RelativeError: full smoothness of the inverse-flow transported test

theorem AVenhance.Infra.Section5.RelativeError.inverseFlowTransportTest_contDiff_infty {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) {h₀ : Homogenization.Vec 2 → ℝ} (hh₀ : ContDiff ℝ (↑⊤) h₀) : ContDiff ℝ (↑⊤) (Function.uncurry (inverseFlowTransportTest X))

A smooth initial scalar transported by the inverse flow remains jointly smooth in time and space. This supplies the regularity needed by the integrated parabolic/transport pairing identity.