High-contrast homogenization: Provider.Regularity.RoundedUnitCubeDirichletEuclideanHsRegularity

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

Rounded-reference Euclidean fractional regularity on the unit cube

The selected small positive order from the rounded affine iteration is converted from its quadratic continuous-K energy to the exact Euclidean fractional carrier and additive full norm. The conversion keeps the datum and solution membership statements internal to the proof: the caller supplies only Euclidean H^s membership of the datum, while existence, the weak equation, output membership, and the quantitative estimate are all conclusions.

theorem HCPolySupport.HighContrast.unitCubeNormalizedContinuousKEnergy_le_two_mul_continuousKFullENorm_sq {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) (hweight : ENNReal.ofReal (2 * ↑s) ≤ 1) : unitCubeNormalizedContinuousKEnergy s F ≤ 2 * continuousKFullENorm s F ^ 2

When the selected scalar weight is at most one, the quadratic continuous-K energy is controlled by twice the square of the additive continuous-K full norm.

theorem HCPolySupport.HighContrast.continuousKFullENorm_le_mul_unitCubeNormalizedContinuousKEnergy_rpow {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) (hweightZero : ENNReal.ofReal (2 * ↑s) ≠ 0) (hweightTop : ENNReal.ofReal (2 * ↑s) ≠ ⊤) : continuousKFullENorm s F ≤ (1 + (ENNReal.ofReal (2 * ↑s))⁻¹ ^ (1 / 2)) * unitCubeNormalizedContinuousKEnergy s F ^ (1 / 2)

A positive continuous-K energy weight controls the additive continuous-K full norm by the square root of the quadratic energy.

theorem HCPolySupport.HighContrast.exists_roundedUnitCubeDirichletEuclideanHsRegularity (d : ℕ) [NeZero d] : ∃ (s : ↑FractionalOrder), ↑s < 1 / 12 ∧ ∃ C < ⊤, ∀ (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (h : UnitCubeEuclideanL2Field d), MemEuclideanHs s h → ∃ (u : H10Function (openCubeSet (originCube d 0))), (IsZeroTraceDirichletRhsWeakSolution (constantCoeffField (roundedReferenceMatrix abar hS)) (openCubeSet (originCube d 0)) u fun (x : Vec d) => -h.toField x) ∧ MemEuclideanHs s (unitCubeGradientEuclideanL2Field u) ∧ euclideanHsFullENorm s (unitCubeGradientEuclideanL2Field u) ≤ C * euclideanHsFullENorm s h

For one selected order below 1/12, every rounded-reference constant-coefficient divergence datum in exact Euclidean H^s has a zero-trace weak response whose gradient remains in Euclidean H^s, with one finite constant fixed before the matrix and datum.