Coarse-graining support: Support.Sobolev.Foundations.AffineAverage

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

theorem HCPolySupport.CorrectionFieldData.integral_pairing_affine_eq_volume_mul_vecDot {d : ℕ} {U : Set (Vec d)} (hU : IsSobolevRegularDomain U) (X : CorrectionFieldData U) (p q : Vec d) : ∫ (x : Vec d) in U, vecDot (p + X.potential x) (q + X.flux x) = (MeasureTheory.volume U).toReal * vecDot p q

theorem HCPolySupport.CorrectionFieldData.integral_potential_affine_eq_volume_smul {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (X : CorrectionFieldData U) (p : Vec d) : (fun (i : Fin d) => ∫ (x : Vec d) in U, (p + X.potential x) i) = (MeasureTheory.volume U).toReal • p

theorem HCPolySupport.CorrectionFieldData.integral_flux_affine_eq_volume_smul {d : ℕ} {U : Set (Vec d)} (hU : IsSobolevRegularDomain U) (X : CorrectionFieldData U) (q : Vec d) : (fun (i : Fin d) => ∫ (x : Vec d) in U, (q + X.flux x) i) = (MeasureTheory.volume U).toReal • q

theorem HCPolySupport.CorrectionFieldData.average_potential_affine {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hvol : (MeasureTheory.volume U).toReal ≠ 0) (X : CorrectionFieldData U) (p : Vec d) : (fun (i : Fin d) => integralAverage U fun (x : Vec d) => (p + X.potential x) i) = p

theorem HCPolySupport.CorrectionFieldData.average_flux_affine {d : ℕ} {U : Set (Vec d)} (hU : IsSobolevRegularDomain U) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (X : CorrectionFieldData U) (q : Vec d) : (fun (i : Fin d) => integralAverage U fun (x : Vec d) => (q + X.flux x) i) = q

theorem HCPolySupport.CorrectionFieldData.average_state_affine {d : ℕ} {U : Set (Vec d)} (hU : IsSobolevRegularDomain U) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (X : CorrectionFieldData U) (P : BlockVec d) : (fun (i : Fin d) => integralAverage U fun (x : Vec d) => (P.1 + X.potential x) i, fun (i : Fin d) => integralAverage U fun (x : Vec d) => (P.2 + X.flux x) i) = P