Coarse-graining support: Support.Book.Ch02.Theorems.CoarseGrainingEstimatesDefinitions

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

structure HCPolySupport.Book.Ch02.ResponseCoarseGrainingEstimatesTheory {d : ℕ} (U : Domain d) (a : CoeffOn U) : Prop

Public theorem package for l.cg.response.estimates.basic.definitions.

The canonical public theorem proving this package is responseCoarseGrainingEstimatesTheory in CoarseGrainingEstimates.lean.

• linear_response (p q : Vec d) (w : Solution U a) : |average U fun (x : Vec d) => vecDot p (matVecMul (a.toCoeffField x) (w.toH1.grad x)) - vecDot q (w.toH1.grad x)| ≤ √(variationEnergyValue U a w) * √(2 * responseJ U a p q)
• coarse_graining (p : Vec d) (w : Solution U a) : |vecDot p (matVecMul (aStarCoarse U a) (averageGradient U a w) - averageFlux U a w)| ≤ √2 * √(vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p)) * √(variationEnergyValue U a w)
• average_gradient_energy (w : Solution U a) : 1 / 2 * vecDot (averageGradient U a w) (matVecMul (sigmaStarCoarse U a) (averageGradient U a w)) ≤ 1 / 2 * variationEnergyValue U a w
• average_flux_energy (w : Solution U a) : 1 / 2 * vecDot (averageFlux U a w) (matVecMul (bCoarse U a)⁻¹ (averageFlux U a w)) ≤ 1 / 2 * variationEnergyValue U a w

theorem HCPolySupport.Book.Ch02.ResponseCoarseGrainingEstimatesTheory.ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (hTheory : ResponseCoarseGrainingEstimatesTheory U a) : ResponseCoarseGrainingEstimatesTheory U b

The coarse-graining estimates depend only on the public coefficient representative up to a.e. equality on the domain.

theorem HCPolySupport.Book.Ch02.ResponseCoarseGrainingEstimatesTheory.iff_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) : ResponseCoarseGrainingEstimatesTheory U a ↔ ResponseCoarseGrainingEstimatesTheory U b

A.e.-equivalent coefficient representatives satisfy the same coarse-graining estimate package.