High-contrast homogenization: Provider.PolynomialHomogenization.CompactTestCutoffKernel #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Cutoff kernel estimates #
This file collects interpolation and supported-field estimates used to compactify smooth fractional Sobolev test fields.
theorem
HCPolySupport.HighContrast.CompactTestDensity.fractionalKernel_le_of_bounded_lipschitz
{d : ℕ}
[NeZero d]
{s theta M L : ℝ}
(hs : 0 ≤ s)
(hstheta : s < theta)
(hthetaHalf : theta < 1 / 2)
(hM : 0 ≤ M)
(hL : 0 ≤ L)
(g : Vec d → Vec d)
{x y : Vec d}
(hxM : ‖g x‖ ≤ M)
(hyM : ‖g y‖ ≤ M)
(hxyLip : ‖g x - g y‖ ≤ L * ‖x - y‖)
:
A bounded Lipschitz field satisfies the interpolated fractional-kernel bound.
theorem
HCPolySupport.HighContrast.CompactTestDensity.fracSeminormSq_le_supported_bounded_lipschitz
{d : ℕ}
[NeZero d]
(Q : TriadicCube d)
{s theta M L : ℝ}
(hs : 0 ≤ s)
(hstheta : s < theta)
(hthetaHalf : theta < 1 / 2)
(hM : 0 ≤ M)
(hL : 0 ≤ L)
(g : Vec d → Vec d)
(hgcont : Continuous g)
(hgbound : ∀ x ∈ openCubeSet Q, ‖g x‖ ≤ M)
(hglip : ∀ (x y : Vec d), ‖g x - g y‖ ≤ L * ‖x - y‖)
{A : Set (Vec d)}
(hAmeas : MeasurableSet A)
(hAU : A ⊆ openCubeSet Q)
(hgzero : ∀ x ∈ openCubeSet Q, x ∉ A → g x = 0)
{C : ENNReal}
(hC :
∀ (x : Vec d) {r : ℝ},
0 < r →
∫⁻ (y : Vec d) in Metric.ball x r, ENNReal.ofReal (‖x - y‖ ^ (2 * theta - ↑d - 2 * s)) ≤ C * ENNReal.ofReal (r ^ (2 * theta - ↑d - 2 * s + ↑d)))
:
fracSeminormSq (openCubeSet Q) s g ≤ 2 * (ENNReal.ofReal (((2 * √↑d * M) ^ (1 - theta) * (√↑d * L) ^ theta) ^ 2) * C * ENNReal.ofReal ((2 * cubeRadius Q) ^ (2 * theta - ↑d - 2 * s + ↑d)) * MeasureTheory.volume A) / MeasureTheory.volume (openCubeSet Q)
The fractional square seminorm of a supported bounded Lipschitz field is controlled by its support geometry.