Documentation

LeanPool.HighContrastHomogenization.Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.HarmonicFinal.InputSpecializations.LocalPatchNoteRawBridge.CoefficientBounds

Coarse-graining support: #

Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.HarmonicFinal.InputSpecializations .LocalPatchNoteRawBridge.CoefficientBounds

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

Local-patch note raw bridge #

This sidecar ties the arbitrary-center local-patch descendant summation to the harmonic weak-testing identity. It covers the interior-contained local patch case: the translated cutoff support is required to lie inside the parent open cube, so the compact-support test function is admissible without a boundary zero-trace argument.

source
def HCPolySupport.boundaryCaccioppoliSmallCubeLocalPatchCoefficientSplit {d : ℕ} (Q : TriadicCube d) (center : Vec d) (a : CoeffField d) (s t Clocal Calpha Ccross : ℝ) :
Prop

Split exact-to-parent-raw coefficient comparisons for the arbitrary-center local patch route.

Calpha controls the centered/front branch and may carry the small-s front budget. Ccross controls only the local constant/cross branch, so the later note-facing constant can stay dimension-only in that branch.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def HCPolySupport.boundaryCaccioppoliSmallCubeLocalPatchCoefficientSplitAllRadii {d : ℕ} (Q : TriadicCube d) (center : Vec d) (a : CoeffField d) (s t Clocal Calpha Ccross : ℝ) :
    Prop

    All-radii split exact-to-parent-raw coefficient comparisons for the arbitrary-center local-patch route. This is the coefficient package needed by the standard beta-dependent radius iteration.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem HCPolySupport.boundaryCaccioppoliSmallCubeLocalPatchCoefficientSplit.of_allRadii {d : ℕ} (Q : TriadicCube d) (center : Vec d) (a : CoeffField d) (s t Clocal Calpha Ccross : ℝ) (h : boundaryCaccioppoliSmallCubeLocalPatchCoefficientSplitAllRadii Q center a s t Clocal Calpha Ccross) :
      boundaryCaccioppoliSmallCubeLocalPatchCoefficientSplit Q center a s t Clocal Calpha Ccross

      The all-radii local-patch split coefficient package restricts to the legacy Chapter-3 radius sequence.