Coarse-graining support:

Support.Book.Ch05.Theorems.Section56.VarianceEstimateQuadratic.TraceBudget

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

noncomputable def HCPolySupport.Book.Ch05.Section56.fullBlockJTraceBudgetWithNormalizers {d : ℕ} (S T : FullBlockMat d) (A : BlockMat d) : ℝ

Sum of half-weighted quadratic responses for two normalizers, with reflection in the second response and subtraction of their mixed pairing.

Equations

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

theorem HCPolySupport.Book.Ch05.Section56.sum_doubledResponseJ_fullBlockNormalizers_eq_traceBudget {d : ℕ} (U : Ch02.Domain d) (a : Ch02.CoeffOn U) (S T : FullBlockMat d) : ∑ α : BlockCoord d, Ch02.doubledResponseJ U a (fullBlockMatrixProbe S α) (fullBlockMatrixProbe T α) = fullBlockJTraceBudgetWithNormalizers S T (Ch02.coarseBlockMatrix U a)

theorem HCPolySupport.Book.Ch05.Section56.weightedAverage_const_mul' {d : ℕ} {U : Ch02.Domain d} (Pcell : Ch02.DomainPartition U) (c : ℝ) (f : Pcell.Cell → ℝ) : (Pcell.weightedAverage fun (i : Pcell.Cell) => c * f i) = c * Pcell.weightedAverage f

theorem HCPolySupport.Book.Ch05.Section56.vecDot_matVecMul_weightedMatAverage' {d : ℕ} {U : Ch02.Domain d} (Pcell : Ch02.DomainPartition U) (F : Pcell.Cell → Mat d) (x y : Vec d) : vecDot x (matVecMul (Pcell.weightedMatAverage F) y) = Pcell.weightedAverage fun (i : Pcell.Cell) => vecDot x (matVecMul (F i) y)

theorem HCPolySupport.Book.Ch05.Section56.blockVecDot_blockMatVecMul_weightedBlockAverage' {d : ℕ} {U : Ch02.Domain d} (Pcell : Ch02.DomainPartition U) (F : Pcell.Cell → BlockMat d) (X : BlockVec d) : blockVecDot X (blockMatVecMul (Pcell.weightedBlockAverage F) X) = Pcell.weightedAverage fun (c : Pcell.Cell) => blockVecDot X (blockMatVecMul (F c) X)

theorem HCPolySupport.Book.Ch05.Section56.blockReflect_weightedBlockAverage {d : ℕ} {U : Ch02.Domain d} (Pcell : Ch02.DomainPartition U) (F : Pcell.Cell → BlockMat d) : blockReflect (Pcell.weightedBlockAverage F) = Pcell.weightedBlockAverage fun (c : Pcell.Cell) => blockReflect (F c)

theorem HCPolySupport.Book.Ch05.Section56.blockVecDot_blockReflect_weightedBlockAverage' {d : ℕ} {U : Ch02.Domain d} (Pcell : Ch02.DomainPartition U) (F : Pcell.Cell → BlockMat d) (X : BlockVec d) : blockVecDot X (blockMatVecMul (blockReflect (Pcell.weightedBlockAverage F)) X) = Pcell.weightedAverage fun (c : Pcell.Cell) => blockVecDot X (blockMatVecMul (blockReflect (F c)) X)

theorem HCPolySupport.Book.Ch05.Section56.sum_weightedAverage_two_terms_sub_const {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (w : κ → ℝ) (hw : ∑ c : κ, w c = 1) (f g : ι → κ → ℝ) (h : ι → ℝ) : ∑ α : ι, (1 / 2 * ∑ c : κ, w c * f α c + 1 / 2 * ∑ c : κ, w c * g α c - h α) = ∑ c : κ, w c * ∑ α : ι, (1 / 2 * f α c + 1 / 2 * g α c - h α)

theorem HCPolySupport.Book.Ch05.Section56.fullBlockJTraceBudgetWithNormalizers_weightedBlockAverage {d : ℕ} {U : Ch02.Domain d} (Pcell : Ch02.DomainPartition U) (S T : FullBlockMat d) (F : Pcell.Cell → BlockMat d) : fullBlockJTraceBudgetWithNormalizers S T (Pcell.weightedBlockAverage F) = Pcell.weightedAverage fun (c : Pcell.Cell) => fullBlockJTraceBudgetWithNormalizers S T (F c)

theorem HCPolySupport.Book.Ch05.Section56.fullBlockTrace_transpose_mul_mul_eq_sum_blockVecDot {d : ℕ} (S M : FullBlockMat d) : Ch02.fullBlockTrace (Matrix.transpose S * M * S) = ∑ α : BlockCoord d, blockVecDot (fullBlockMatrixProbe S α) (blockMatVecMul (ofFullBlockMat M) (fullBlockMatrixProbe S α))

theorem HCPolySupport.Book.Ch05.Section56.fullBlockTrace_transpose_blockSub_le_two_fullBlockJTraceBudgetWithNormalizers {d : ℕ} (S T : FullBlockMat d) {A B : BlockMat d} (hAB : BlockMatLoewnerLE A B) (hStarAB : BlockMatLoewnerLE (blockReflect A) (blockReflect B)) (hParentBudget_nonneg : 0 ≤ fullBlockJTraceBudgetWithNormalizers S T A) : Ch02.fullBlockTrace (Matrix.transpose S * (toFullBlockMat B - toFullBlockMat A) * S) ≤ 2 * fullBlockJTraceBudgetWithNormalizers S T B

theorem HCPolySupport.Book.Ch05.Section56.BlockMatLoewnerLE.blockReflect' {d : ℕ} {A B : BlockMat d} (hAB : BlockMatLoewnerLE A B) : BlockMatLoewnerLE (blockReflect A) (blockReflect B)