Step 4b: pointwise derivative bounds for (∂_i T ∂_j T) ∘ X

Appendix B proposition 10528 (compositionEstimate10528) applied to the product h = ∂_iT ∂_jT (⟦h⟧_{n,2a} ≤ C_f) and the flow slice X (⟦X⟧_{j,2A/e} ≤ K e) gives ⟦h ∘ X⟧_{n,R'} ≤ C_f; the coordinate derivatives are then bounded pointwise.

theorem AVenhance.Infra.Section5.AnalyticBridge.orderedPartial_comp_le {K : ℝ} (hK1 : 1 ≤ K) (hK : ∀ (n : ℕ), (↑n + 3) ^ 5 ≤ K * 2 ^ n) {A ρ e N : ℝ} (hA : 1 ≤ A) (hρ : 0 < ρ) (hρe : ρ ≤ e) (he1 : e ≤ 1) (hN : 0 < N) {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : IsZ2Periodic f) (hreg : ∀ (n : ℕ) (i : Fin n → Fin 2), √(l2NormSq fun (x : Homogenization.Vec 2) => (iteratedFDeriv ℝ n f x) fun (j : Fin n) => Homogenization.basisVec (i j)) ≤ A * N * ↑n.factorial * (A / ρ) ^ n) {X : Homogenization.Vec 2 → Homogenization.Vec 2} (hX : FlowForErgodicBound A e X) (hXs : ContDiff ℝ (↑⊤) X) (i j : Fin 2) (n : ℕ) (x : Homogenization.Vec 2) (I : Fin n → Fin 2) : ‖FaaDiBruno.orderedPartial n ((fun (y : Homogenization.Vec 2) => (fderiv ℝ f y) (Homogenization.basisVec i) * (fderiv ℝ f y) (Homogenization.basisVec j)) ∘ X) x I‖ ≤ 4 * (3 * sobolevConst * (A * N) * K * (A / ρ) ^ 3) ^ 2 * ↑n.factorial * (2 * A / e * (1 + ↑2 * (K * e) * (2 * (A / ρ)))) ^ n

Pointwise bound on the ordered partials of (∂_i f ∂_j f) ∘ X.