Step 1: pointwise bounds on ∂^α ∂_i T(t) from the L²_x bounds

H² ⊂ L∞ (abs_le_sobolevConst_mul) applied to u = Dⁿ⁺¹T(·)(w, e_i) converts the all-orders L²_x estimate on T into a pointwise bound on the order-n derivatives of ∂_i T.

theorem AVenhance.Infra.Section5.AnalyticBridge.factorial_mul_pow_succ_le (n : ℕ) {a : ℝ} (ha : 1 ≤ a) : ↑(n + 1).factorial * a ^ (n + 1) ≤ ↑(n + 3).factorial * a ^ (n + 3)

(n+1)! a^{n+1} ≤ (n+3)! a^{n+3} for a ≥ 1.

theorem AVenhance.Infra.Section5.AnalyticBridge.sobolev_sum_le {s₁ s₂ s₃ M : ℝ} (h₁ : s₁ ≤ M) (h₂ : s₂ ≤ M) (h₃ : s₃ ≤ M) : s₁ + s₂ + s₃ ≤ 3 * M

Sum of the three Sobolev terms, in abstract-real form.

theorem AVenhance.Infra.Section5.AnalyticBridge.SupBound.basisVec_snoc {n : ℕ} (w : Fin n → Fin 2) (v : Fin 2) : (fun (j : Fin (n + 1)) => Homogenization.basisVec (Fin.snoc w v j)) = Fin.snoc (fun (j : Fin n) => Homogenization.basisVec (w j)) (Homogenization.basisVec v)

theorem AVenhance.Infra.Section5.AnalyticBridge.SupBound.basisVec_cons {n : ℕ} (w : Fin n → Fin 2) (v : Fin 2) : (fun (j : Fin (n + 1)) => Homogenization.basisVec (Fin.cons v w j)) = Fin.cons (Homogenization.basisVec v) fun (j : Fin n) => Homogenization.basisVec (w j)

theorem AVenhance.Infra.Section5.AnalyticBridge.SupBound.test_smooth_periodic {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : IsZ2Periodic f) (m : ℕ) (w : Fin m → Fin 2) : (ContDiff ℝ ↑⊤ fun (y : Homogenization.Vec 2) => (iteratedFDeriv ℝ m f y) fun (j : Fin m) => Homogenization.basisVec (w j)) ∧ IsZ2Periodic fun (y : Homogenization.Vec 2) => (iteratedFDeriv ℝ m f y) fun (j : Fin m) => Homogenization.basisVec (w j)

The test function y ↦ Dᵐ f(y)(e_w) is smooth and periodic.

theorem AVenhance.Infra.Section5.AnalyticBridge.SupBound.sqrt_l2NormSq_second_le {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) {B a : ℝ} (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) (m : ℕ) (w : Fin m → Fin 2) (k : Fin 2) : √(l2NormSq fun (y : Homogenization.Vec 2) => (iteratedFDeriv ℝ 2 (fun (z : Homogenization.Vec 2) => (iteratedFDeriv ℝ m f z) fun (j : Fin m) => Homogenization.basisVec (w j)) y) fun (x : Fin 2) => Homogenization.basisVec k) ≤ B * ↑(m + 2).factorial * a ^ (m + 2)

The L²_x bound for the second pure derivative of the test function.

theorem AVenhance.Infra.Section5.AnalyticBridge.abs_iteratedFDeriv_fderiv_le {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hp : IsZ2Periodic f) {B a : ℝ} (hB : 0 ≤ B) (ha : 1 ≤ a) (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) (n : ℕ) (w : Fin n → Fin 2) (v : Fin 2) (x : Homogenization.Vec 2) : |(iteratedFDeriv ℝ n (fun (y : Homogenization.Vec 2) => (fderiv ℝ f y) (Homogenization.basisVec v)) x) fun (j : Fin n) => Homogenization.basisVec (w j)| ≤ 3 * sobolevConst * (B * ↑(n + 3).factorial * a ^ (n + 3))

Pointwise bound on the order-n derivatives of ∂_v f, from the L²_x bounds on f.