RelativeError: control the gradient of the transported test

theorem AVenhance.Infra.Section5.RelativeError.TransportTraceGradient.inverseFlow_transportedGradient_pointwise_le {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) {B T : ℝ} (hB : 0 ≤ B) (hBT : B * T ≤ 1) (hDb : ∀ (r : ℝ) (y : Homogenization.Vec 2), ‖Flow.jointSpatialFDeriv b r y‖ ≤ B) {h₀ : Homogenization.Vec 2 → ℝ} (hh₀ : ContDiff ℝ (↑⊤) h₀) {t : ℝ} (ht : t ∈ Set.Icc 0 T) (x : Homogenization.Vec 2) : Homogenization.vecNormSq (spaceGrad (inverseFlowTransportTest X t) x) ≤ 4 * Real.exp 1 ^ 2 * Homogenization.vecNormSq (spaceGrad h₀ (X 0 x t))