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

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

Finite-p direct Euclidean overlap versus fractional Sobolev seminorm

This is the source-facing comparison for the canonical vector-valued overlap seminorm. The proof keeps its direct Euclidean local oscillations intact and uses scalar coordinates only internally.

noncomputable def HCPolySupport.CubeEuclideanLpField.measurableRepresentative {d : ℕ} {Q : TriadicCube d} {p : FiniteLpExponent} (F : CubeEuclideanLpField Q p) : CubeEuclideanLpField Q p

The globally measurable representative selected from a direct Euclidean L^p field. It is used internally to discharge scalar real-variable measurability conditions, while source-facing statements retain the original field carrier.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.CubeEuclideanLpField.measurable_measurableRepresentative {d : ℕ} {Q : TriadicCube d} {p : FiniteLpExponent} (F : CubeEuclideanLpField Q p) : Measurable F.measurableRepresentative.toField

theorem HCPolySupport.CubeEuclideanLpField.ae_eq_measurableRepresentative {d : ℕ} {Q : TriadicCube d} {p : FiniteLpExponent} (F : CubeEuclideanLpField Q p) : F.toField =ᵐ[normalizedCubeMeasure Q] F.measurableRepresentative.toField

noncomputable def HCPolySupport.cubeEuclideanPositiveBesovOverlapPowerEnergy {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) : ENNReal

The direct vector overlap series before its outer finite-p root.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.cubeEuclideanPositiveBesovOverlapESeminorm_rpow_eq_powerEnergy {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) : cubeEuclideanPositiveBesovOverlapESeminorm Q s p F ^ p.exponent.toReal = cubeEuclideanPositiveBesovOverlapPowerEnergy Q s p F

The canonical direct overlap seminorm to the exact finite p power is its complete source scale series.

theorem HCPolySupport.cubeEuclideanPositiveBesovOverlapESeminorm_congr_ae {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} {F G : Vec d → Vec d} (hFG : F =ᵐ[normalizedCubeMeasure Q] G) : cubeEuclideanPositiveBesovOverlapESeminorm Q s p F = cubeEuclideanPositiveBesovOverlapESeminorm Q s p G

The direct canonical Euclidean overlap seminorm is invariant under an almost-everywhere change on its parent cube.

theorem HCPolySupport.exactOverlapScalarPIntegrableOfEuclideanField {d : ℕ} (Q : TriadicCube d) (p : FiniteLpExponent) (F : CubeEuclideanLpField Q p) (i : Fin d) : ExactOverlapIntegrable Q fun (x : Vec d) => F.toField x i

noncomputable def HCPolySupport.cubeEuclideanCoordinateExactOverlapPowerEnergy {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : CubeEuclideanLpField Q p) : ENNReal

The finite sum of exact scalar overlap p-energies of the Euclidean coordinates. This is an internal aggregation device, not an additional source-facing seminorm.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.cubeEuclideanCoordinateOverlapPowerEnergy {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : CubeEuclideanLpField Q p) : ENNReal

The coordinate overlap series with the scale and center sums still explicit.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.cubeEuclideanCoordinateOverlapPowerEnergy_eq_exact {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : CubeEuclideanLpField Q p) : cubeEuclideanCoordinateOverlapPowerEnergy Q s p F = cubeEuclideanCoordinateExactOverlapPowerEnergy Q s p F

Reordering the nonnegative depth and coordinate sums identifies the explicit coordinate series with the sum of exact scalar overlap energies.

theorem HCPolySupport.cubeEuclideanCoordinateOverlapPowerEnergy_le_dimension_mul_overlap {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : CubeEuclideanLpField Q p) : cubeEuclideanCoordinateOverlapPowerEnergy Q s p F ≤ ↑d * cubeEuclideanPositiveBesovOverlapPowerEnergy Q s p F.toField

Aggregating the coordinate lower bound over centers and all scales.

theorem HCPolySupport.exactOverlapScalarPSeminorm_le_dimension_mul_cubeEuclideanOverlap {d : ℕ} [NeZero d] (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : CubeEuclideanLpField Q p) (i : Fin d) (hF : ExactOverlapIntegrable Q fun (x : Vec d) => F.toField x i) : exactOverlapFiniteSeminorm (exactOverlapScalarPParameters s p) Q (fun (x : Vec d) => F.toField x i) hF ≤ ↑d * cubeEuclideanPositiveBesovOverlapESeminorm Q s p F.toField

One scalar exact-overlap seminorm is controlled by the direct Euclidean overlap seminorm. This is the coordinate extraction needed when a scalar positive test is assembled from a Euclidean fractional-Sobolev field.

theorem HCPolySupport.cubeEuclideanOverlapPowerEnergy_le_coordinate_mul {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : CubeEuclideanLpField Q p) (hF : Measurable F.toField) : cubeEuclideanPositiveBesovOverlapPowerEnergy Q s p F.toField ≤ cubeCoordinateGagliardoComparisonConstant d p * cubeEuclideanCoordinateOverlapPowerEnergy Q s p F

Aggregating the finite-dimensional Euclidean upper bound over centers and all scales. Measurability is needed only to invoke the standard coordinate-sum L^p estimate; it is not an additional regularity premise.

noncomputable def HCPolySupport.cubeEuclideanOverlapToWspPowerConstant (d : ℕ) (p : FiniteLpExponent) : ENNReal

The finite comparison constant bounding the pth power of the Euclidean overlap seminorm by the pth power of the fractional Sobolev seminorm.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.cubeEuclideanWspToOverlapPowerConstant (d : ℕ) (p : FiniteLpExponent) : ENNReal

The finite comparison constant bounding the pth power of the Euclidean fractional Sobolev seminorm by the pth power of the overlap seminorm.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.cubeEuclideanOverlapToWspPowerConstant_lt_top (d : ℕ) (p : FiniteLpExponent) : cubeEuclideanOverlapToWspPowerConstant d p < ⊤

theorem HCPolySupport.cubeEuclideanWspToOverlapPowerConstant_lt_top (d : ℕ) (p : FiniteLpExponent) : cubeEuclideanWspToOverlapPowerConstant d p < ⊤

noncomputable def HCPolySupport.cubeEuclideanWspOverlapDimensionConstant (d : ℕ) : ENNReal

A deliberately coarse constant depending only on the dimension. It absorbs the finite-coordinate and metric changes without any dependence on the fractional order or the finite exponent.

Equations

• HCPolySupport.cubeEuclideanWspOverlapDimensionConstant d = 2 * 3 ^ d * HCPolySupport.Gagliardo.gagliardoBesovLowerConstant d * ↑d ^ (↑d + 4)

theorem HCPolySupport.cubeEuclideanWspOverlapDimensionConstant_lt_top (d : ℕ) : cubeEuclideanWspOverlapDimensionConstant d < ⊤

The dimension-only overlap/fractional comparison constant is finite.

theorem HCPolySupport.cubeEuclideanOverlapRootConstant_le_dimensionConstant {d : ℕ} [NeZero d] (p : FiniteLpExponent) : cubeEuclideanOverlapToWspPowerConstant d p ^ p.exponent.toReal⁻¹ ≤ cubeEuclideanWspOverlapDimensionConstant d

theorem HCPolySupport.cubeEuclideanWspRootConstant_le_dimensionConstant {d : ℕ} [NeZero d] (p : FiniteLpExponent) : cubeEuclideanWspToOverlapPowerConstant d p ^ p.exponent.toReal⁻¹ ≤ cubeEuclideanWspOverlapDimensionConstant d

theorem HCPolySupport.cubeEuclideanOverlap_le_rootConstant_mul_wsp {d : ℕ} [NeZero d] (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : CubeEuclideanLpField Q p) : cubeEuclideanPositiveBesovOverlapESeminorm Q s p F.toField ≤ cubeEuclideanOverlapToWspPowerConstant d p ^ p.exponent.toReal⁻¹ * cubeEuclideanWspESeminorm Q s p F.toField

Source-facing finite-p overlap-to-fractional comparison. The field carrier provides only its L^p class; a globally measurable representative is selected internally and the two seminorms are transported back by their proved a.e. congruence.

theorem HCPolySupport.cubeEuclideanWsp_le_rootConstant_mul_overlap {d : ℕ} [NeZero d] (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : CubeEuclideanLpField Q p) : cubeEuclideanWspESeminorm Q s p F.toField ≤ cubeEuclideanWspToOverlapPowerConstant d p ^ p.exponent.toReal⁻¹ * cubeEuclideanPositiveBesovOverlapESeminorm Q s p F.toField

Source-facing finite-p fractional-to-overlap comparison, with the same internally selected measurable representative.

theorem HCPolySupport.cubeEuclideanOverlap_le_dimensionConstant_mul_wsp {d : ℕ} [NeZero d] (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : CubeEuclideanLpField Q p) : cubeEuclideanPositiveBesovOverlapESeminorm Q s p F.toField ≤ cubeEuclideanWspOverlapDimensionConstant d * cubeEuclideanWspESeminorm Q s p F.toField

Source-facing finite-p overlap-to-fractional comparison with a constant depending only on the dimension.

theorem HCPolySupport.cubeEuclideanWsp_le_dimensionConstant_mul_overlap {d : ℕ} [NeZero d] (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : CubeEuclideanLpField Q p) : cubeEuclideanWspESeminorm Q s p F.toField ≤ cubeEuclideanWspOverlapDimensionConstant d * cubeEuclideanPositiveBesovOverlapESeminorm Q s p F.toField

Source-facing finite-p fractional-to-overlap comparison with the same dimension-only constant.