Slicewise L² bound of cutoff1

‖cutoff1(t)‖²_{L²(𝕋²)} ≤ P² ‖∇T(t)‖²_{L²(𝕋²)}, from the pointwise bound sb_cutoff1_abs_le (a Bochner integral dominated by an integrable function needs no integrability of the dominated function).

theorem AVenhance.Infra.Section5.Contracts.sb_l2NormSq_cutoff1_le {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) {κ : ℝ} (hκ : 0 ≤ κ) {T : ℝ → Homogenization.Vec 2 → ℝ} {t : ℝ} (hTt : ContDiff ℝ (↑⊤) (T t)) : l2NormSq (cutoff1 I hΦ m κ T t) ≤ (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)))) ^ 2 * gradNormSq fun (x : Homogenization.Vec 2) => spaceGrad (T t) x