Coarse-graining support: Support.Deterministic.CoarseFluxResponse.EnergyForm

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

theorem HCPolySupport.cubeAverageFluxDefect_energyForm_le_BlockResponseMax_mul_energyAverage {d : ℕ} [NeZero d] (R : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {lam Lam lam0 Lam0 : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet R) a) (ha0 : IsEllipticMatrix lam0 Lam0 a0) (w : AHarmonicFunction a (cubeSet R)) (v : ScalarCanonicalMaximizer (cubeSet R) (-matVecMul (symmPart a0)⁻¹ (cubeAverageVec R fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x) - matVecMul a0 (w.toH1.grad x))) (-matVecMul (matTranspose a0) (matVecMul (symmPart a0)⁻¹ (cubeAverageVec R fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x) - matVecMul a0 (w.toH1.grad x)))) a) : vecDot (cubeAverageVec R fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x) - matVecMul a0 (w.toH1.grad x)) (matVecMul (symmPart a0)⁻¹ (cubeAverageVec R fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x) - matVecMul a0 (w.toH1.grad x))) ≤ 4 * normalizedBlockResponseMax R a a0 * cubeAverage R (scalarVariationEnergyIntegrand a w)

Single-cube response-control theorem for the actual flux defect measured against the natural symmPart a0 energy form.

def HCPolySupport.DescendantScalarCanonicalFluxDefectData {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (defect : Vec d → Vec d) (energy : Vec d → ℝ) : Prop

Descendant-local Chapter-3 witness package for the actual flux defect relative to the constant matrix a0.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.DescendantScalarCanonicalFluxDefectAHarmonicData {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (u : AHarmonicFunction a (cubeSet Q)) : Prop

Descendant-local Chapter-3 witness package for the actual flux defect of a single global harmonic field on cubeSet Q. Each descendant comes with a local harmonic witness whose gradient agrees with the global field on that cube and which carries the needed scalar canonical maximizer.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.descendantScalarCanonicalFluxDefectData_of_aHarmonicData {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) (u : AHarmonicFunction a (cubeSet Q)) (hdesc : DescendantScalarCanonicalFluxDefectAHarmonicData Q a a0 u) : DescendantScalarCanonicalFluxDefectData Q a a0 (fun (x : Vec d) => matVecMul (a x) (u.toH1.grad x) - matVecMul a0 (u.toH1.grad x)) (scalarVariationEnergyIntegrand a u)

theorem HCPolySupport.descendantScalarCanonicalFluxDefectAHarmonicData_of_aHarmonicFunction {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (u : AHarmonicFunction a (cubeSet Q)) : DescendantScalarCanonicalFluxDefectAHarmonicData Q a a0 u

Every descendant cube of a global harmonic field on cubeSet Q carries the scalar canonical maximizer needed for the flux-defect argument.

theorem HCPolySupport.descendantScalarCanonicalFluxDefectData_of_aHarmonicFunction {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (a0 : Mat d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (u : AHarmonicFunction a (cubeSet Q)) : DescendantScalarCanonicalFluxDefectData Q a a0 (fun (x : Vec d) => matVecMul (a x) (u.toH1.grad x) - matVecMul a0 (u.toH1.grad x)) (scalarVariationEnergyIntegrand a u)

Direct descendant-local flux-defect witness package for one harmonic field on cubeSet Q, with no separate scalar-canonical assumptions.