TinyHMinusSourceContract producer: scalar bookkeeping

The L²_{t,x} energies of the word gradients of the last increment are controlled by VIncrementContract at the index N*; this file turns that contract into the explicit bound √κ_{m-1} √Q_w ≤ G and proves the corrector size |χTilde| ≤ K.

theorem AVenhance.Infra.Section5.Contracts.sc_gamma_le_one {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : gamma β ≤ 1

theorem AVenhance.Infra.Section5.Contracts.sc_length_le_two_of_mem {w : List (Fin 2)} (hw : w ∈ scWords2) : w.length ≤ 2

theorem AVenhance.Infra.Section5.Contracts.sc_Q_le {β : ℝ} (I : Ingredients β) (m : ℕ) {κprev : ℝ} (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) {Cs Rθ B : ℝ} (hCs : 0 ≤ Cs) (hB : 0 ≤ B) (hRθ : epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) ≤ Rθ) (hV : Integration.VIncrementContract I m κprev T Cs Rθ B) {w : List (Fin 2)} (hw : w ∈ scWords2) : √κprev * √(spaceTimeGradNormSq (scWordGrad (Section4.iterateIncrement T (Nstar β)) w)) ≤ B * (Cs ^ 3 * epsilon β I.Λ (m - 1) ^ (2 * delta β)) ^ (↑(Nstar β) / 2) * ↑(2 * Nstar β + 2).factorial * (max 1 Cs * epsilon β I.Λ (m - 1) ^ (-(1 + gamma β / 2))) ^ 2

The contract VIncrementContract at the index N*, in explicit form.

theorem AVenhance.Infra.Section5.Contracts.sc_sqrt_sum_le {κp G c : ℝ} (hκp : 0 < κp) (hG : 0 ≤ G) (hc : 0 ≤ c) {Q : List (Fin 2) → ℝ} (hQ0 : ∀ (w : List (Fin 2)), 0 ≤ Q w) (hQ : ∀ w ∈ scWords2, √κp * √(Q w) ≤ G) : √(c * ∑ w ∈ scWords2, Q w) ≤ √(7 * c) * (G / √κp)

Summing the seven word energies.

theorem AVenhance.Infra.Section5.Contracts.sc_chiTilde_le {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm K : ℝ} (hKnn : 0 ≤ K) (hκm : 0 < κm) (hK4 : a β I.Λ m * epsilon β I.Λ m ^ 2 / κm ≤ K * epsilon β I.Λ m ^ (-gamma β)) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (j : Fin 2) : |I.chiTilde hΦ m κm k t x j| ≤ K

The corrector size |χTilde_{m,k}| ≤ K from the scale package.