High-contrast homogenization: Provider.PolynomialHomogenization.NegativeSobolevCubeDuality

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

Negative Sobolev duality on triadic cubes

Below order one half, the compact-test negative Sobolev norm agrees with the normalized smooth-dual cube norm. The resulting pairing estimate extends to the full square-integrable fractional class.

noncomputable def HCPolySupport.HighContrast.cubeEuclideanWspL2FieldOfHsNormSq {d : ℕ} (Q : TriadicCube d) {s : ℝ} (hs : 0 < s) (hsHalf : s < 1 / 2) (G : Vec d → Vec d) (hGmeas : MeasureTheory.AEStronglyMeasurable G (MeasureTheory.volume.restrict (openCubeSet Q))) (hGfinite : hsNormSq (openCubeSet Q) s G ≠ ⊤) : CubeEuclideanWspL2Field Q ⟨s, ⋯⟩ FiniteLpExponent.two

Package almost everywhere strongly measurable, finite hsNormSq data as a Euclidean fractional Sobolev L² field on Q.

Equations

• HCPolySupport.HighContrast.cubeEuclideanWspL2FieldOfHsNormSq Q hs hsHalf G hGmeas hGfinite = { toField := G, euclideanMemLp := ⋯, euclideanMemWsp := ⋯, euclideanMemL2 := ⋯ }

theorem HCPolySupport.HighContrast.cubeEuclideanNegativeWspSmoothDualENorm_le_negSobolevNorm {d : ℕ} [NeZero d] (Q : TriadicCube d) {s : ℝ} (hs : 0 < s) (hsHalf : s < 1 / 2) (F : CubeEuclideanLpField Q FiniteLpExponent.two) : cubeEuclideanNegativeWspSmoothDualENorm Q ⟨s, ⋯⟩ FiniteLpExponent.two F ≤ negSobolevNorm (openCubeSet Q) s F.toField

theorem HCPolySupport.HighContrast.negSobolevNorm_le_cubeEuclideanNegativeWspSmoothDualENorm {d : ℕ} [NeZero d] (Q : TriadicCube d) {s : ℝ} (hs : 0 < s) (hsHalf : s < 1 / 2) (F : CubeEuclideanLpField Q FiniteLpExponent.two) : negSobolevNorm (openCubeSet Q) s F.toField ≤ cubeEuclideanNegativeWspSmoothDualENorm Q ⟨s, ⋯⟩ FiniteLpExponent.two F

Below the trace threshold, every compactly supported smooth unit test for the compact-test negative Sobolev norm is a unit test for the normalized cube smooth-dual norm.

theorem HCPolySupport.HighContrast.negSobolevNorm_eq_cubeEuclideanNegativeWspSmoothDualENorm {d : ℕ} [NeZero d] (Q : TriadicCube d) {s : ℝ} (hs : 0 < s) (hsHalf : s < 1 / 2) (F : CubeEuclideanLpField Q FiniteLpExponent.two) : negSobolevNorm (openCubeSet Q) s F.toField = cubeEuclideanNegativeWspSmoothDualENorm Q ⟨s, ⋯⟩ FiniteLpExponent.two F

For p = 2 and orders below one half, the compact-test negative Sobolev norm is exactly the normalized cube smooth-dual norm.

theorem HCPolySupport.HighContrast.ofReal_abs_volumeAverage_le_sqrt_hsNormSq_mul_negSobolevNorm {d : ℕ} [NeZero d] (Q : TriadicCube d) {s : ℝ} (hs : 0 < s) (hsHalf : s < 1 / 2) (F G : Vec d → Vec d) (hF : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict (openCubeSet Q))) (hGmeas : MeasureTheory.AEStronglyMeasurable G (MeasureTheory.volume.restrict (openCubeSet Q))) (hGfinite : hsNormSq (openCubeSet Q) s G ≠ ⊤) : ENNReal.ofReal |volumeAverage (openCubeSet Q) fun (x : Vec d) => vecDot (F x) (G x)| ≤ hsNormSq (openCubeSet Q) s G ^ (1 / 2) * negSobolevNorm (openCubeSet Q) s F

The normalized pairing with a finite fractional field extends from compact smooth tests to the full square-integrable fractional class.