Documentation

LeanPool.HighContrastHomogenization.Support.CoarseGraining.OriginCubeEllipticRecovery.Subadditivity

Coarse-graining support: Support.CoarseGraining.OriginCubeEllipticRecovery.Subadditivity #

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

Origin-cube elliptic recovery -- subadditivity wrappers #

These wrappers package the descendant deterministic-coarse-data burden behind either OpenCubeDescendantDeterministicCoarseData or the stronger recovery- family hypothesis. This is the note-facing surface downstream Chapter-3 consumers should use, rather than unpacking the individual coarse witnesses by hand.

source
theorem HCPolySupport.coarseMatrix_subadditive_cube_descendants_in_loewner_of_deterministicCoarseData {d : ℕ} (j : ℕ) (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : OpenCubeDescendantDeterministicCoarseData Q a) :
BlockMatLoewnerLE (coarseBlockMatrix (openCubeSet Q) a) (descendantsAverageBlockMat Q j fun (R : TriadicCube d) => coarseBlockMatrix (openCubeSet R) a)

Subadditivity of the coarse block matrix in Loewner order, packaged from deterministic coarse data on all descendants.

source
theorem HCPolySupport.coarseStarredBlockMatrixInv_subadditive_cubeDescendants_in_loewner_order {d : ℕ} (j : ℕ) (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : OpenCubeDescendantDeterministicCoarseData Q a) :
BlockMatLoewnerLE (coarseStarredBlockMatrixInv (openCubeSet Q) a) (descendantsAverageBlockMat Q j fun (R : TriadicCube d) => coarseStarredBlockMatrixInv (openCubeSet R) a)

Subadditivity of the inverse starred block matrix in Loewner order, packaged from deterministic coarse data on all descendants.

source
theorem HCPolySupport.sigmaStarInvCoarse_subadditive_cube_descendants_in_of_deterministicCoarseData {d : ℕ} (j : ℕ) (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : OpenCubeDescendantDeterministicCoarseData Q a) :
MatLoewnerLE (sigmaStarInvCoarse (openCubeSet Q) a) (descendantsAverageMat Q j fun (R : TriadicCube d) => sigmaStarInvCoarse (openCubeSet R) a)

Subadditivity of σ_*^{-1} in Loewner order, packaged from deterministic coarse data on all descendants.

source
theorem HCPolySupport.bCoarse_subadditive_openCubeSet_descendantsAtDepth_in_loewner_order_of_deterministicCoarseData {d : ℕ} (j : ℕ) (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : OpenCubeDescendantDeterministicCoarseData Q a) :
MatLoewnerLE (bCoarse (sigmaCoarse (openCubeSet Q) a) (sigmaStarCoarse (openCubeSet Q) a) (kappaCoarse (openCubeSet Q) a)) (descendantsAverageMat Q j fun (R : TriadicCube d) => bCoarse (sigmaCoarse (openCubeSet R) a) (sigmaStarCoarse (openCubeSet R) a) (kappaCoarse (openCubeSet R) a))

Subadditivity of the canonical b-matrix in Loewner order, packaged from deterministic coarse data on all descendants.

source
theorem HCPolySupport.coarseBlockMatrix_subadditive_openCubeSet_descendantsAtDepth_in_loewner_order_of_recoveryFamily {d : ℕ} (j : ℕ) (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hRec : OpenCubeDescendantEllipticRecoveryFamily Q a) :
BlockMatLoewnerLE (coarseBlockMatrix (openCubeSet Q) a) (descendantsAverageBlockMat Q j fun (R : TriadicCube d) => coarseBlockMatrix (openCubeSet R) a)

Recovery-family wrapper for coarse-block-matrix subadditivity in Loewner order.

source
theorem HCPolySupport.coarseStarredBlockMatrixInv_subadditive_cubeDescendants_in_of_recoveryFamily {d : ℕ} (j : ℕ) (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hRec : OpenCubeDescendantEllipticRecoveryFamily Q a) :
BlockMatLoewnerLE (coarseStarredBlockMatrixInv (openCubeSet Q) a) (descendantsAverageBlockMat Q j fun (R : TriadicCube d) => coarseStarredBlockMatrixInv (openCubeSet R) a)

Recovery-family wrapper for inverse-starred-block-matrix subadditivity in Loewner order.

source
theorem HCPolySupport.sigmaStarInvCoarse_subadditive_openCubeSet_descendantsAtDepth_in_loewner_order_of_recoveryFamily {d : ℕ} (j : ℕ) (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hRec : OpenCubeDescendantEllipticRecoveryFamily Q a) :
MatLoewnerLE (sigmaStarInvCoarse (openCubeSet Q) a) (descendantsAverageMat Q j fun (R : TriadicCube d) => sigmaStarInvCoarse (openCubeSet R) a)

Recovery-family wrapper for σ_*^{-1} subadditivity in Loewner order.

source
theorem HCPolySupport.bCoarse_subadditive_openCubeSet_descendantsAtDepth_in_loewner_order_of_recoveryFamily {d : ℕ} (j : ℕ) (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hRec : OpenCubeDescendantEllipticRecoveryFamily Q a) :
MatLoewnerLE (bCoarse (sigmaCoarse (openCubeSet Q) a) (sigmaStarCoarse (openCubeSet Q) a) (kappaCoarse (openCubeSet Q) a)) (descendantsAverageMat Q j fun (R : TriadicCube d) => bCoarse (sigmaCoarse (openCubeSet R) a) (sigmaStarCoarse (openCubeSet R) a) (kappaCoarse (openCubeSet R) a))

Recovery-family wrapper for canonical b-matrix subadditivity in Loewner order.