High-contrast homogenization: Provider.PolynomialHomogenization.CompactTestCutoffEstimate #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Quantitative compact cutoff estimate #
The canonical cube cutoff has a vanishing boundary-layer error in the normalized fractional square norm below the trace threshold.
theorem
HCPolySupport.HighContrast.CompactTestDensity.hsNormSq_canonicalCutoff_sub_le
{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₀)
(h₀ : Vec d → Vec d)
(h₀smooth : ContDiff ℝ (↑⊤) h₀)
(h₀bound : ∀ (x : Vec d), ‖h₀ x‖ ≤ M)
(h₀lip : ∀ (x y : Vec d), ‖h₀ x - h₀ y‖ ≤ L₀ * ‖x - y‖)
{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)))
{t : ℝ}
(ht : 0 < t)
(htHalf : t < 1 / 2)
:
have η := QuantitativeCubeCutoff.canonicalFun Q (1 - 2 * t) (1 - t);
have D := ↑d * smoothTransitionProfile.derivBound * 2 / cubeRadius Q;
have B := L₀ + M * D + 1;
have Kvol := 2 * ↑d * cubeVolume Q;
have K₀ := ((2 * √↑d * M) ^ (1 - theta) * (√↑d * B) ^ theta) ^ 2;
have p := 1 - 2 * theta;
(hsNormSq (openCubeSet Q) s fun (x : Vec d) => η x • h₀ x - h₀ x) ≤ MeasureTheory.volume (openCubeSet Q) ^ (-(2 * s) / ↑d) * (ENNReal.ofReal (↑d * M ^ 2) * ENNReal.ofReal Kvol / MeasureTheory.volume (openCubeSet Q)) * ENNReal.ofReal t + 2 * (ENNReal.ofReal K₀ * ENNReal.ofReal Kvol * C * ENNReal.ofReal ((2 * cubeRadius Q) ^ (2 * theta - ↑d - 2 * s + ↑d)) / MeasureTheory.volume (openCubeSet Q)) * ENNReal.ofReal t ^ p
The canonical cube cutoff converges in the fractional square norm below order one half.