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

theorem AVenhance.Infra.Section5.timeHMinusOneNorm_twistie3_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 ℝ (↑⊤) (twistie3Flux I hΦ m κm T t)) (hper : ∀ t ∈ Set.Ioo 0 1, IsZ2Periodic (twistie3Flux I hΦ m κm T t)) (hsource : (∫⁻ (t : ℝ) in Set.Ioo 0 1, ENNReal.ofReal √(gradNormSq (twistie3Flux I hΦ m κm T t)) ^ 2) ^ (1 / 2) ≤ ENNReal.ofReal (section5SourceScale β I.Λ m κm C θ₀)) : (timeHMinusOneNorm fun (t : ℝ) => twistie3 I hΦ m κm T t) ≤ ENNReal.ofReal (section5SourceScale β I.Λ m κm C θ₀)

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