Coarse-graining support:

Support.Deterministic.ConstantCoefficientDirichletBesov.ContinuousKRegularity

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

Continuous K-functional regularity for the unit-cube Dirichlet problem

This module transfers the concrete constant-coefficient Dirichlet endpoint estimates to the exact continuous K-functional on the centered unit cube.

noncomputable def HCPolySupport.unitCubeGradientEuclideanL2Field {d : ℕ} (w : H10Function (openCubeSet (originCube d 0))) : UnitCubeEuclideanL2Field d

The gradient of a zero-trace unit-cube function, packaged as the exact Euclidean L² field consumed by the continuous K-functional.

Equations

• HCPolySupport.unitCubeGradientEuclideanL2Field w = { toField := fun (x : HCPolySupport.Vec d) => w.grad x, euclideanMemL2 := ⋯ }

@[simp]

theorem HCPolySupport.unitCubeGradientEuclideanL2Field_apply {d : ℕ} (w : H10Function (openCubeSet (originCube d 0))) (x : Vec d) : (unitCubeGradientEuclideanL2Field w).toField x = w.grad x

theorem HCPolySupport.exists_unitCubeDirichletContinuousKFunctionalRegularity (d : ℕ) [NeZero d] : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (h : UnitCubeEuclideanL2Field d) (w : H10Function (openCubeSet (originCube d 0))) (t : ↑ContinuousKScale), CubeDirichletDivergenceProblem (originCube d 0) w h.toField → continuousKFunctional t (unitCubeGradientEuclideanL2Field w) ≤ C * continuousKFunctional t h

The exact continuous K-functional estimate for the constant-coefficient zero-Dirichlet divergence problem on the centered unit cube. The constant is chosen before the datum, solution, and interpolation scale, so it depends only on the dimension.