Source-scale estimate for normie2, conditional on the Section 3/4 space-time L² estimate for its vector flux.

theorem AVenhance.Infra.Section5.timeHMinusOneNorm_normie2_sourceScale {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm C : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (hF : ∀ t ∈ Set.Ioo 0 1, ContDiff ℝ (↑⊤) (normie2Flux I hΦ m κm T t)) (hper : ∀ t ∈ Set.Ioo 0 1, IsZ2Periodic (normie2Flux I hΦ m κm T t)) (hsource : (∫⁻ (t : ℝ) in Set.Ioo 0 1, ENNReal.ofReal √(gradNormSq (normie2Flux I hΦ m κm T t)) ^ 2) ^ (1 / 2) ≤ ENNReal.ofReal (section5SourceScale β I.Λ m κm C θ₀)) : (timeHMinusOneNorm fun (t : ℝ) => normie2 I hΦ m κm T t) ≤ ENNReal.ofReal (section5SourceScale β I.Λ m κm C θ₀)

Conditional source-scale estimate for normie2 from its flux bound.