Coarse-graining support: Support.CoarseGraining.BlockResponse.Perturbation.VolumeAverage

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

BlockResponse perturbation -- volume-averaged identities

Volume-average versions of the pair-half scalar decomposition (with and without the finite-measure assumption), the first-variation pair-half identity, and the statePairing = quarter scalarVariationEnergy equality.

theorem HCPolySupport.volumeAverage_blockResponseIntegrand_pair_half_eq_scalarResponse_sum {d : ℕ} {U : Set (Vec d)} (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : MeasurableSet U) (hEll : IsEllipticFieldOn lam Lam U a) (p pStar q qStar : Vec d) (u : AHarmonicFunction a U) (v : AHarmonicFunction (adjointCoeffField a) U) : volumeAverage U (blockResponseIntegrand a (p, q) (qStar, pStar) (blockResponsePairHalfState a u v)) = 1 / 2 * volumeAverage U (scalarResponseIntegrand U a (p - pStar) (qStar - q) u) + 1 / 2 * volumeAverage U (scalarResponseIntegrand U (adjointCoeffField a) (pStar + p) (qStar + q) v)

theorem HCPolySupport.blockFirstVariationIntegrand_pair_half_eq_scalarFirstVariation_sum_on_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (p pStar q qStar : Vec d) (u w : AHarmonicFunction a U) (v z : AHarmonicFunction (adjointCoeffField a) U) (x : Vec d) : x ∈ U → blockFirstVariationIntegrand a (p, q) (qStar, pStar) (blockResponsePairHalfState a u v) (blockResponsePairHalfState a w z) x = 1 / 2 * scalarFirstVariationIntegrand U a (p - pStar) (qStar - q) u w x + 1 / 2 * scalarFirstVariationIntegrand U (adjointCoeffField a) (pStar + p) (qStar + q) v z x

The block first variation around a primal/adjoint half-pair splits into the corresponding primal and adjoint scalar first variations.

theorem HCPolySupport.volumeAverage_blockFirstVariationIntegrand_pair_half_eq_scalarFirstVariation_sum {d : ℕ} {U : Set (Vec d)} (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : MeasurableSet U) (hEll : IsEllipticFieldOn lam Lam U a) (p pStar q qStar : Vec d) (u w : AHarmonicFunction a U) (v z : AHarmonicFunction (adjointCoeffField a) U) : volumeAverage U (blockFirstVariationIntegrand a (p, q) (qStar, pStar) (blockResponsePairHalfState a u v) (blockResponsePairHalfState a w z)) = 1 / 2 * volumeAverage U (scalarFirstVariationIntegrand U a (p - pStar) (qStar - q) u w) + 1 / 2 * volumeAverage U (scalarFirstVariationIntegrand U (adjointCoeffField a) (pStar + p) (qStar + q) v z)

Averaged form of blockFirstVariationIntegrand_pair_half_eq_scalarFirstVariation_sum_on_of_isEllipticFieldOn.

theorem HCPolySupport.statePairing_blockResponsePairHalfState_eq_quarter_scalarVariationEnergy_sub {d : ℕ} {U : Set (Vec d)} (a : CoeffField d) (u : AHarmonicFunction a U) (v : AHarmonicFunction (adjointCoeffField a) U) : (fun (x : Vec d) => vecDot ((blockResponsePairHalfState a u v).potential x) ((blockResponsePairHalfState a u v).flux x)) = fun (x : Vec d) => 1 / 4 * scalarVariationEnergyIntegrand a u x - 1 / 4 * scalarVariationEnergyIntegrand (adjointCoeffField a) v x

The pointwise state pairing of a primal/adjoint half-pair is the quarter-difference of the primal and adjoint scalar energies.

theorem HCPolySupport.volumeAverage_statePairing_blockResponsePairHalfState_eq_quarter_scalarVariationEnergy_sub {d : ℕ} {U : Set (Vec d)} (a : CoeffField d) {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hEll : IsEllipticFieldOn lam Lam U a) (u : AHarmonicFunction a U) (v : AHarmonicFunction (adjointCoeffField a) U) : (volumeAverage U fun (x : Vec d) => vecDot ((blockResponsePairHalfState a u v).potential x) ((blockResponsePairHalfState a u v).flux x)) = 1 / 4 * volumeAverage U (scalarVariationEnergyIntegrand a u) - 1 / 4 * volumeAverage U (scalarVariationEnergyIntegrand (adjointCoeffField a) v)

Averaged state-pairing form for a primal/adjoint half-pair.