Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Foundations.CubeCalderonZygmund.GoodLambdaParameters

Coarse-graining support: Support.Sobolev.Foundations.CubeCalderonZygmund.GoodLambdaParameters #

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Strict parameters for the cube good-lambda iteration #

The local comparison coefficient is fixed before the cube, solution, and datum. This file chooses the amplification and datum parameters which make the weighted layer-cake self coefficient strictly smaller than one.

source
theorem HCPolySupport.CubeCalderonZygmund.INTERNAL.exists_strict_goodLambda_parameters {p r : ℝ} {C : ENNReal} (hC : C ≠ ⊤) (_hp : 2 < p) (hpr : p < r) :
∃ (M : ℝ) (eps : ℝ), 1 < M ∧ 0 < eps ∧ eps ≤ 1 ∧ C * (ENNReal.ofReal ((M / 2) ^ (2 - r)) + ENNReal.ofReal (eps ^ 2)) * ENNReal.ofReal ((2 * M) ^ (p - 2)) < 1

Fixed parameters which make the one-level good-lambda self coefficient strictly smaller than one. The result is deliberately stated in ENNReal, matching the layer-cake integration theorem.