Coarse-graining support: Support.Sobolev.Fractional.EuclideanH2

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

Exact Euclidean fractional H^s carrier on the centered unit cube

This module is the literal p = 2 fractional Sobolev side of the Chapter 1 constant-coefficient Dirichlet argument. It deliberately does not identify this seminorm with the continuous K-functional: that equivalence is a separate analytic theorem.

The project carrier Vec d retains its product norm. Both the domain metric and the target magnitude below are instead spelled out through euclideanDist and HilbertVec.ofVec, exactly as required by the source's Euclidean convention for vector fields.

noncomputable def HCPolySupport.euclideanHsProductMeasure (d : ℕ) : MeasureTheory.Measure (Vec d × Vec d)

The source measure fint_{□_0} dx ∫_{□_0} dy: normalized volume in the first variable and unnormalized restricted Lebesgue volume in the second.

Equations

• HCPolySupport.euclideanHsProductMeasure d = (HCPolySupport.unitCenteredCubeDomain d).normalizedVolume.prod (HCPolySupport.unitCenteredCubeDomain d).restrictedVolume

noncomputable def HCPolySupport.euclideanHsIntegrand {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) : Vec d × Vec d → ENNReal

The literal nonnegative integrand |F(x)-F(y)|² / |x-y|^(d + 2s) of the p = 2 fractional Sobolev seminorm. The numerator uses the Euclidean Hilbert realization, not the ambient Vec norm.

Equations

• HCPolySupport.euclideanHsIntegrand s F z = ENNReal.ofReal (‖HCPolySupport.HilbertVec.ofVec (F.toField z.1 - F.toField z.2)‖ ^ 2 / (HCPolySupport.euclideanDist z.1 z.2).rpow (↑d + 2 * ↑s))

noncomputable def HCPolySupport.euclideanHsEnergy {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) : ENNReal

The squared exact fractional Sobolev quantity, before the 1/2 power.

Equations

• HCPolySupport.euclideanHsEnergy s F = ∫⁻ (z : HCPolySupport.Vec d × HCPolySupport.Vec d), HCPolySupport.euclideanHsIntegrand s F z ∂HCPolySupport.euclideanHsProductMeasure d

noncomputable def HCPolySupport.euclideanHsESeminorm {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) : ENNReal

The exact extended H^s seminorm of a vector field on the centered unit cube. It is extended-valued so that no non-finiteness is silently totalized.

Equations

• HCPolySupport.euclideanHsESeminorm s F = HCPolySupport.euclideanHsEnergy s F ^ 2⁻¹

structure HCPolySupport.MemEuclideanHs {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) : Prop

Membership in the exact fractional Euclidean H^s carrier: the literal kernel is measurable and its source integral is finite.

• integrand_aemeasurable : AEMeasurable (euclideanHsIntegrand s F) (euclideanHsProductMeasure d)
• energy_lt_top : euclideanHsEnergy s F < ⊤

theorem HCPolySupport.euclideanHsEnergy_eq_lintegral {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) : euclideanHsEnergy s F = ∫⁻ (z : Vec d × Vec d), ENNReal.ofReal (‖HilbertVec.ofVec (F.toField z.1 - F.toField z.2)‖ ^ 2 / (euclideanDist z.1 z.2).rpow (↑d + 2 * ↑s)) ∂euclideanHsProductMeasure d

theorem HCPolySupport.euclideanHsESeminorm_eq_lintegral {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) : euclideanHsESeminorm s F = (∫⁻ (z : Vec d × Vec d), ENNReal.ofReal (‖HilbertVec.ofVec (F.toField z.1 - F.toField z.2)‖ ^ 2 / (euclideanDist z.1 z.2).rpow (↑d + 2 * ↑s)) ∂euclideanHsProductMeasure d) ^ 2⁻¹

theorem HCPolySupport.memEuclideanHs_iff {d : ℕ} {s : ↑FractionalOrder} {F : UnitCubeEuclideanL2Field d} : MemEuclideanHs s F ↔ AEMeasurable (euclideanHsIntegrand s F) (euclideanHsProductMeasure d) ∧ euclideanHsEnergy s F < ⊤

theorem HCPolySupport.euclideanHsIntegrand_congr_ae {d : ℕ} {s : ↑FractionalOrder} {F G : UnitCubeEuclideanL2Field d} (hFG : F.toField =ᵐ[(unitCenteredCubeDomain d).normalizedVolume] G.toField) : euclideanHsIntegrand s F =ᵐ[euclideanHsProductMeasure d] euclideanHsIntegrand s G

Altering a datum on a normalized-volume null set does not alter the literal double-integral integrand except on a product-measure null set.

theorem HCPolySupport.euclideanHsEnergy_congr_ae {d : ℕ} {s : ↑FractionalOrder} {F G : UnitCubeEuclideanL2Field d} (hFG : F.toField =ᵐ[(unitCenteredCubeDomain d).normalizedVolume] G.toField) : euclideanHsEnergy s F = euclideanHsEnergy s G

The squared source integral is invariant under normalized-volume a.e. replacement of the vector field.

theorem HCPolySupport.euclideanHsESeminorm_congr_ae {d : ℕ} {s : ↑FractionalOrder} {F G : UnitCubeEuclideanL2Field d} (hFG : F.toField =ᵐ[(unitCenteredCubeDomain d).normalizedVolume] G.toField) : euclideanHsESeminorm s F = euclideanHsESeminorm s G

The exact extended fractional seminorm is invariant under normalized-volume a.e. replacement of the vector field.

theorem HCPolySupport.memEuclideanHs_congr_ae {d : ℕ} {s : ↑FractionalOrder} {F G : UnitCubeEuclideanL2Field d} (hFG : F.toField =ᵐ[(unitCenteredCubeDomain d).normalizedVolume] G.toField) : MemEuclideanHs s F ↔ MemEuclideanHs s G

Exact fractional membership is stable under normalized-volume a.e. replacement of the field.