High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorDecay.H1HsTestEmbedding

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

noncomputable def HCPolySupport.HighContrast.testCubeVectorH1 {d : ℕ} (n : ℤ) (psi : Vec d → Vec d) (hpsi : IsLocalVecTest (openCubeSet (originCube d n)) psi) : CubeVectorH1Function (originCube d n)

The coordinatewise H¹ representation of a smooth local vector test on the origin cube.

Equations

• HCPolySupport.HighContrast.testCubeVectorH1 n psi hpsi = { coord := fun (i : Fin d) => HCPolySupport.H1Function.ofContDiff ⋯ ⋯ ⋯ }

noncomputable def HCPolySupport.HighContrast.pulledTestCompetitor {d : ℕ} (n : ℤ) (psi : Vec d → Vec d) (hpsi : IsLocalVecTest (openCubeSet (originCube d n)) psi) : ContinuousKCompetitor d

A unit-cube continuous K-functional competitor obtained by pulling psi back along x ↦ centeredCubeScale n • x.

Equations

• HCPolySupport.HighContrast.pulledTestCompetitor n psi hpsi = { coord := fun (i : Fin d) => HCPolySupport.H1Function.ofContDiff ⋯ ⋯ ⋯ }

noncomputable def HCPolySupport.HighContrast.physicalGradientMatrix {d : ℕ} (psi : Vec d → Vec d) (x : Vec d) : Mat d

Matrix of coordinate gradients of the components of psi at x.

Equations

• HCPolySupport.HighContrast.physicalGradientMatrix psi x i j = HCPolySupport.HighContrast.smoothGrad (fun (y : HCPolySupport.Vec d) => psi y i) x j

noncomputable def HCPolySupport.HighContrast.physicalGradientMagnitude {d : ℕ} (psi : Vec d → Vec d) (x : Vec d) : ℝ

Frobenius magnitude of the coordinate-gradient matrix of psi at x.

Equations

• HCPolySupport.HighContrast.physicalGradientMagnitude psi x = HCPolySupport.matrixFrobeniusMagnitude (HCPolySupport.HighContrast.physicalGradientMatrix psi x)

theorem HCPolySupport.HighContrast.exists_hsNormSq_le_h1NormSq (d : ℕ) [NeZero d] (s : ↑FractionalOrder) : ∃ (K : ℝ), 0 < K ∧ ∀ (n : ℤ) (psi : Vec d → Vec d), IsLocalVecTest (openCubeSet (originCube d n)) psi → hsNormSq (openCubeSet (originCube d n)) (↑s) psi ≤ ENNReal.ofReal (K * 3 ^ (2 * (1 - ↑s) * ↑n)) * h1NormSq (openCubeSet (originCube d n)) psi

Quantitative H^1-to-H^s embedding for the complete local test class on every origin cube. The constant depends only on the dimension and order.