Coarse-graining support: Support.CoarseGraining.Subadditivity

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

Subadditivity and scaling results for the deterministic coarse objects.

This file is reserved for the theorem families implementing the Chapter-2 note label l.cg.subadditivity.basic.definitions together with the downstream block-matrix subadditivity consequences.

Planned theorem-family prefixes:

• responseJ_subadditive_*
• coarseBlockMatrix_subadditive_*
• coarseStarredBlockMatrixInv_subadditive_*

theorem HCPolySupport.descendantsAverage_add {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F G : TriadicCube d → ℝ) : (descendantsAverage Q j fun (R : TriadicCube d) => F R + G R) = descendantsAverage Q j F + descendantsAverage Q j G

theorem HCPolySupport.descendantsAverage_smul {d : ℕ} (Q : TriadicCube d) (j : ℕ) (c : ℝ) (F : TriadicCube d → ℝ) : (descendantsAverage Q j fun (R : TriadicCube d) => c * F R) = c * descendantsAverage Q j F

noncomputable def HCPolySupport.descendantsAverageMat {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F : TriadicCube d → Mat d) : Mat d

Entrywise descendants average of a matrix-valued observable on the depth-j descendants of Q.

Equations

• HCPolySupport.descendantsAverageMat Q j F i k = HCPolySupport.descendantsAverage Q j fun (R : HCPolySupport.TriadicCube d) => F R i k

noncomputable def HCPolySupport.descendantsAverageBlockMat {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F : TriadicCube d → BlockMat d) : BlockMat d

Entrywise descendants average of a block-matrix-valued observable on the depth-j descendants of Q.

Equations

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

theorem HCPolySupport.matVecMul_descendantsAverageMat {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F : TriadicCube d → Mat d) (x : Vec d) : matVecMul (descendantsAverageMat Q j F) x = fun (i : Fin d) => descendantsAverage Q j fun (R : TriadicCube d) => matVecMul (F R) x i

theorem HCPolySupport.vecDot_matVecMul_descendantsAverageMat {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F : TriadicCube d → Mat d) (x y : Vec d) : vecDot x (matVecMul (descendantsAverageMat Q j F) y) = descendantsAverage Q j fun (R : TriadicCube d) => vecDot x (matVecMul (F R) y)

theorem HCPolySupport.blockVecDot_blockMatVecMul_descendantsAverageBlockMat {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F : TriadicCube d → BlockMat d) (X Y : BlockVec d) : blockVecDot X (blockMatVecMul (descendantsAverageBlockMat Q j F) Y) = descendantsAverage Q j fun (R : TriadicCube d) => blockVecDot X (blockMatVecMul (F R) Y)

theorem HCPolySupport.responseJ_subadditive_openCubeSet_childCubes_of_isEllipticFieldOn {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (p q : Vec d) : ResponseJ (openCubeSet Q) p q a ≤ descendantsAverage Q 1 fun (R : TriadicCube d) => ResponseJ (openCubeSet R) p q a

theorem HCPolySupport.responseJ_subadditive_openCubeSet_originCube_childCubes_of_isEllipticFieldOn {d : ℕ} (n : ℤ) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet (originCube d n)) a) (p q : Vec d) : ResponseJ (openCubeSet (originCube d n)) p q a ≤ descendantsAverage (originCube d n) 1 fun (R : TriadicCube d) => ResponseJ (openCubeSet R) p q a

theorem HCPolySupport.responseJ_subadditive_openCubeSet_descendantsAtDepth_of_isEllipticFieldOn {d : ℕ} (j : ℕ) (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (p q : Vec d) : ResponseJ (openCubeSet Q) p q a ≤ descendantsAverage Q j fun (R : TriadicCube d) => ResponseJ (openCubeSet R) p q a

theorem HCPolySupport.responseJ_subadditive_cubeSet_childCubes_of_isEllipticFieldOn {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (p q : Vec d) : ResponseJ (cubeSet Q) p q a ≤ descendantsAverage Q 1 fun (R : TriadicCube d) => ResponseJ (cubeSet R) p q a

theorem HCPolySupport.responseJ_subadditive_cubeSet_descendantsAtDepth_of_isEllipticFieldOn {d : ℕ} [NeZero d] (j : ℕ) (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (p q : Vec d) : ResponseJ (cubeSet Q) p q a ≤ descendantsAverage Q j fun (R : TriadicCube d) => ResponseJ (cubeSet R) p q a

theorem HCPolySupport.responseJ_subadditive_openCubeSet_originCube_descendantsAtDepth_of_isEllipticFieldOn {d : ℕ} (j : ℕ) (n : ℤ) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet (originCube d n)) a) (p q : Vec d) : ResponseJ (openCubeSet (originCube d n)) p q a ≤ descendantsAverage (originCube d n) j fun (R : TriadicCube d) => ResponseJ (openCubeSet R) p q a

theorem HCPolySupport.responseJ_subadditive_cubeSet_originCube_childCubes_of_isEllipticFieldOn {d : ℕ} [NeZero d] (n : ℤ) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet (originCube d n)) a) (p q : Vec d) : ResponseJ (cubeSet (originCube d n)) p q a ≤ descendantsAverage (originCube d n) 1 fun (R : TriadicCube d) => ResponseJ (cubeSet R) p q a

theorem HCPolySupport.responseJ_subadditive_cubeSet_originCube_descendantsAtDepth_of_isEllipticFieldOn {d : ℕ} [NeZero d] (j : ℕ) (n : ℤ) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet (originCube d n)) a) (p q : Vec d) : ResponseJ (cubeSet (originCube d n)) p q a ≤ descendantsAverage (originCube d n) j fun (R : TriadicCube d) => ResponseJ (cubeSet R) p q a

theorem HCPolySupport.coarseBlockMatrix_subadditive_openCubeSet_descendantsAtDepth_pair_of_responseJ_blockQuadratic {d : ℕ} (j : ℕ) (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hRespQ : ∀ (p q : Vec d), ResponseJ (openCubeSet Q) p q a = 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (coarseBlockMatrix (openCubeSet Q) a) (-p, q)) - vecDot p q) (hRespDesc : ∀ R ∈ descendantsAtDepth Q j, ∀ (p q : Vec d), ResponseJ (openCubeSet R) p q a = 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (coarseBlockMatrix (openCubeSet R) a) (-p, q)) - vecDot p q) (p q : Vec d) : 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (coarseBlockMatrix (openCubeSet Q) a) (-p, q)) ≤ descendantsAverage Q j fun (R : TriadicCube d) => 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (coarseBlockMatrix (openCubeSet R) a) (-p, q))

theorem HCPolySupport.coarseMatrix_subadditive_cube_descendants_blockQuadratic {d : ℕ} (j : ℕ) (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hRespQ : ∀ (p q : Vec d), ResponseJ (openCubeSet Q) p q a = 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (coarseBlockMatrix (openCubeSet Q) a) (-p, q)) - vecDot p q) (hRespDesc : ∀ R ∈ descendantsAtDepth Q j, ∀ (p q : Vec d), ResponseJ (openCubeSet R) p q a = 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (coarseBlockMatrix (openCubeSet R) a) (-p, q)) - vecDot p q) (X : BlockVec d) : 1 / 2 * blockVecDot X (blockMatVecMul (coarseBlockMatrix (openCubeSet Q) a) X) ≤ descendantsAverage Q j fun (R : TriadicCube d) => 1 / 2 * blockVecDot X (blockMatVecMul (coarseBlockMatrix (openCubeSet R) a) X)

theorem HCPolySupport.coarseMatrix_subadditive_cube_descendants_in_loewner_order_of_blockQuadratic {d : ℕ} (j : ℕ) (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hRespQ : ∀ (p q : Vec d), ResponseJ (openCubeSet Q) p q a = 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (coarseBlockMatrix (openCubeSet Q) a) (-p, q)) - vecDot p q) (hRespDesc : ∀ R ∈ descendantsAtDepth Q j, ∀ (p q : Vec d), ResponseJ (openCubeSet R) p q a = 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (coarseBlockMatrix (openCubeSet R) a) (-p, q)) - vecDot p q) : BlockMatLoewnerLE (coarseBlockMatrix (openCubeSet Q) a) (descendantsAverageBlockMat Q j fun (R : TriadicCube d) => coarseBlockMatrix (openCubeSet R) a)

theorem HCPolySupport.coarseStarredBlockMatrixInv_subadditive_cubeDescendants_of_blockQuadratic {d : ℕ} (j : ℕ) (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hRespQ : ∀ (p q : Vec d), ResponseJ (openCubeSet Q) p q a = 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (coarseBlockMatrix (openCubeSet Q) a) (-p, q)) - vecDot p q) (hRespDesc : ∀ R ∈ descendantsAtDepth Q j, ∀ (p q : Vec d), ResponseJ (openCubeSet R) p q a = 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (coarseBlockMatrix (openCubeSet R) a) (-p, q)) - vecDot p q) (X : BlockVec d) : 1 / 2 * blockVecDot X (blockMatVecMul (coarseStarredBlockMatrixInv (openCubeSet Q) a) X) ≤ descendantsAverage Q j fun (R : TriadicCube d) => 1 / 2 * blockVecDot X (blockMatVecMul (coarseStarredBlockMatrixInv (openCubeSet R) a) X)

theorem HCPolySupport.coarseStarredBlockMatrixInv_subadditive_cubeDescendants_in_loewner_of_responseJ {d : ℕ} (j : ℕ) (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hRespQ : ∀ (p q : Vec d), ResponseJ (openCubeSet Q) p q a = 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (coarseBlockMatrix (openCubeSet Q) a) (-p, q)) - vecDot p q) (hRespDesc : ∀ R ∈ descendantsAtDepth Q j, ∀ (p q : Vec d), ResponseJ (openCubeSet R) p q a = 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (coarseBlockMatrix (openCubeSet R) a) (-p, q)) - vecDot p q) : BlockMatLoewnerLE (coarseStarredBlockMatrixInv (openCubeSet Q) a) (descendantsAverageBlockMat Q j fun (R : TriadicCube d) => coarseStarredBlockMatrixInv (openCubeSet R) a)

theorem HCPolySupport.coarseStarredBlockMatrixInv_upperLeft_subadditive_cubeDescendants {d : ℕ} (j : ℕ) (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hRespQ : ∀ (p q : Vec d), ResponseJ (openCubeSet Q) p q a = 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (coarseBlockMatrix (openCubeSet Q) a) (-p, q)) - vecDot p q) (hRespDesc : ∀ R ∈ descendantsAtDepth Q j, ∀ (p q : Vec d), ResponseJ (openCubeSet R) p q a = 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (coarseBlockMatrix (openCubeSet R) a) (-p, q)) - vecDot p q) (p : Vec d) : 1 / 2 * vecDot p (matVecMul (coarseStarredBlockMatrixInv (openCubeSet Q) a).upperLeft p) ≤ descendantsAverage Q j fun (R : TriadicCube d) => 1 / 2 * vecDot p (matVecMul (coarseStarredBlockMatrixInv (openCubeSet R) a).upperLeft p)

theorem HCPolySupport.coarseStarredBlockMatrixInv_lowerRight_subadditive_cubeDescendants {d : ℕ} (j : ℕ) (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hRespQ : ∀ (p q : Vec d), ResponseJ (openCubeSet Q) p q a = 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (coarseBlockMatrix (openCubeSet Q) a) (-p, q)) - vecDot p q) (hRespDesc : ∀ R ∈ descendantsAtDepth Q j, ∀ (p q : Vec d), ResponseJ (openCubeSet R) p q a = 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (coarseBlockMatrix (openCubeSet R) a) (-p, q)) - vecDot p q) (q : Vec d) : 1 / 2 * vecDot q (matVecMul (coarseStarredBlockMatrixInv (openCubeSet Q) a).lowerRight q) ≤ descendantsAverage Q j fun (R : TriadicCube d) => 1 / 2 * vecDot q (matVecMul (coarseStarredBlockMatrixInv (openCubeSet R) a).lowerRight q)