Coarse-graining support:

Support.Sobolev.Fractional.ContinuousInterpolation.EuclideanHsMeasurability

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

Measurability closure for the exact Euclidean fractional energy

theorem HCPolySupport.measurable_euclideanHsIntegrand_of_measurable {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) (hF : Measurable F.toField) : Measurable (euclideanHsIntegrand s F)

A globally measurable representative has a measurable totalized exact Euclidean fractional-energy integrand.

theorem HCPolySupport.aemeasurable_euclideanHsIntegrand {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) : AEMeasurable (euclideanHsIntegrand s F) (euclideanHsProductMeasure d)

The exact Euclidean integrand is a.e.-measurable for every stored L² field, by transport from its canonical measurable representative.

theorem HCPolySupport.memEuclideanHs_iff_energy_lt_top {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) : MemEuclideanHs s F ↔ euclideanHsEnergy s F < ⊤

With integrand measurability now automatic, exact fractional membership is precisely finiteness of the extended Euclidean energy.

theorem HCPolySupport.euclideanHsESeminorm_lt_top_iff_energy_lt_top {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) : euclideanHsESeminorm s F < ⊤ ↔ euclideanHsEnergy s F < ⊤

Taking the positive half-power preserves finiteness of the exact Euclidean fractional energy.

theorem HCPolySupport.memEuclideanHs_iff_euclideanHsESeminorm_lt_top {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) : MemEuclideanHs s F ↔ euclideanHsESeminorm s F < ⊤

Exact fractional membership is equivalently finiteness of the extended Euclidean fractional seminorm.