Product-rule lemmas for the transport identity of the finite cutoff ansatz.

theorem AVenhance.Infra.Section5.hasDerivAt_vecDot {χ G : ℝ → Homogenization.Vec 2} {χ' G' : Homogenization.Vec 2} {t : ℝ} (hχ : HasDerivAt χ χ' t) (hG : HasDerivAt G G' t) : HasDerivAt (fun (s : ℝ) => Homogenization.vecDot (χ s) (G s)) (Homogenization.vecDot χ' (G t) + Homogenization.vecDot (χ t) G') t

Derivative of the vector pairing along a curve.

theorem AVenhance.Infra.Section5.hasDerivAt_finiteAnsatz {ι : Type u_1} (S : Finset ι) (T H T' H' : ℝ → ℝ) (ξ ξ' : ι → ℝ → ℝ) (χ G χ' G' : ι → ℝ → Homogenization.Vec 2) {t : ℝ} (hT : HasDerivAt T (T' t) t) (hH : HasDerivAt H (H' t) t) (hξ : ∀ k ∈ S, HasDerivAt (ξ k) (ξ' k t) t) (hχ : ∀ k ∈ S, HasDerivAt (χ k) (χ' k t) t) (hG : ∀ k ∈ S, HasDerivAt (G k) (G' k t) t) : HasDerivAt (fun (s : ℝ) => T s + ∑ k ∈ S, ξ k s * Homogenization.vecDot (χ k s) (G k s) + H s) (T' t + ∑ k ∈ S, (ξ' k t * Homogenization.vecDot (χ k t) (G k t) + ξ k t * (Homogenization.vecDot (χ' k t) (G k t) + Homogenization.vecDot (χ k t) (G' k t))) + H' t) t

Derivative of a finite cutoff ansatz along any differentiable curve. The two summands inside each product are kept separate, matching e.timecomp.0.