Positive-order temperature jets and arbitrary amplitude; no zeroth-order temperature supremum. Existing Sobolev, product and composition engines are reused.

theorem AVenhance.Infra.Section5.RelativeError.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), 0 < n → √(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 : AnalyticBridge.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 * AnalyticBridge.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.