High-contrast homogenization: Provider.Regularity.UnitCubeDirichletContinuousKCompetitor

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Unit-cube continuous K-functional competitor bounds

The exact normalized Euclidean L² residual contraction is combined with the identity-Dirichlet H² lift. For every genuine continuous H¹ competitor of the datum, this produces a genuine continuous H¹ competitor of the solution gradient. The lower endpoint retains constant one; only the upper endpoint carries a dimension-dependent constant.

noncomputable def HCPolySupport.HighContrast.continuousKCompetitorToUnitCubeEuclideanL2Field {d : ℕ} (G : ContinuousKCompetitor d) : UnitCubeEuclideanL2Field d

The unit-cube Euclidean L² field underlying a continuous K-functional competitor.

Equations

• HCPolySupport.HighContrast.continuousKCompetitorToUnitCubeEuclideanL2Field G = { toField := G.toField, euclideanMemL2 := ⋯ }

theorem HCPolySupport.HighContrast.exists_unitCubeDirichletContinuousKCompetitorBounds (d : ℕ) [NeZero d] : ∃ (B : ℝ), 0 ≤ B ∧ ∀ (h : UnitCubeEuclideanL2Field d) (w : H10Function (openCubeSet (originCube d 0))) (G : ContinuousKCompetitor d), CubeDirichletDivergenceProblem (originCube d 0) w h.toField → ∃ (V : ContinuousKCompetitor d), continuousKResidualNorm (unitCubeGradientEuclideanL2Field w) V ≤ continuousKResidualNorm h G ∧ continuousKGradientNorm V ≤ B * continuousKGradientNorm G

Every continuous H¹ competitor for the datum lifts to a continuous H¹ competitor for the unit-cube Dirichlet solution gradient. The residual bound is nonexpansive in the exact normalized Euclidean L² norm; the upper endpoint constant is fixed before the datum, solution, and competitor.