Pointwise bound of cutoff1 (e.monster.est.3)

At fixed (t, x) at most three odd k have ξ'_{m,k}(t) ≠ 0; for each, ξ'_{m,k} is ≤ C_ξ/τ_m, the corrector χTilde_{m,k} is ≤ (4/3) τ_m e^{-π²κ τ_m/(3ε_m²)} · 2π a_m ε_m (it vanishes before (k - 2/3) τ_m and decays after (k + 3/4) τ_m), and |G_{l_k}| ≤ 4 |∇T|.

theorem AVenhance.Infra.Section5.Contracts.sb_chiTilde_abs_le {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 ≤ κ) (k : ℤ) {t : ℝ} (hsupp : (↑k + 3 / 4) * tau β I.Λ m ≤ t ∨ t ≤ (↑k - 3 / 4) * tau β I.Λ m) (x : Homogenization.Vec 2) (j : Fin 2) : |I.chiTilde hΦ m κ k t x j| ≤ 4 / 3 * tau β I.Λ m * Real.exp (-(4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2 * (tau β I.Λ m / 12))) * (2 * Real.pi * a β I.Λ m * epsilon β I.Λ m)

The corrector χTilde_{m,k}(t) is small on the support of ξ'_{m,k}, entrywise.

theorem AVenhance.Infra.Section5.Contracts.sb_G_abs_le {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) (k : ℤ) {t : ℝ} (hξ : I.xiMK m k t ≠ 0) {T : ℝ → Homogenization.Vec 2 → ℝ} (hTt : ContDiff ℝ (↑⊤) (T t)) (x : Homogenization.Vec 2) (j : Fin 2) : |G I hΦ m T (lIdx β I.Λ m k) t x j| ≤ 4 * √(Homogenization.vecNormSq (spaceGrad (T t) x))

|G_l| ≤ 4 |∇T| when the flow is ε^{2δ}-close to the identity.

theorem AVenhance.Infra.Section5.Contracts.sb_xiMK_ne_zero_abs_le {β : ℝ} (I : Ingredients β) (m : ℕ) {k : ℤ} {t : ℝ} (hne : I.xiMK m k t ≠ 0) : |t - ↑k * tau β I.Λ m| ≤ 5 / 4 * tau β I.Λ m

Every odd k with ξ_{m,k}(t) ≠ 0 has |t - kτ_m| ≤ 5/4 τ_m.

theorem AVenhance.Infra.Section5.Contracts.sb_odd_support_card {β : ℝ} (I : Ingredients β) (m : ℕ) (t : ℝ) : ∃ (s : Finset { k : ℤ // Odd k }), s.card ≤ 3 ∧ ∀ (q : { k : ℤ // Odd k }), I.xiMK m (↑q) t ≠ 0 → q ∈ s

At most three odd indices have ξ_{m,k}(t) ≠ 0: they lie in a finite set of card ≤ 3.

theorem AVenhance.Infra.Section5.Contracts.sb_cutoff1_abs_le {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) {κ : ℝ} (hκ : 0 ≤ κ) {T : ℝ → Homogenization.Vec 2 → ℝ} {t : ℝ} (hTt : ContDiff ℝ (↑⊤) (T t)) (x : Homogenization.Vec 2) : |cutoff1 I hΦ m κ T t x| ≤ 64 * Real.pi * I.Cxi * (a β I.Λ m * epsilon β I.Λ m) * Real.exp (-(4 * Real.pi ^ 2 * κ / epsilon β I.Λ m ^ 2 * (tau β I.Λ m / 12))) * √(Homogenization.vecNormSq (spaceGrad (T t) x))

Pointwise bound of cutoff1.