Pointwise bounds for the fluxes and slow factors of twistie4, twistie5

The entrywise bounds are in TermCenteredFluxEntries, the real-algebra steps in TermCenteredFluxAlg; absolute constants: c = 64, c₀ = 28 * 2^16, c₁ = 7.

theorem AVenhance.Infra.Section5.Contracts.sd_flux_bound {β : ℝ} : ∃ (c : ℝ), 0 ≤ c ∧ ∀ (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ}, 2 ≤ m → ∀ {κm : ℝ}, 0 < κm → ∀ (T : ℝ → Homogenization.Vec 2 → ℝ) {t : ℝ}, ContDiff ℝ (↑⊤) (T t) → ∀ (x : Homogenization.Vec 2), Homogenization.vecNormSq (twistie4Flux I hΦ m κm T t x) ≤ (c * (epsilon β I.Λ (m - 1) ^ (2 * delta β) * (a β I.Λ m * epsilon β I.Λ m ^ 2))) ^ 2 * Homogenization.vecNormSq (spaceGrad (T t) x) ∧ Homogenization.vecNormSq (twistie5Flux I hΦ m κm T t x) ≤ (c * (epsilon β I.Λ (m - 1) ^ (2 * delta β) * (a β I.Λ m * epsilon β I.Λ m ^ 2))) ^ 2 * Homogenization.vecNormSq (spaceGrad (T t) x)

Pointwise flux bound (source e.monster.est.8a, e.monster.est.9a): with the corrector amplitude a_m ε_m², the fluxes Σ ξ_k D_k G_k, Σ ξ_k E_k G_k are bounded by c ε_{m-1}^{2δ} a_m ε_m² |∇T| (c an absolute constant), for t arbitrary and κm > 0. This holds for all x, not only on a support, since the flux is a convex combination over the supports of ξ_{m,k}.

theorem AVenhance.Infra.Section5.Contracts.sd_slow_pointwise {β : ℝ} : ∃ (c₀ : ℝ) (c₁ : ℝ), 0 ≤ c₀ ∧ 0 ≤ c₁ ∧ ∀ (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ}, 2 ≤ m → ∀ {κm : ℝ}, 0 ≤ κm → ∀ (T : ℝ → Homogenization.Vec 2 → ℝ) {t : ℝ}, ContDiff ℝ (↑⊤) (T t) → ∀ (k : ℤ) (a j : Fin 2) (x : Homogenization.Vec 2), section5SlowChoice2 I hΦ m κm T k t a j x ^ 2 ≤ (c₀ * κm * epsilon β I.Λ (m - 1) ^ (2 * delta β) * (epsilon β I.Λ (m - 1))⁻¹) ^ 2 * Homogenization.vecNormSq (spaceGrad (T t) x) + (c₁ * κm * epsilon β I.Λ (m - 1) ^ (2 * delta β)) ^ 2 * (Homogenization.vecNormSq (spaceGrad (Section4.iterateSpatialWord [0] (T t)) x) + Homogenization.vecNormSq (spaceGrad (Section4.iterateSpatialWord [1] (T t)) x)) ∧ section5SlowChoice3 I hΦ m T k t a j x ^ 2 ≤ (c₀ * epsilon β I.Λ (m - 1) ^ (2 * delta β) * (epsilon β I.Λ (m - 1))⁻¹) ^ 2 * Homogenization.vecNormSq (spaceGrad (T t) x) + (c₁ * epsilon β I.Λ (m - 1) ^ (2 * delta β)) ^ 2 * (Homogenization.vecNormSq (spaceGrad (Section4.iterateSpatialWord [0] (T t)) x) + Homogenization.vecNormSq (spaceGrad (Section4.iterateSpatialWord [1] (T t)) x))

Pointwise bounds of the slow factors (e.fg.choice.2, e.fg.choice.3): with ε = ε_{m-1}, |f|² ≲ (κ ε^{2δ})² (ε⁻² |∇T|² + |∇∂_0T|² + |∇∂_1T|²) (choice 2) and without κ (choice 3). Uses |∇X^{-1} - I| ≤ ε^{2δ}, |∇X∘X⁻¹ - I| ≤ ε^{2δ}, |∂²X| ≤ 2^{16} ε⁻¹ on supp ξ_{m,k} (and ξ_{m,k} = 0 elsewhere).