Coarse-graining support:

Support.CoarseGraining.BlockResponse.Perturbation.BlockEnergyFirstVariation

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

BlockResponse perturbation -- blockEnergyAverage and scalarFirstVariation

blockEnergyAverage_blockResponsePairHalfState = quarter scalarVariationEnergySum under IsEllipticFieldOn, together with the three scalarFirstVariation-zero theorems (zero_right, neg_left_zero, neg_left_right) for ae-equal pair-half states under IsBlockMuAdmissible.

theorem HCPolySupport.blockEnergyAverage_blockResponseHalfState_eq_quarter_scalarVariationEnergySum {d : ℕ} {U : Set (Vec d)} (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : MeasurableSet U) (hEll : IsEllipticFieldOn lam Lam U a) (u : AHarmonicFunction a U) (v : AHarmonicFunction (adjointCoeffField a) U) : blockEnergyAverage U a (blockResponsePairHalfState a u v) = 1 / 4 * volumeAverage U (scalarVariationEnergyIntegrand a u) + 1 / 4 * volumeAverage U (scalarVariationEnergyIntegrand (adjointCoeffField a) v)

The half-pair witness has block energy equal to one quarter of the sum of the primal and adjoint scalar variation energies.

theorem HCPolySupport.scalarFirstVariation_zero_right_of_ae_eq_blockResponsePairHalfState_of_isBlockMuAdmissible {d : ℕ} {U : Set (Vec d)} (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : MeasurableSet U) (hEll : IsEllipticFieldOn lam Lam U a) (q : Vec d) (u : AHarmonicFunction a U) (v : AHarmonicFunction (adjointCoeffField a) U) (X : BlockState d) (hEq : (fun (x : Vec d) => (blockResponsePairHalfState a u v).eval x) =ᵐ[volumeMeasureOn U] X.eval) (hAdm : IsBlockMuAdmissible U (0, q) X) (w : AHarmonicFunction a U) : volumeAverage U (scalarFirstVariationIntegrand U a 0 q u w) = 0

Decoupling lemma for the pure-flux slice.

If a recovered \mu-admissible state at coarse data (0,q) is a.e. a primal/adjoint half-pair, then the primal member of the half-pair satisfies the scalar Euler-Lagrange identity for ResponseJ U 0 q a.

theorem HCPolySupport.scalarFirstVariation_neg_left_zero_of_ae_eq_blockResponsePairHalfState_of_isBlockMuAdmissible {d : ℕ} {U : Set (Vec d)} (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : MeasurableSet U) (hEll : IsEllipticFieldOn lam Lam U a) (p : Vec d) (u : AHarmonicFunction a U) (v : AHarmonicFunction (adjointCoeffField a) U) (X : BlockState d) (hEq : (fun (x : Vec d) => (blockResponsePairHalfState a u v).eval x) =ᵐ[volumeMeasureOn U] X.eval) (hAdm : IsBlockMuAdmissible U (p, 0) X) (w : AHarmonicFunction a U) : volumeAverage U (scalarFirstVariationIntegrand U a (-p) 0 u w) = 0

Decoupling lemma for the pure-gradient slice.

The sign is forced by the block convention: a recovered \mu-admissible state at coarse data (p,0) yields the primal scalar Euler-Lagrange identity for ResponseJ U (-p) 0 a. The final energy statement removes this sign using the quadratic homogeneity of ResponseJ.

theorem HCPolySupport.scalarFirstVariation_neg_left_right_of_ae_eq_blockResponsePairHalfState_of_isBlockMuAdmissible {d : ℕ} {U : Set (Vec d)} (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : MeasurableSet U) (hEll : IsEllipticFieldOn lam Lam U a) (p q : Vec d) (u : AHarmonicFunction a U) (v : AHarmonicFunction (adjointCoeffField a) U) (X : BlockState d) (hEq : (fun (x : Vec d) => (blockResponsePairHalfState a u v).eval x) =ᵐ[volumeMeasureOn U] X.eval) (hAdm : IsBlockMuAdmissible U (p, q) X) (w : AHarmonicFunction a U) : volumeAverage U (scalarFirstVariationIntegrand U a (-p) q u w) = 0

Decoupling lemma for arbitrary block data.

The sign in the primal scalar first variation is dictated by the block convention: a recovered \mu-admissible state at coarse datum (p,q) yields the Euler-Lagrange identity for ResponseJ U (-p) q a.