L²_{t,x} transfer for the cutoff1 source contract

From a slicewise bound ‖F(t)‖²_{L²} ≤ c² ‖∇T(t)‖²_{L²} (t ∈ (0,1)) to the left side of Cutoff1SourceContract, in terms of the space-time gradient norm of T.

theorem AVenhance.Infra.Section5.Contracts.TermSourcesCutoffL2.sb_gradNormSq_nonneg (F : Homogenization.Vec 2 → Homogenization.Vec 2) : 0 ≤ gradNormSq F

theorem AVenhance.Infra.Section5.Contracts.sb_l2_timeL2_le {F T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) {c : ℝ} (hc : 0 ≤ c) (h : ∀ t ∈ Set.Ioo 0 1, l2NormSq (F t) ≤ c ^ 2 * gradNormSq fun (x : Homogenization.Vec 2) => spaceGrad (T t) x) : (∫⁻ (t : ℝ) in Set.Ioo 0 1, ENNReal.ofReal ((2 * Real.pi)⁻¹ * √(l2NormSq (F t))) ^ 2) ^ (1 / 2) ≤ ENNReal.ofReal ((2 * Real.pi)⁻¹ * c) * ENNReal.ofReal √(spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (T t) x)