Coarse-graining support:

Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.HarmonicFinal.ExactSmallCube .CenteredFactors.Besov

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

Exact small-cube centered factors: Besov cutoff pieces

theorem HCPolySupport.coarseCaccioppoliFluxEnergyExactCenteredBesovCoeffFactorBound_localAcirc_le_rpow_sub {d : ℕ} {Q R : TriadicCube d} (a : CoeffField d) {s Ceff : ℝ} {k j : ℕ} {ρ₁ ρ₂ : ℝ} (hCeff : 0 ≤ Ceff) (hs : 0 < s) (hs1 : s < 1) (hR : R ∈ descendantsAtDepth Q j) (hchoice : CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂) (hlt : ρ₁ < ρ₂) (hjk : k ≤ j) : have Pone := (LambdaSq R s (MultiscaleExponent.finite 1) a).rpow (1 / 2) * (lambdaSq R 1 (MultiscaleExponent.finite 1) a).rpow (-1 / 2); have Psub := (LambdaSq R s (MultiscaleExponent.finite 1) a).rpow (1 / 2) * (lambdaSq R (1 - s) (MultiscaleExponent.finite 1) a).rpow (-1 / 2); coarseCaccioppoliFluxEnergyExactCenteredBesovCoeffFactorBound R s (coarseCaccioppoliLambdaFactor R a s) (coarseCaccioppoliLambdaFactor R a s) (coarseCaccioppoliCenteredCutoffCoeffFactorBound R s (coarseCaccioppoliQuantitativeCutoffGradientBound Q ρ₁ ρ₂) (coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρ₂) (coarseCaccioppoliCanonicalGradientAcircOne R a ρ₁ ρ₂) (coarseCaccioppoliCanonicalGradientAcircOneSub R a s ρ₁ ρ₂) Ceff) ≤ coarseCaccioppoliCenteredBesovHessianFront d s Ceff * Real.rpow 3 (↑k - ↑j) * Pone + coarseCaccioppoliCenteredBesovGradientFront d s Ceff * Real.rpow 3 (↑k - ↑j) * Psub

The Besov/cutoff-product part of the centered exact coefficient has the two small-cube cutoff gains appearing in the LaTeX proof. The Hessian subterm uses the extra descendant scale in cubeBesovScaleWeight_neg_one_mul_descendantCutoffHessianScaleBound_le_rpow_sub; the gradient subterm uses cubeBesovScaleWeight_neg_one_mul_parent_cutoffGradient_le_rpow_sub.

theorem HCPolySupport.coarseCaccioppoliFluxEnergyExactCenteredBesovCoeffFactorBound_buffered_localAcirc_le_rpow_sub {d : ℕ} {Q R : TriadicCube d} (a : CoeffField d) {s Ceff : ℝ} {k j : ℕ} {ρ₁ ρ₂ : ℝ} (hCeff : 0 ≤ Ceff) (hs : 0 < s) (hs1 : s < 1) (hR : R ∈ descendantsAtDepth Q j) (hchoice : CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂) (hlt : ρ₁ < ρ₂) (hjk : k ≤ j) : have ρm := coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂; have Pone := (LambdaSq R s (MultiscaleExponent.finite 1) a).rpow (1 / 2) * (lambdaSq R 1 (MultiscaleExponent.finite 1) a).rpow (-1 / 2); have Psub := (LambdaSq R s (MultiscaleExponent.finite 1) a).rpow (1 / 2) * (lambdaSq R (1 - s) (MultiscaleExponent.finite 1) a).rpow (-1 / 2); 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) Ceff) ≤ 4 * coarseCaccioppoliCenteredBesovHessianFront d s Ceff * Real.rpow 3 (↑k - ↑j) * Pone + 2 * coarseCaccioppoliCenteredBesovGradientFront d s Ceff * Real.rpow 3 (↑k - ↑j) * Psub

Buffered version of coarseCaccioppoliFluxEnergyExactCenteredBesovCoeffFactorBound_localAcirc_le_rpow_sub. The midpoint cutoff quadruples the Hessian contribution and doubles the gradient contribution, while the triadic scale is still chosen from the full outer gap.