Documentation

LeanPool.HighContrastHomogenization.Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.HarmonicFinal.InputSpecializations.NoteRawBridge.CoefficientLocalization

Coarse-graining support: #

Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.HarmonicFinal.InputSpecializations .NoteRawBridge.CoefficientLocalization

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

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

Split exact-to-parent-raw coefficient comparisons for the buffered localized-energy route.

The explicit height and absorption coefficient are chosen with Calpha, while the constant/cross branch is charged to Ccross. This is the coefficient surface needed to keep the public note constant split all the way back to the small-cube estimates.

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

    All-radii split exact-to-parent-raw coefficient comparisons for the buffered localized-energy 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.BoundaryCaccioppoliHarmonicVectorSmallCubeCoefficientSplit.of_allRadii {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t Clocal Calpha Ccross : ℝ) (h : boundaryCaccioppoliSmallCubeCoefficientSplitAllRadii Q a s t Clocal Calpha Ccross) :
      BoundaryCaccioppoliHarmonicVectorSmallCubeCoefficientSplit Q a s t Clocal Calpha Ccross

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