Coarse-graining support: Support.Book.Ch03.Theorems.Duality

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Section 3.3.1: Duality estimate from flux defect to solution comparison

This file freezes the public contract for l.duality.from.flux.defect.deterministic.theory.

structure HCPolySupport.Book.Ch03.FluxDefectDualityTheory (d : ℕ) [NeZero d] : Prop

Public two-exponent replacement package for the deterministic duality estimate. This is the proved replacement surface for the false same-exponent route: the comparison fields are measured at exponent s, while the localized flux defect is measured at an independent exponent t < s / 2.

• exists_constant : ∃ (C : ℝ), 0 < C ∧ ∀ {Q : TriadicCube d} {a : CoeffFamily d} {a0 : ConstantCoeffMatrix d} {s t : ℝ} {j : ℕ}, IsPositiveScalarMatrix a0.matrix → ∀ (w : HomogenizationComparisonDatum Q a a0), 0 < s → 0 < t → t < s / 2 → s < 1 → homogenizationComparisonNegativeBesovLHS Q a a0 s w.u w.v ≤ dualityFromFluxDefectExponentLossRHS C Q a a0 s t j w.u

theorem HCPolySupport.Book.Ch03.fluxDefectDualityTheory (d : ℕ) [NeZero d] : FluxDefectDualityTheory d

Public two-exponent duality package with all currently formalized analytic inputs discharged.