Coarse-graining support:

Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.HarmonicFinal.ExactSmallCube .LocalPatchConstructor.Factors

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

Local-patch exact small-cube factor estimates

This file contains the centered average/Besov factor estimates for the arbitrary-center local-patch exact small-cube coefficient route.

theorem HCPolySupport.coarseCaccioppoliCenteredAverageFactorBound_buffered_localAcircOne_le_rpow_sub {d : ℕ} {Q R : TriadicCube d} (a : CoeffField d) {s Ceff : ℝ} {k j : ℕ} {ρ₁ ρ₂ : ℝ} (hCeff : 0 ≤ Ceff) (hs : 0 < s) (hR : R ∈ descendantsAtDepth Q (j + 1)) (hchoice : CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂) (hlt : ρ₁ < ρ₂) : have ρm := coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂; coarseCaccioppoliFluxEnergyExactCenteredAverageCoeffFactorBound (coarseCaccioppoliLambdaFactor R a s) (coarseCaccioppoliLocalPatchCutoffGradientBound Q ρ₁ ρm) (coarseCaccioppoliCanonicalGradientAcircOne R a ρ₁ ρm) Ceff ≤ ↑d * (3 / 2 * Ceff * 3 ^ (↑d + 1) * ((geometricDiscount s 1)⁻¹ * (geometricDiscount 1 1)⁻¹)) * (4 * quantitativeCubeCutoffGradientConst d * Real.rpow 3 (↑k - ↑j)) * ((LambdaSq R s (MultiscaleExponent.finite 1) a).rpow (1 / 2) * (lambdaSq R 1 (MultiscaleExponent.finite 1) a).rpow (-1 / 2))

Average part of the centered exact coefficient for the local-patch midpoint cutoff. The local cutoff radius and the extra descendant generation combine to give the same normalized front as the centered buffered route.

theorem HCPolySupport.coarseCaccioppoliCenteredBesovFactorBound_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 + 1)) (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 (coarseCaccioppoliLocalPatchCutoffGradientBound Q ρ₁ ρm) (coarseCaccioppoliLocalPatchCutoffHessianBound 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

Besov/cutoff-product part of the centered exact coefficient for the local-patch midpoint cutoff.

theorem HCPolySupport.fluxEnergyExactFactorBounds_localPatch_le_boundaryAlpha {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 + 1)) (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 : (6 * coarseCaccioppoliCenteredAverageFront d s CeffLocal + 12 * coarseCaccioppoliCenteredBesovHessianFront d s CeffLocal + 6 * 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) (coarseCaccioppoliLocalPatchCutoffGradientBound Q ρ₁ ρm) (coarseCaccioppoliCanonicalGradientAcircOne R a ρ₁ ρm) CeffLocal + coarseCaccioppoliFluxEnergyExactCenteredBesovCoeffFactorBound R s (coarseCaccioppoliLambdaFactor R a s) (coarseCaccioppoliLambdaFactor R a s) (coarseCaccioppoliCenteredCutoffCoeffFactorBound R s (coarseCaccioppoliLocalPatchCutoffGradientBound Q ρ₁ ρm) (coarseCaccioppoliLocalPatchCutoffHessianBound Q ρ₁ ρm) (coarseCaccioppoliCanonicalGradientAcircOne R a ρ₁ ρm) (coarseCaccioppoliCanonicalGradientAcircOneSub R a s ρ₁ ρm) CeffLocal) ≤ coarseCaccioppoliBoundaryAlphaOfHeight Q a s t CeffWork hheight ρ₁ ρ₂

Average-plus-Besov factor-bound comparison for the local-patch centered exact coefficient. The extra descendant generation is charged as an extra factor 3 in the centered-front budget.

theorem HCPolySupport.fluxEnergyExactCenteredCoeff_localPatch_le_boundaryAlpha {d : ℕ} [NeZero d] {Q R : TriadicCube d} (center : Vec d) (a : CoeffField d) {s t CeffLocal CeffWork : ℝ} {k j : ℕ} {ρ₁ ρ₂ lam Lam : ℝ} {hheight : ℝ → ℝ → ℝ} (hρ₁_pos : 0 < ρ₁) (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 + 1)) (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 : (6 * coarseCaccioppoliCenteredAverageFront d s CeffLocal + 12 * coarseCaccioppoliCenteredBesovHessianFront d s CeffLocal + 6 * coarseCaccioppoliCenteredBesovGradientFront d s CeffLocal) * Real.rpow 3 ↑k ≤ CeffWork / (s * (1 - s)) * coarseCaccioppoliGapInv ρ₁ ρ₂) (hheight_le_j : hheight ρ₁ ρ₂ ≤ ↑j) : have ρm := coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂; coarseCaccioppoliFluxEnergyExactCenteredCoeff R a s (scalarCutoffGradientField (coarseCaccioppoliLocalCanonicalFun Q center ρ₁ ρm)) (coarseCaccioppoliCanonicalGradientAcircOne R a ρ₁ ρm) (coarseCaccioppoliCanonicalGradientAcircOneSub R a s ρ₁ ρm) (coarseCaccioppoliLocalPatchCutoffHessianBound Q ρ₁ ρm) CeffLocal ≤ coarseCaccioppoliBoundaryAlphaOfHeight Q a s t CeffWork hheight ρ₁ ρ₂

Local-patch exact centered coefficient, with descendant-local canonical A^\circ factors, localized directly to the parent Alpha coefficient. The cutoff is the translated local patch cutoff on the midpoint radius, so the descendant lies one generation deeper than the centered buffered route.