The pointwise Section 3 flux-energy estimate in the finite-support form used by the Section 5 consumers.

noncomputable def AVenhance.Infra.Section3.lFluxToEnergyConstant (C₀ : ℝ) : ℝ

Uniform coefficient in the flux-energy estimate when the cutoff derivative constants are bounded by C₀.

Equations

• AVenhance.Infra.Section3.lFluxToEnergyConstant C₀ = (C₀ + C₀) / (4 * Real.pi ^ 2) * (1 / 2) + C₀ ^ 2 / (16 * Real.pi ^ 4)

theorem AVenhance.Infra.Section3.l_flux_to_energy {β C₀ : ℝ} (I : Ingredients β) (hCz : I.Czeta ≤ C₀) (hCh : I.Chat ≤ C₀) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (hκ : 0 < κ) (t : ℝ) (hcondition : epsilon β I.Λ m ^ 2 ≤ κ * tau β I.Λ m / 2) : (∀ (x : Homogenization.Vec 2), have S := ⋯.toFinset; ∑ k ∈ S, ∑ l ∈ S, (I.xiMK m (↑k) t * I.xiMK m (↑l) t) • (κ • 1 + (gradMatrix (I.chiMK κ m (↑k) t) x).transpose * gradMatrix (I.chiMK κ m (↑l) t) x) = κ • 1 + ∑ k ∈ S, I.xiMK m (↑k) t ^ 2 • ((gradMatrix (I.chiMK κ m (↑k) t) x).transpose * gradMatrix (I.chiMK κ m (↑k) t) x)) ∧ have S := ⋯.toFinset; ∀ (i j : Fin 2), |(I.flux κ m t - movingEnergyReducedSourceMatrix I κ m t S) i j| ≤ lFluxToEnergyConstant C₀ * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ) * (epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m))

The source's full odd-mode energy double sum reduces to the finite cutoff support, and the flux differs entrywise from that reduced energy by the Section 3 scale error. The coefficient is independent of I among all ingredients satisfying the displayed common cutoff bound C₀.