Coarse-graining support: Support.CoarseGraining.BlockResponse.Equalities.Helpers

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

BlockResponse Equalities -- helpers and existence / volumeAverage

Private blockResponse_upper-add / upper-sub-flux equalities, the big exists_blockResponsePairHalfState_ae_eq_of_mem_responseSpace_of_lowerImage_isPotential theorem, and the matching volumeAverage_blockResponseIntegrand_eq_scalarResponse_sum theorem.

theorem HCPolySupport.exists_blockResponseHalfState_ae_eq_of_lowerImage_isPotential {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {X : BlockState d} {lam Lam : ℝ} (hU : MeasurableSet U) (hX : BlockResponseSpace a U X) (hLower : IsPotentialOn U fun (x : Vec d) => (blockMatVecMul (blockCoeffField a x) (X.eval x)).2) (hEll : IsEllipticFieldOn lam Lam U a) : ∃ (u : AHarmonicFunction a U) (v : AHarmonicFunction (adjointCoeffField a) U), (fun (x : Vec d) => (blockResponsePairHalfState a u v).eval x) =ᵐ[volumeMeasureOn U] X.eval

theorem HCPolySupport.exists_blockResponseHalfState_ae_eq_of_lowerImage_memVectorL2 {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {X : BlockState d} (hConv : IsOpenBoundedConvexDomain U) (hX : BlockResponseSpace a U X) (hLowerL2 : MemVectorL2 U fun (x : Vec d) => (blockMatVecMul (blockCoeffField a x) (X.eval x)).2) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) : ∃ (u : AHarmonicFunction a U) (v : AHarmonicFunction (adjointCoeffField a) U), (fun (x : Vec d) => (blockResponsePairHalfState a u v).eval x) =ᵐ[volumeMeasureOn U] X.eval

Preferred convex-domain reverse-inclusion wrapper for response states whose lower image is known to be L². This is the note-facing way to reconstruct the primal/adjoint harmonic half-pair from a block-response state without manually supplying a lower-image potential representative.

theorem HCPolySupport.exists_blockResponseHalfState_ae_eq_of_integrabilityData_of_ellipticField {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {X : BlockState d} (hConv : IsOpenBoundedConvexDomain U) (hX : BlockResponseSpace a U X) (hInt : BlockResponseIntegrabilityData U a X) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) : ∃ (u : AHarmonicFunction a U) (v : AHarmonicFunction (adjointCoeffField a) U), (fun (x : Vec d) => (blockResponsePairHalfState a u v).eval x) =ᵐ[volumeMeasureOn U] X.eval

Preferred convex-domain reverse-inclusion wrapper for integrable response states. Since BlockResponseIntegrabilityData supplies the flux L² control, this packages the lower-image promotion and half-pair reconstruction into one standalone theorem.

theorem HCPolySupport.volumeAverage_blockResponseIntegrand_eq_scalarResponse_sum {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {X : BlockState d} {lam Lam : ℝ} (hU : MeasurableSet U) (hX : BlockResponseSpace a U X) (hLower : IsPotentialOn U fun (x : Vec d) => (blockMatVecMul (blockCoeffField a x) (X.eval x)).2) (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) X) = 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)