Coarse-graining support: #
Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.HarmonicFinal.ExactSmallCube .CenteredFactors.BufferedAlpha
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Exact small-cube centered factors: buffered alpha comparison #
theorem
HCPolySupport.coarseCaccioppoliFluxEnergyExactCenteredFactorBounds_buffered_localAcirc_le_alpha_of_scale
{d : ℕ}
[NeZero d]
{Q R : TriadicCube d}
(a : CoeffField d)
{s t CeffLocal CeffWork : ℝ}
{k j : ℕ}
{ρ₁ ρ₂ lam Lam : ℝ}
{hheight : ℝ → ℝ → ℝ}
(hCeffLocal : 0 ≤ CeffLocal)
(hCeffWork : 0 ≤ CeffWork)
(hs : 0 < s)
(ht : 0 < t)
(hst : s + t < 1)
(hEllCube : IsEllipticFieldOn lam Lam (cubeSet Q) a)
(hR : R ∈ descendantsAtDepth Q j)
(hBsum_s :
Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
(hSigmaSum_t :
Summable fun (n : ℕ) =>
geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2))
(hchoice : CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂)
(hlt : ρ₁ < ρ₂)
(hjk : k ≤ j)
(hscale :
(2 * coarseCaccioppoliCenteredAverageFront d s CeffLocal + 4 * coarseCaccioppoliCenteredBesovHessianFront d s CeffLocal + 2 * coarseCaccioppoliCenteredBesovGradientFront d s CeffLocal) * Real.rpow 3 ↑k ≤ CeffWork / (s * (1 - s)) * coarseCaccioppoliGapInv ρ₁ ρ₂)
(hheight_le_j : hheight ρ₁ ρ₂ ≤ ↑j)
:
have ρm := coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂;
coarseCaccioppoliFluxEnergyExactCenteredAverageCoeffFactorBound (coarseCaccioppoliLambdaFactor R a s)
(coarseCaccioppoliQuantitativeCutoffGradientBound Q ρ₁ ρm) (coarseCaccioppoliCanonicalGradientAcircOne R a ρ₁ ρm)
CeffLocal + coarseCaccioppoliFluxEnergyExactCenteredBesovCoeffFactorBound R s (coarseCaccioppoliLambdaFactor R a s)
(coarseCaccioppoliLambdaFactor R a s)
(coarseCaccioppoliCenteredCutoffCoeffFactorBound R s (coarseCaccioppoliQuantitativeCutoffGradientBound Q ρ₁ ρm)
(coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρm) (coarseCaccioppoliCanonicalGradientAcircOne R a ρ₁ ρm)
(coarseCaccioppoliCanonicalGradientAcircOneSub R a s ρ₁ ρm) CeffLocal) ≤ coarseCaccioppoliBoundaryAlphaOfHeight Q a s t CeffWork hheight ρ₁ ρ₂
Buffered average-plus-Besov factor-bound comparison for the centered exact
coefficient. The cutoff is taken at the midpoint radius, while the scale
choice, height, and parent Alpha coefficient are still indexed by the full
outer pair (ρ₁, ρ₂).