Coarse-graining support:

Support.Deterministic.ConstantCoefficientDirichletBesov.ContinuousKFullRegularity

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

Full continuous K-regularity for the unit-cube Dirichlet problem

This module integrates the pointwise continuous K-functional estimate and combines it with the exact normalized Euclidean L² energy estimate. The resulting full-norm constant is chosen before the fractional order, datum, and solution.

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

Integrating the pointwise continuous K-functional estimate gives a uniform continuum interpolation-seminorm estimate.

theorem HCPolySupport.exists_unitCubeGradientNormalizedEuclideanL2EnergyRegularity (d : ℕ) : ∃ C < ⊤, ∀ (h : UnitCubeEuclideanL2Field d) (w : H10Function (openCubeSet (originCube d 0))), CubeDirichletDivergenceProblem (originCube d 0) w h.toField → (unitCenteredCubeDomain d).normalizedEuclideanLpENorm 2 (unitCubeGradientEuclideanL2Field w).toField ≤ C * (unitCenteredCubeDomain d).normalizedEuclideanLpENorm 2 h.toField

The weak Dirichlet equation controls the exact normalized Euclidean L² norm of the solution gradient by that of the datum. The concrete ambient-norm energy theorem is converted here using both directions of the explicit finite-dimensional Euclidean/ambient norm comparison.

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

The exact additive continuous-interpolation full norm of the unit-cube Dirichlet solution gradient is controlled by that of the datum. A single finite dimension-dependent constant is chosen before the fractional order, datum, and solution; all endpoint and comparison estimates are discharged in the proof.