Coarse-graining support:

Support.Deterministic.ConstantCoefficientDirichletBesov.CenteredCubeHsRegularity

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

Exact centered-cube Euclidean H^s Dirichlet regularity

This module first converts the unit-cube continuous interpolation estimate to the exact Euclidean fractional full norm. It then transports that estimate to every centered triadic cube. The physical full norm carries the essential root factor 3^(-m s) in front of its normalized L² term, making both terms scale by the same factor.

Main definitions

• centeredCubeEuclideanHsFullENorm: the homogeneous physical fractional full norm.

Main results

• exactOverlapRootWeight_originCube_eq_scale_rpow: the exact root-factor formula.
• centeredCubeEuclideanHsFullENorm_eq_scale_mul_pullbackToUnit: exact full norm scaling.
• exists_centeredCubeDirichletEuclideanHsFullENormRegularity: the all-scale exact Euclidean H^s Dirichlet estimate.

noncomputable def HCPolySupport.centeredCubeEuclideanHsFullENorm {d : ℕ} {m : ℤ} (s : ↑FractionalOrder) (F : CenteredCubeEuclideanL2Field d m) : ENNReal

The homogeneous exact Euclidean fractional full norm on a centered cube. The normalized L² term carries the same root-scale weight as the fractional seminorm.

Equations

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

theorem HCPolySupport.centeredCubeEuclideanHsFullENorm_eq {d : ℕ} {m : ℤ} (s : ↑FractionalOrder) (F : CenteredCubeEuclideanL2Field d m) : centeredCubeEuclideanHsFullENorm s F = exactOverlapRootWeight (originCube d m) ↑s * (centeredCubeDomain d m).normalizedEuclideanLpENorm 2 F.toField + centeredCubeEuclideanHsESeminorm s F

Evaluation formula for the homogeneous physical fractional full norm.

theorem HCPolySupport.exactOverlapRootWeight_originCube_eq_scale_rpow {d : ℕ} (m : ℤ) (s : ℝ) : exactOverlapRootWeight (originCube d m) s = ENNReal.ofReal (centeredCubeScale m) ^ (-s)

On originCube d m, the overlap root factor is exactly the fractional dilation factor (3 ^ m)^(-s).

theorem HCPolySupport.centeredCubeEuclideanHsFullENorm_eq_scale_mul_pullbackToUnit {d : ℕ} {m : ℤ} (s : ↑FractionalOrder) (F : CenteredCubeEuclideanL2Field d m) : centeredCubeEuclideanHsFullENorm s F = ENNReal.ofReal (centeredCubeScale m) ^ (-↑s) * euclideanHsFullENorm s F.pullbackToUnit

The physical full norm scales homogeneously by (3 ^ m)^(-s) under pullback to the centered unit cube.

theorem HCPolySupport.exists_unitCubeDirichletEuclideanHsFullENormRegularity (d : ℕ) [NeZero d] (s : ↑FractionalOrder) : ∃ C < ⊤, ∀ (h : UnitCubeEuclideanL2Field d) (w : H10Function (openCubeSet (originCube d 0))), CubeDirichletDivergenceProblem (originCube d 0) w h.toField → euclideanHsFullENorm s (unitCubeGradientEuclideanL2Field w) ≤ C * euclideanHsFullENorm s h

The unit-cube weak Dirichlet problem controls the exact Euclidean fractional full norm. Both directions of the approved full-norm comparison are used internally.

theorem HCPolySupport.exists_centeredCubeDirichletEuclideanHsFullENormRegularity (d : ℕ) [NeZero d] (s : ↑FractionalOrder) : ∃ C < ⊤, ∀ (m : ℤ) (h : CenteredCubeEuclideanL2Field d m) (w : H10Function (openCubeSet (originCube d m))), CubeDirichletDivergenceProblem (originCube d m) w h.toField → centeredCubeEuclideanHsFullENorm s (centeredCubeGradientEuclideanL2Field w) ≤ C * centeredCubeEuclideanHsFullENorm s h

One finite constant, fixed before the cube scale, datum, and solution, controls the homogeneous exact Euclidean fractional full norm on every centered triadic cube.