Physical coefficient bound for the twisted initial corrector.

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_chiTilde_bound {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) (k : ℤ) (x : Homogenization.Vec 2) (i : Fin 2) : |I.chiTilde hΦ m κ k 0 x i| ≤ (4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2)⁻¹ * |2 * Real.pi * a β I.Λ m * epsilon β I.Λ m|

Twisting changes the evaluation point, but not the explicit coefficient bound.

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_corrector_explicit {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) {g : Homogenization.Vec 2 → ℝ} (hg : ContDiff ℝ (↑⊤) g) (T : ℝ → Homogenization.Vec 2 → ℝ) (hT0 : T 0 = g) : √(l2NormSq fun (x : Homogenization.Vec 2) => ∑' (k : ℤ), I.xiMK m k 0 * Homogenization.vecDot (I.chiTilde hΦ m κ k 0 x) (spaceGrad (fun (y : Homogenization.Vec 2) => T 0 (I.xFlow hΦ m (lIdx β I.Λ m k) 0 y)) (I.xFlowInv hΦ m (lIdx β I.Λ m k) 0 x))) ≤ 24 * ((4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2)⁻¹ * |2 * Real.pi * a β I.Λ m * epsilon β I.Λ m|) * √(gradNormSq (spaceGrad g))

Actual corrector estimate with cutoff and active-flow inputs discharged. Only the explicit coefficient and the positive derivative of the datum occur.