Coarse-graining support: #
Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.QuantitativeCutoffInputs.Setup.ConstantCoeff
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Quantitative cutoff inputs: constant coefficient comparisons #
theorem
HCPolySupport.coarseCaccioppoliFactorBound_mul_parentCutoffTerms_le_boundaryCoefficient
{d : ℕ}
{Q R : TriadicCube d}
(a : CoeffField d)
{Ceff : ℝ}
{k j : ℕ}
{ρ₁ ρ₂ : ℝ}
(hR : R ∈ descendantsAtDepth Q j)
(hchoice : CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂)
(hlt : ρ₁ < ρ₂)
(hjk : k ≤ j)
(hlarge :
↑d * 3 ^ (↑d + 1) * (geometricDiscount 1 1)⁻¹ * (quantitativeCubeCutoffHessianConst d * cubeScaleFactor Q / cubeRadius Q ^ 2 + quantitativeCubeCutoffGradientConst d / cubeRadius Q) ≤ Ceff)
:
coarseCaccioppoliFluxEnergyExactConstantCoeffFactorBound R (coarseCaccioppoliLambdaFactor R a 1)
(coarseCaccioppoliLambdaFactor R a 1) * (coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ ρ₂ + cubeBesovScaleWeight 1 R * coarseCaccioppoliQuantitativeCutoffGradientBound Q ρ₁ ρ₂) ≤ coarseCaccioppoliSingleCubeBoundaryConstantBaseCoeff R a Ceff ↑k
Constant-branch exact coefficient comparison on a descendant cube, after the parent cutoff constants have been converted to the note's triadic scale.
The only scalar input is the expected fixed-constant calibration: the local
constant Ceff dominates the dimension/geometric-discount factor times the
parent-radius cutoff front.
theorem
HCPolySupport.coarseCaccioppoliFactorBound_mul_bufferedCutoffTerms_le_of_descendant
{d : ℕ}
{Q R : TriadicCube d}
(a : CoeffField d)
{Ceff : ℝ}
{k j : ℕ}
{ρ₁ ρ₂ : ℝ}
(hR : R ∈ descendantsAtDepth Q j)
(hchoice : CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂)
(hlt : ρ₁ < ρ₂)
(hjk : k ≤ j)
(hlarge :
↑d * 3 ^ (↑d + 1) * (geometricDiscount 1 1)⁻¹ * (4 * (quantitativeCubeCutoffHessianConst d * cubeScaleFactor Q / cubeRadius Q ^ 2) + 2 * (quantitativeCubeCutoffGradientConst d / cubeRadius Q)) ≤ Ceff)
:
coarseCaccioppoliFluxEnergyExactConstantCoeffFactorBound R (coarseCaccioppoliLambdaFactor R a 1)
(coarseCaccioppoliLambdaFactor R a 1) * (coarseCaccioppoliQuantitativeCutoffHessianBound Q ρ₁ (coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂) + cubeBesovScaleWeight 1 R * coarseCaccioppoliQuantitativeCutoffGradientBound Q ρ₁ (coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂)) ≤ coarseCaccioppoliSingleCubeBoundaryConstantBaseCoeff R a Ceff ↑k
Buffered constant-branch exact coefficient comparison on a descendant cube.
The midpoint cutoff uses the full-gap triadic scale but requires the inflated
fixed cutoff front 4 * Hessian + 2 * Gradient.