Coarse-graining support:

Support.Book.Ch05.Theorems.Section56.VarianceEstimateQuadratic.MatrixTools

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

theorem HCPolySupport.Book.Ch05.Section56.normalizedInvSqrtBlockProbe_inl_eq {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (i : Fin d) : normalizedInvSqrtBlockProbe hP hStruct center (Sum.inl i) = ((√(hP.barSigmaAtScale hStruct center))⁻¹ • Pi.single i 1, 0)

theorem HCPolySupport.Book.Ch05.Section56.normalizedSqrtBlockProbe_inl_eq {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (i : Fin d) : normalizedSqrtBlockProbe hP hStruct center (Sum.inl i) = (√(hP.barSigmaAtScale hStruct center) • Pi.single i 1, 0)

theorem HCPolySupport.Book.Ch05.Section56.fullBlockOperatorNorm_le_trace_of_posSemidef {d : ℕ} (M : FullBlockMat d) (hM : Matrix.PosSemidef M) : ‖Matrix.toEuclideanCLM M‖ ≤ Ch02.fullBlockTrace M

theorem HCPolySupport.Book.Ch05.Section56.fullBlockOperatorNormSq_le_trace_sq_of_posSemidef {d : ℕ} (M : FullBlockMat d) (hM : Matrix.PosSemidef M) : ‖Matrix.toEuclideanCLM M‖ ^ 2 ≤ Ch02.fullBlockTrace M ^ 2

theorem HCPolySupport.Book.Ch05.Section56.blockSub_posSemidef_of_blockMatLoewnerLE {d : ℕ} {A B : BlockMat d} (hAB : BlockMatLoewnerLE A B) (hA : IsSymmetricBlockMat A) (hB : IsSymmetricBlockMat B) : Matrix.PosSemidef (toFullBlockMat B - toFullBlockMat A)

theorem HCPolySupport.Book.Ch05.Section56.transpose_blockSub_posSemidef_of_blockMatLoewnerLE {d : ℕ} (S : FullBlockMat d) {A B : BlockMat d} (hAB : BlockMatLoewnerLE A B) (hA : IsSymmetricBlockMat A) (hB : IsSymmetricBlockMat B) : (Matrix.transpose S * (toFullBlockMat B - toFullBlockMat A) * S).PosSemidef

theorem HCPolySupport.Book.Ch05.Section56.diagonal_blockSub_posSemidef_of_blockMatLoewnerLE {d : ℕ} {A B : BlockMat d} (r : BlockCoord d → ℝ) (hAB : BlockMatLoewnerLE A B) (hA : IsSymmetricBlockMat A) (hB : IsSymmetricBlockMat B) : (Matrix.diagonal r * (toFullBlockMat B - toFullBlockMat A) * Matrix.diagonal r).PosSemidef

theorem HCPolySupport.Book.Ch05.Section56.toFullBlockMat_descendantsAverageBlockMat {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F : TriadicCube d → BlockMat d) : toFullBlockMat (descendantsAverageBlockMat Q j F) = descendantsAverageFullBlockMat Q j fun (R : TriadicCube d) => toFullBlockMat (F R)

theorem HCPolySupport.Book.Ch05.Section56.descendantsAverageFullBlockMat_eq_smul_sum {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F : TriadicCube d → FullBlockMat d) : descendantsAverageFullBlockMat Q j F = (↑(descendantsAtDepth Q j).card)⁻¹ • (descendantsAtDepth Q j).sum F

theorem HCPolySupport.Book.Ch05.Section56.descendantsAverageFullBlockMat_const {d : ℕ} (Q : TriadicCube d) (j : ℕ) (M : FullBlockMat d) : (descendantsAverageFullBlockMat Q j fun (x : TriadicCube d) => M) = M

theorem HCPolySupport.Book.Ch05.Section56.descendantsAverageFullBlockMat_sub {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F G : TriadicCube d → FullBlockMat d) : (descendantsAverageFullBlockMat Q j fun (R : TriadicCube d) => F R - G R) = descendantsAverageFullBlockMat Q j F - descendantsAverageFullBlockMat Q j G

def HCPolySupport.Book.Ch05.Section56.diagonalCongrLinearMap {d : ℕ} (D : FullBlockMat d) : FullBlockMat d →ₗ[ℝ] FullBlockMat d

Linear map multiplying a full block matrix on both sides by a fixed matrix.

Equations

• HCPolySupport.Book.Ch05.Section56.diagonalCongrLinearMap D = { toFun := fun (M : HCPolySupport.FullBlockMat d) => D * M * D, map_add' := ⋯, map_smul' := ⋯ }

def HCPolySupport.Book.Ch05.Section56.transposeCongrLinearMap {d : ℕ} (S : FullBlockMat d) : FullBlockMat d →ₗ[ℝ] FullBlockMat d

Linear congruence map sending a matrix M to Sᵀ * M * S for a fixed matrix S.

Equations

• HCPolySupport.Book.Ch05.Section56.transposeCongrLinearMap S = { toFun := fun (M : HCPolySupport.FullBlockMat d) => Matrix.transpose S * M * S, map_add' := ⋯, map_smul' := ⋯ }

theorem HCPolySupport.Book.Ch05.Section56.descendantsAverageFullBlockMat_linearMap {d : ℕ} (Q : TriadicCube d) (j : ℕ) (L : FullBlockMat d →ₗ[ℝ] FullBlockMat d) (F : TriadicCube d → FullBlockMat d) : (descendantsAverageFullBlockMat Q j fun (R : TriadicCube d) => L (F R)) = L (descendantsAverageFullBlockMat Q j F)

theorem HCPolySupport.Book.Ch05.Section56.descendantsAverageFullBlockMat_diagonal_sub_const_mul_diagonal {d : ℕ} (Q : TriadicCube d) (j : ℕ) (D C : FullBlockMat d) (F : TriadicCube d → FullBlockMat d) : (descendantsAverageFullBlockMat Q j fun (R : TriadicCube d) => D * (F R - C) * D) = D * (descendantsAverageFullBlockMat Q j F - C) * D

theorem HCPolySupport.Book.Ch05.Section56.descendantsAverageFullBlockMat_transpose_sub_const_mul {d : ℕ} (Q : TriadicCube d) (j : ℕ) (S C : FullBlockMat d) (F : TriadicCube d → FullBlockMat d) : (descendantsAverageFullBlockMat Q j fun (R : TriadicCube d) => Matrix.transpose S * (F R - C) * S) = Matrix.transpose S * (descendantsAverageFullBlockMat Q j F - C) * S

theorem HCPolySupport.Book.Ch05.Section56.normalizedCoarseAveragePositiveErrorMatrix_eq_diagonal_blockSub {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (Q : TriadicCube d) (j : ℕ) (a : RegCoeffField d) : have b := hP.barSigmaAtScale hStruct center; have c := hP.barSigmaStarAtScale hStruct center; have D := Matrix.diagonal (Ch04.scalarFullBlockInvSqrtDiag b c); normalizedCoarseAveragePositiveErrorMatrix hP hStruct center Q j a = D * (toFullBlockMat (descendantsAverageBlockMat Q j fun (R : TriadicCube d) => coarseBlockMatrix (cubeSet R) a.toFun) - toFullBlockMat (coarseBlockMatrix (cubeSet Q) a.toFun)) * D

theorem HCPolySupport.Book.Ch05.Section56.coarseAveragePositiveErrorMatrixWithNormalizer_eq_transpose_blockSub {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (center : ℤ) (S : FullBlockMat d) (Q : TriadicCube d) (j : ℕ) (a : RegCoeffField d) : coarseAveragePositiveErrorMatrixWithNormalizer hP hStruct center S Q j a = Matrix.transpose S * (toFullBlockMat (descendantsAverageBlockMat Q j fun (R : TriadicCube d) => coarseBlockMatrix (cubeSet R) a.toFun) - toFullBlockMat (coarseBlockMatrix (cubeSet Q) a.toFun)) * S