Steps 2 and 3: analytic snorm bounds for ∂_i T and ∂_i T ∂_j T

From the pointwise bounds of SupBound we obtain ⟦∂_i T⟧_{n,2a} ≤ C_h for every n, and then ⟦∂_i T ∂_j T⟧_{n,2a} ≤ 4 C_h² by the Appendix B product estimate.

theorem AVenhance.Infra.Section5.AnalyticBridge.exists_poly_le_two_pow : ∃ (K : ℝ), 1 ≤ K ∧ ∀ (n : ℕ), (↑n + 3) ^ 5 ≤ K * 2 ^ n

An absolute constant dominating (n+3)⁵ / 2ⁿ.

theorem AVenhance.Infra.Section5.AnalyticBridge.factorial_mul_sq_le {K : ℝ} (hK : ∀ (n : ℕ), (↑n + 3) ^ 5 ≤ K * 2 ^ n) (n : ℕ) : ↑(n + 3).factorial * (↑n + 1) ^ 2 ≤ K * 2 ^ n * ↑n.factorial

(n+3)! (n+1)² ≤ K 2ⁿ n!.

theorem AVenhance.Infra.Section5.AnalyticBridge.grad_bound_le_radius_form {K : ℝ} (hK : ∀ (n : ℕ), (↑n + 3) ^ 5 ≤ K * 2 ^ n) {c a : ℝ} (hc : 0 ≤ c) (ha : 0 < a) (n : ℕ) : c * (↑(n + 3).factorial * a ^ (n + 3)) ≤ c * K * a ^ 3 * (2 * a) ^ n * ↑n.factorial / (↑n + 1) ^ 2

Abstract-real core of step 2.

theorem AVenhance.Infra.Section5.AnalyticBridge.contDiff_fderiv_apply_basis {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (v : Fin 2) : ContDiff ℝ ↑⊤ fun (y : Homogenization.Vec 2) => (fderiv ℝ f y) (Homogenization.basisVec v)

Smoothness of the coordinate derivative ∂_v f.

theorem AVenhance.Infra.Section5.AnalyticBridge.snorm_fderiv_le {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : IsZ2Periodic f) {B a K : ℝ} (hB : 0 ≤ B) (ha : 1 ≤ a) (hK : ∀ (n : ℕ), (↑n + 3) ^ 5 ≤ K * 2 ^ n) (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)) ≤ B * ↑n.factorial * a ^ n) (v : Fin 2) (n : ℕ) : FaaDiBruno.snorm (fun (y : Homogenization.Vec 2) => (fderiv ℝ f y) (Homogenization.basisVec v)) n (2 * a) ≤ ENNReal.ofReal (3 * sobolevConst * B * K * a ^ 3)

Step 2: ⟦∂_v f⟧_{n,2a} ≤ 3 sc K B a³ for every order n.

theorem AVenhance.Infra.Section5.AnalyticBridge.snormMax_fderiv_le {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : IsZ2Periodic f) {B a K : ℝ} (hB : 0 ≤ B) (ha : 1 ≤ a) (hK : ∀ (n : ℕ), (↑n + 3) ^ 5 ≤ K * 2 ^ n) (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)) ≤ B * ↑n.factorial * a ^ n) (v : Fin 2) (n : ℕ) : FaaDiBruno.snormMax (fun (y : Homogenization.Vec 2) => (fderiv ℝ f y) (Homogenization.basisVec v)) n (2 * a) ≤ ENNReal.ofReal (3 * sobolevConst * B * K * a ^ 3)

snormMax of ∂_v f up to order n.

theorem AVenhance.Infra.Section5.AnalyticBridge.snorm_fderiv_mul_le {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : IsZ2Periodic f) {B a K : ℝ} (hB : 0 ≤ B) (ha : 1 ≤ a) (hK : ∀ (n : ℕ), (↑n + 3) ^ 5 ≤ K * 2 ^ n) (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)) ≤ B * ↑n.factorial * a ^ n) (i j : Fin 2) (n : ℕ) : FaaDiBruno.snorm (fun (y : Homogenization.Vec 2) => (fderiv ℝ f y) (Homogenization.basisVec i) * (fderiv ℝ f y) (Homogenization.basisVec j)) n (2 * a) ≤ ENNReal.ofReal (4 * (3 * sobolevConst * B * K * a ^ 3) ^ 2)

Step 3: ⟦∂_i f ∂_j f⟧_{n,2a} ≤ 4 C_h².