Chain rules for the transport identities in Section 5.1.

theorem AVenhance.Infra.Section5.deriv_uncurry_comp {F : ℝ → Homogenization.Vec 2 → ℝ} {γ : ℝ → ℝ × Homogenization.Vec 2} {t : ℝ} {v : ℝ × Homogenization.Vec 2} {L : ℝ × Homogenization.Vec 2 →L[ℝ] ℝ} (hF : HasFDerivAt (Function.uncurry F) L (γ t)) (hγ : HasDerivAt γ v t) : deriv (fun (s : ℝ) => Function.uncurry F (γ s)) t = L v

Differentiate a smooth scalar field along a spacetime curve.

theorem AVenhance.Infra.Section5.deriv_comp_flow {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} {F : ℝ → Homogenization.Vec 2 → ℝ} {t s : ℝ} {x : Homogenization.Vec 2} {v : ℝ × Homogenization.Vec 2 →L[ℝ] ℝ} (hF : HasFDerivAt (Function.uncurry F) v (t, X t x s)) (hX : IsFlow b X) : deriv (fun (r : ℝ) => F r (X r x s)) t = v (1, b t (X t x s))

The derivative of F pulled back by a forward flow, in spacetime Fréchet-derivative form.

theorem AVenhance.Infra.Section5.inverse_transport_comp {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {F : ℝ → Homogenization.Vec 2 → ℝ} {Z : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {t : ℝ} {x z v : Homogenization.Vec 2} {L : ℝ × Homogenization.Vec 2 →L[ℝ] ℝ} {A : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} (hF : HasFDerivAt (Function.uncurry F) L (t, z)) (hZtime : HasDerivAt (fun (s : ℝ) => Z s x) v t) (hZspace : HasFDerivAt (Z t) A x) (hz : Z t x = z) (htransport : v + A (b t x) = 0) : deriv (fun (s : ℝ) => F s (Z s x)) t + (fderiv ℝ (fun (y : Homogenization.Vec 2) => F t (Z t y)) x) (b t x) = L (1, 0)

Transport calculus for composition with a time-dependent inverse map. The inverse transport equation is the single cancellation hypothesis ∂ₜZ + DₓZ b = 0; all composition and product rules are proved here.

theorem AVenhance.Infra.Section5.inverse_flow_transport_comp {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} {Z : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {F : ℝ → Homogenization.Vec 2 → ℝ} {s t : ℝ} {x : Homogenization.Vec 2} {L : ℝ × Homogenization.Vec 2 →L[ℝ] ℝ} {M : ℝ × Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} (hF : HasFDerivAt (Function.uncurry F) L (t, Z t x)) (hZ : HasFDerivAt (Function.uncurry Z) M (t, x)) (hX : IsFlow b X) (hleft : ∀ (r : ℝ) (y : Homogenization.Vec 2), Z r (X r y s) = y) (hright : ∀ (r : ℝ) (y : Homogenization.Vec 2), X r (Z r y) s = y) : deriv (fun (r : ℝ) => F r (Z r x)) t + (fderiv ℝ (fun (y : Homogenization.Vec 2) => F t (Z t y)) x) (b t x) = L (1, 0)

The inverse-flow transport formula, derived from the forward ODE and the two inverse identities. Smoothness of the inverse map is stated as a Fréchet derivative hypothesis so this bridge can be instantiated independently of a particular flow regularity theorem.

theorem AVenhance.Infra.Section5.inverse_flow_transport_comp_apply {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} {Z F : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {s t : ℝ} {x : Homogenization.Vec 2} {L M : ℝ × Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} (hF : HasFDerivAt (Function.uncurry F) L (t, Z t x)) (hZ : HasFDerivAt (Function.uncurry Z) M (t, x)) (hX : IsFlow b X) (hleft : ∀ (r : ℝ) (y : Homogenization.Vec 2), Z r (X r y s) = y) (hright : ∀ (r : ℝ) (y : Homogenization.Vec 2), X r (Z r y) s = y) (i : Fin 2) : deriv (fun (r : ℝ) => F r (Z r x) i) t + (fderiv ℝ (fun (y : Homogenization.Vec 2) => F t (Z t y) i) x) (b t x) = L (1, 0) i

Coordinate form of the inverse-flow transport formula for a vector field. This is the form used for the pulled gradient in e.tbm1.two.