Coordinate chain rule for the flow-pulled gradient used in Section 5.1.

theorem AVenhance.Infra.Section5.spaceGrad_comp_eq_gradMatrix_mul {f : Homogenization.Vec 2 → ℝ} {X : Homogenization.Vec 2 → Homogenization.Vec 2} {x : Homogenization.Vec 2} {Lf : Homogenization.Vec 2 →L[ℝ] ℝ} {LX : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} (hf : HasFDerivAt f Lf (X x)) (hX : HasFDerivAt X LX x) (i : Fin 2) : spaceGrad (fun (y : Homogenization.Vec 2) => f (X y)) x i = ∑ j : Fin 2, gradMatrix X x i j * spaceGrad f (X x) j

The gradient of a scalar composition is the flow Jacobian times the gradient of the outer function, in the row-Jacobian convention of gradMatrix.

theorem AVenhance.Infra.Section5.spaceGrad_vecDot {χ G : Homogenization.Vec 2 → Homogenization.Vec 2} {x : Homogenization.Vec 2} {Lχ LG : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} (hχ : HasFDerivAt χ Lχ x) (hG : HasFDerivAt G LG x) (i : Fin 2) : spaceGrad (fun (y : Homogenization.Vec 2) => Homogenization.vecDot (χ y) (G y)) x i = (gradMatrix χ x).mulVec (G x) i + ∑ j : Fin 2, χ x j * spaceGrad (fun (y : Homogenization.Vec 2) => G y j) x i

Product rule for the gradient of the corrector pairing χ · G.

def AVenhance.Infra.Section5.vecDotDerivativeAt {χ G : Homogenization.Vec 2 → Homogenization.Vec 2} (x : Homogenization.Vec 2) (Lχ LG : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2) : Homogenization.Vec 2 →L[ℝ] ℝ

The Fréchet derivative of the scalar pairing χ · G, expressed using the component projections of the two vector derivatives.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Section5.hasFDerivAt_vecDot {χ G : Homogenization.Vec 2 → Homogenization.Vec 2} {x : Homogenization.Vec 2} {Lχ LG : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} (hχ : HasFDerivAt χ Lχ x) (hG : HasFDerivAt G LG x) : HasFDerivAt (fun (y : Homogenization.Vec 2) => Homogenization.vecDot (χ y) (G y)) (vecDotDerivativeAt x Lχ LG) x

Product rule for the finite-dimensional vector pairing.

theorem AVenhance.Infra.Section5.G_eq_flowGrad_mulVec {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (T : ℝ → Homogenization.Vec 2 → ℝ) (l : ℤ) (t : ℝ) (x : Homogenization.Vec 2) {LT : Homogenization.Vec 2 →L[ℝ] ℝ} {LX : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} (hT : HasFDerivAt (T t) LT x) (hX : HasFDerivAt (I.xFlow hΦ m l t) LX (I.xFlowInv hΦ m l t x)) (hinv : I.xFlow hΦ m l t (I.xFlowInv hΦ m l t x) = x) : G I hΦ m T l t x = (I.flowGrad hΦ m l t x).mulVec (spaceGrad (T t) x)

The defining flow-pulled gradient obeys the source chain rule G_l = (∇X_l ∘ X_l⁻¹) ∇T.