Coarse-graining support:

Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.QuantitativeCutoffInputs.LocalPatch

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

Local-patch cutoff input scalars

This file contains the scalar cutoff bookkeeping for the arbitrary-center local-patch Caccioppoli route. The cutoff lives at radius cubeRadius Q / 3, while descendants are taken one generation deeper than the centered route.

noncomputable def HCPolySupport.coarseCaccioppoliLocalPatchCutoffGradientBound {d : ℕ} (Q : TriadicCube d) (ρ₁ ρ₂ : ℝ) : ℝ

Canonical L∞ gradient bound for the arbitrary-center local-patch cutoff.

Equations

• HCPolySupport.coarseCaccioppoliLocalPatchCutoffGradientBound Q ρ₁ ρ₂ = HCPolySupport.quantitativeCubeCutoffGradientConst d / ((ρ₂ - ρ₁) * (HCPolySupport.cubeRadius Q / 3))

noncomputable def HCPolySupport.coarseCaccioppoliLocalPatchCutoffHessianBound {d : ℕ} (Q : TriadicCube d) (ρ₁ ρ₂ : ℝ) : ℝ

Canonical Hessian bound for the arbitrary-center local-patch cutoff.

Equations

• HCPolySupport.coarseCaccioppoliLocalPatchCutoffHessianBound Q ρ₁ ρ₂ = HCPolySupport.quantitativeCubeCutoffHessianConst d / ((ρ₂ - ρ₁) * (HCPolySupport.cubeRadius Q / 3)) ^ 2

noncomputable def HCPolySupport.coarseCaccioppoliLocalPatchDescendantCutoffHessianScaleBound {d : ℕ} (Q : TriadicCube d) (j : ℕ) (ρ₁ ρ₂ : ℝ) : ℝ

Hessian contribution after the extra local-patch descendant generation.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.cubeScaleFactor_mul_coarseCaccioppoliLocalPatchCutoffHessianBound_eq_descendant {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q (j + 1)) (ρ₁ ρ₂ : ℝ) : cubeScaleFactor R * coarseCaccioppoliLocalPatchCutoffHessianBound Q ρ₁ ρ₂ = coarseCaccioppoliLocalPatchDescendantCutoffHessianScaleBound Q j ρ₁ ρ₂

theorem HCPolySupport.cubeBesovScaleWeight_neg_one_mul_localPatch_buffered_cutoffGradient_eq_depthGap {d : ℕ} {Q R : TriadicCube d} {j : ℕ} {ρ₁ ρ₂ : ℝ} (hR : R ∈ descendantsAtDepth Q (j + 1)) (hlt : ρ₁ < ρ₂) : cubeBesovScaleWeight (-1) R * coarseCaccioppoliLocalPatchCutoffGradientBound Q ρ₁ (coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂) = 4 * quantitativeCubeCutoffGradientConst d * ((3 ^ j)⁻¹ * coarseCaccioppoliGapInv ρ₁ ρ₂)

The local-patch midpoint cutoff has the same normalized gradient size as the parent midpoint cutoff one generation earlier.

theorem HCPolySupport.cubeBesovScaleWeight_neg_one_mul_localPatch_buffered_cutoffGradient_le_rpow_sub {d : ℕ} {Q R : TriadicCube d} {k j : ℕ} {ρ₁ ρ₂ : ℝ} (hR : R ∈ descendantsAtDepth Q (j + 1)) (hchoice : CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂) (hlt : ρ₁ < ρ₂) : cubeBesovScaleWeight (-1) R * coarseCaccioppoliLocalPatchCutoffGradientBound Q ρ₁ (coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂) ≤ 4 * quantitativeCubeCutoffGradientConst d * Real.rpow 3 (↑k - ↑j)

LaTeX-shaped normalized gradient bound for the local-patch midpoint cutoff.

theorem HCPolySupport.cubeBesovScaleWeight_hessianScaleBound_eq_depthGap {d : ℕ} {Q R : TriadicCube d} {j : ℕ} {ρ₁ ρ₂ : ℝ} (hR : R ∈ descendantsAtDepth Q (j + 1)) (hlt : ρ₁ < ρ₂) : cubeBesovScaleWeight (-1) R * coarseCaccioppoliLocalPatchDescendantCutoffHessianScaleBound Q j ρ₁ (coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂) = 16 * quantitativeCubeCutoffHessianConst d * ((3 ^ j)⁻¹ * ((3 ^ j)⁻¹ * coarseCaccioppoliGapInv ρ₁ ρ₂ ^ 2))

Algebraic normal form for the local-patch Hessian contribution in the centered coefficient. The local scale cubeRadius Q / 3 is exactly offset by the extra descendant generation.

theorem HCPolySupport.cubeBesovScaleWeight_hessianScaleBound_le_geometricGap {d : ℕ} {Q R : TriadicCube d} {k j : ℕ} {ρ₁ ρ₂ : ℝ} (hR : R ∈ descendantsAtDepth Q (j + 1)) (hchoice : CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂) (hlt : ρ₁ < ρ₂) (hjk : k ≤ j) : cubeBesovScaleWeight (-1) R * coarseCaccioppoliLocalPatchDescendantCutoffHessianScaleBound Q j ρ₁ (coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂) ≤ 16 * quantitativeCubeCutoffHessianConst d * Real.rpow 3 (↑k - ↑j)

LaTeX-shaped normalized Hessian bound for the local-patch midpoint cutoff.

theorem HCPolySupport.coarseCaccioppoliLocalPatchDescendantBufferedCutoffHessianScaleBound_le_radiusConst_mul_pow {d : ℕ} {Q R : TriadicCube d} {k j : ℕ} {ρ₁ ρ₂ : ℝ} (hR : R ∈ descendantsAtDepth Q (j + 1)) (hchoice : CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂) (hlt : ρ₁ < ρ₂) (hjk : k ≤ j) : cubeScaleFactor R * coarseCaccioppoliLocalPatchCutoffHessianBound Q ρ₁ (coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂) ≤ 12 * (quantitativeCubeCutoffHessianConst d * cubeScaleFactor Q / cubeRadius Q ^ 2) * 3 ^ k

The raw local-patch Hessian bracket in the constant branch is controlled by the full-gap triadic scale.

theorem HCPolySupport.coarseCaccioppoliLocalPatchBufferedCutoffGradientBound_le_radiusConst_mul_pow {d : ℕ} (Q : TriadicCube d) {k : ℕ} {ρ₁ ρ₂ : ℝ} (hchoice : CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂) (hlt : ρ₁ < ρ₂) : coarseCaccioppoliLocalPatchCutoffGradientBound Q ρ₁ (coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂) ≤ 6 * (quantitativeCubeCutoffGradientConst d / cubeRadius Q) * 3 ^ k

Raw local-patch gradient bound for the constant branch.

theorem HCPolySupport.cubeBesovScaleWeight_neg_one_mul_localPatch_buffered_cutoff_terms_le_radiusConst_mul_pow {d : ℕ} {Q R : TriadicCube d} {k j : ℕ} {ρ₁ ρ₂ : ℝ} (hR : R ∈ descendantsAtDepth Q (j + 1)) (hchoice : CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂) (hlt : ρ₁ < ρ₂) (hjk : k ≤ j) : cubeBesovScaleWeight (-1) R * (coarseCaccioppoliLocalPatchCutoffHessianBound Q ρ₁ (coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂) + cubeBesovScaleWeight 1 R * coarseCaccioppoliLocalPatchCutoffGradientBound Q ρ₁ (coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂)) ≤ (12 * (quantitativeCubeCutoffHessianConst d * cubeScaleFactor Q / cubeRadius Q ^ 2) + 6 * (quantitativeCubeCutoffGradientConst d / cubeRadius Q)) * 3 ^ k

Descendant form of the local-patch buffered cutoff bracket used by the constant branch.

theorem HCPolySupport.coarseCaccioppoliFactorBound_mul_bufferedTerms_le_boundaryCoefficient_of_child {d : ℕ} {Q R : TriadicCube d} (a : CoeffField d) {Ceff : ℝ} {k j : ℕ} {ρ₁ ρ₂ : ℝ} (hR : R ∈ descendantsAtDepth Q (j + 1)) (hchoice : CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂) (hlt : ρ₁ < ρ₂) (hjk : k ≤ j) (hlarge : ↑d * 3 ^ (↑d + 1) * (geometricDiscount 1 1)⁻¹ * (12 * (quantitativeCubeCutoffHessianConst d * cubeScaleFactor Q / cubeRadius Q ^ 2) + 6 * (quantitativeCubeCutoffGradientConst d / cubeRadius Q)) ≤ Ceff) : coarseCaccioppoliFluxEnergyExactConstantCoeffFactorBound R (coarseCaccioppoliLambdaFactor R a 1) (coarseCaccioppoliLambdaFactor R a 1) * (coarseCaccioppoliLocalPatchCutoffHessianBound Q ρ₁ (coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂) + cubeBesovScaleWeight 1 R * coarseCaccioppoliLocalPatchCutoffGradientBound Q ρ₁ (coarseCaccioppoliBufferedCutoffRadius ρ₁ ρ₂)) ≤ coarseCaccioppoliSingleCubeBoundaryConstantBaseCoeff R a Ceff ↑k

Constant-branch exact coefficient comparison for the arbitrary-center local-patch midpoint cutoff. The cutoff is supported on the m-1 patch, so descendants are taken one generation deeper than the height depth.