Coarse-graining support: Support.Sobolev.PotentialSolenoidalL2OriginCubeBridge

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

theorem HCPolySupport.CorrectionFieldData.volume_cubeSet_originCube_lt_top_l2 {d : ℕ} (n : ℤ) : MeasureTheory.volume (cubeSet (originCube d n)) < ⊤

theorem HCPolySupport.CorrectionFieldData.volume_openCubeSet_originCube_lt_top_l2 {d : ℕ} (n : ℤ) : MeasureTheory.volume (openCubeSet (originCube d n)) < ⊤

instance HCPolySupport.CorrectionFieldData.instIsFiniteMeasureVolumeMeasureOnOpenCubeSetOriginCube {d : ℕ} {n : ℤ} : MeasureTheory.IsFiniteMeasure (volumeMeasureOn (openCubeSet (originCube d n)))

instance HCPolySupport.CorrectionFieldData.instIsFiniteMeasureVolumeMeasureOnCubeSetOriginCube {d : ℕ} {n : ℤ} : MeasureTheory.IsFiniteMeasure (volumeMeasureOn (cubeSet (originCube d n)))

theorem HCPolySupport.CorrectionFieldData.integrableOn_pairing_affine_openCubeSet_originCube {d : ℕ} {n : ℤ} (X : CorrectionFieldData (openCubeSet (originCube d n))) (p q : Vec d) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (p + X.potential x) (q + X.flux x)) (openCubeSet (originCube d n)) MeasureTheory.volume

On an open centered cube, the affine pairing attached to a zero-trace / zero-normal-trace L² correction is integrable.

theorem HCPolySupport.CorrectionFieldData.integral_pairing_affine_openCubeSet_originCube {d : ℕ} {n : ℤ} (X : CorrectionFieldData (openCubeSet (originCube d n))) (p q : Vec d) : ∫ (x : Vec d) in openCubeSet (originCube d n), vecDot (p + X.potential x) (q + X.flux x) = (MeasureTheory.volume (openCubeSet (originCube d n))).toReal * vecDot p q

On an open centered cube, the affine perturbation of a zero-trace / zero-normal-trace L² correction has pairing integral equal to the cube volume times the constant pairing.

theorem HCPolySupport.CorrectionFieldData.integral_potential_affine_openCubeSet_originCube {d : ℕ} {n : ℤ} (X : CorrectionFieldData (openCubeSet (originCube d n))) (p : Vec d) : (fun (i : Fin d) => ∫ (x : Vec d) in openCubeSet (originCube d n), (p + X.potential x) i) = (MeasureTheory.volume (openCubeSet (originCube d n))).toReal • p

On an open centered cube, the affine potential field p + correction has componentwise integral equal to the cube volume times p.

theorem HCPolySupport.CorrectionFieldData.integral_flux_affine_openCubeSet_originCube {d : ℕ} {n : ℤ} (X : CorrectionFieldData (openCubeSet (originCube d n))) (q : Vec d) : (fun (i : Fin d) => ∫ (x : Vec d) in openCubeSet (originCube d n), (q + X.flux x) i) = (MeasureTheory.volume (openCubeSet (originCube d n))).toReal • q

On an open centered cube, the affine flux field q + correction has componentwise integral equal to the cube volume times q.

theorem HCPolySupport.CorrectionFieldData.integrableOn_pairing_affine_cubeSet_originCube {d : ℕ} {n : ℤ} (X : CorrectionFieldData (cubeSet (originCube d n))) (p q : Vec d) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (p + X.potential x) (q + X.flux x)) (cubeSet (originCube d n)) MeasureTheory.volume

On the half-open centered cube, the affine pairing attached to a zero-trace / zero-normal-trace L² correction is integrable.

theorem HCPolySupport.CorrectionFieldData.integral_pairing_affine_cubeSet_originCube {d : ℕ} [NeZero d] {n : ℤ} (X : CorrectionFieldData (cubeSet (originCube d n))) (p q : Vec d) : ∫ (x : Vec d) in cubeSet (originCube d n), vecDot (p + X.potential x) (q + X.flux x) = (MeasureTheory.volume (cubeSet (originCube d n))).toReal * vecDot p q

On the half-open centered cube, the affine perturbation of a zero-trace / zero-normal-trace L² correction has pairing integral equal to the cube volume times the constant pairing.

theorem HCPolySupport.CorrectionFieldData.integral_potential_affine_cubeSet_originCube {d : ℕ} [NeZero d] {n : ℤ} (X : CorrectionFieldData (cubeSet (originCube d n))) (p : Vec d) : (fun (i : Fin d) => ∫ (x : Vec d) in cubeSet (originCube d n), (p + X.potential x) i) = (MeasureTheory.volume (cubeSet (originCube d n))).toReal • p

On the half-open centered cube, the affine potential field p + correction has componentwise integral equal to the cube volume times p.

theorem HCPolySupport.CorrectionFieldData.integral_flux_affine_cubeSet_originCube {d : ℕ} [NeZero d] {n : ℤ} (X : CorrectionFieldData (cubeSet (originCube d n))) (q : Vec d) : (fun (i : Fin d) => ∫ (x : Vec d) in cubeSet (originCube d n), (q + X.flux x) i) = (MeasureTheory.volume (cubeSet (originCube d n))).toReal • q

On the half-open centered cube, the affine flux field q + correction has componentwise integral equal to the cube volume times q.