High-contrast homogenization: Provider.PolynomialHomogenization.Root.Duality.CubeHodgeByDuality

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

The cube Hodge estimate in the negative norm, by duality

On a triadic cube the Hodge system w zero-trace potential, w + F solenoidal, says exactly that w is the (negative of the) orthogonal projection of F onto the zero-trace potentials. Against a test psi the projection moves to the other slot — the projector is self-adjoint for the L² pairing — so the negative fractional norm of w is priced by the positive H^s stability of that projection.

The step that makes this legal is the ofReal_abs_volumeAverage_le_sqrt_hsNormSq_mul_negSobolevNorm: on a cube and below the trace threshold the normalized pairing against negSobolevNorm extends from compact smooth tests to every square-integrable field of finite fractional norm. The projected test is such a field, so no density or Besov bridge is needed.

def HCPolySupport.HighContrast.RowSupply.CubeGradientProjectionHsStability (d : ℕ) (Q : TriadicCube d) (s Cproj : ℝ) : Prop

Positive H^s stability of the zero-trace gradient projection on a cube. Every admissible test splits into a zero-trace potential part and a solenoidal remainder, with the potential part bounded in H^s by the test. This is the positive-direction input; everything below is duality.

Equations

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

theorem HCPolySupport.HighContrast.RowSupply.negSobolevNorm_le_of_cubeGradientProjectionHsStability {d : ℕ} [NeZero d] (Q : TriadicCube d) {s Cproj : ℝ} (hs : 0 < s) (hsHalf : s < 1 / 2) (hproj : CubeGradientProjectionHsStability d Q s Cproj) {w F : Vec d → Vec d} (hF : MemVectorL2 (openCubeSet Q) F) (hw : IsPotentialZeroTraceOn (openCubeSet Q) w) (hsol : IsSolenoidalOn (openCubeSet Q) fun (x : Vec d) => w x + F x) : negSobolevNorm (openCubeSet Q) s w ≤ ENNReal.ofReal Cproj * negSobolevNorm (openCubeSet Q) s F

The cube Hodge estimate in the negative fractional norm, obtained from the positive stability of the projection by duality.