Coarse-graining support: #
Support.Book.Ch05.Theorems.Section56.SmallContrastAssembly.MatrixAveragePackaging
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.fullBlockFluctuationMatrixWithNormalizer_isSymm_of_isSymmetricBlockMat
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(center : ℤ)
(S : FullBlockMat d)
{U : Set (Vec d)}
{a : RegCoeffField d}
(hA : IsSymmetricBlockMat (coarseBlockMatrix U a.toFun))
:
Matrix.IsSymm (fullBlockFluctuationMatrixWithNormalizer hP hStruct center S U a)
theorem
HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.fullBlockFluctuationMatrixWithNormalizer_isSymm_ae
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(center : ℤ)
(S : FullBlockMat d)
(Q : TriadicCube d)
:
∀ᵐ (a : RegCoeffField d) ∂P, Matrix.IsSymm (fullBlockFluctuationMatrixWithNormalizer hP hStruct center S (cubeSet Q) a)
theorem
HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.descendantsAverageFullBlockMat_isSymm
{d : ℕ}
{Q : TriadicCube d}
{j : ℕ}
{F : TriadicCube d → FullBlockMat d}
(hF : ∀ R ∈ descendantsAtDepth Q j, Matrix.IsSymm (F R))
:
theorem
HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.descendantsAverageFluctuationMatrixWithNormalizer_isSymm_ae
{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) ∂P, Matrix.IsSymm (descendantsAverageFluctuationMatrixWithNormalizer hP hStruct center S Q j a)
theorem
HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.descendantsAverageFluctuationOperatorNormSqWithNormalizer_le_probeSqBudget_ae
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(center : ℤ)
(S : FullBlockMat d)
(Q : TriadicCube d)
(j : ℕ)
:
(fun (a : RegCoeffField d) => descendantsAverageFluctuationOperatorNormSqWithNormalizer hP hStruct center S Q j a) ≤ᵐ[P]
fun (a : RegCoeffField d) =>
↑(Fintype.card (BlockCoord d)) ^ 2 * Section54.VarianceBoundGoodScale.fullBlockProbeSqBudget
(descendantsAverageFluctuationMatrixWithNormalizer hP hStruct center S Q j a)
theorem
HCPolySupport.Book.Ch05.Section56.SmallContrastAssembly.descendantsAverageFluctuationOperatorNormSqWithNormalizer_integral_le_probeBounds
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P)
(m n k : ℕ)
(hk : k ≤ n)
(S : FullBlockMat d)
(Ccoord : BlockCoord d → ℝ)
(Cplus Cminus : BlockCoord d → BlockCoord d → ℝ)
(hcoord_int :
∀ (α : BlockCoord d),
MeasureTheory.Integrable
(fun (a : RegCoeffField d) =>
Section54.VarianceBoundGoodScale.fullBlockQuadratic
(descendantsAverageFluctuationMatrixWithNormalizer hP hStruct (↑m) S (originCube d ↑n) (n - k) a)
(Section54.VarianceBoundGoodScale.fullBlockCoordinateProbe α) ^ 2)
P)
(hplus_int :
∀ (α β : BlockCoord d),
MeasureTheory.Integrable
(fun (a : RegCoeffField d) =>
Section54.VarianceBoundGoodScale.fullBlockQuadratic
(descendantsAverageFluctuationMatrixWithNormalizer hP hStruct (↑m) S (originCube d ↑n) (n - k) a)
(Section54.VarianceBoundGoodScale.fullBlockPlusProbe α β) ^ 2)
P)
(hminus_int :
∀ (α β : BlockCoord d),
MeasureTheory.Integrable
(fun (a : RegCoeffField d) =>
Section54.VarianceBoundGoodScale.fullBlockQuadratic
(descendantsAverageFluctuationMatrixWithNormalizer hP hStruct (↑m) S (originCube d ↑n) (n - k) a)
(Section54.VarianceBoundGoodScale.fullBlockMinusProbe α β) ^ 2)
P)
(hcoord :
∀ (α : BlockCoord d),
∫ (a : RegCoeffField d), Section54.VarianceBoundGoodScale.fullBlockQuadratic
(descendantsAverageFluctuationMatrixWithNormalizer hP hStruct (↑m) S (originCube d ↑n) (n - k) a)
(Section54.VarianceBoundGoodScale.fullBlockCoordinateProbe α) ^ 2 ∂P ≤ Ccoord α)
(hplus :
∀ (α β : BlockCoord d),
∫ (a : RegCoeffField d), Section54.VarianceBoundGoodScale.fullBlockQuadratic
(descendantsAverageFluctuationMatrixWithNormalizer hP hStruct (↑m) S (originCube d ↑n) (n - k) a)
(Section54.VarianceBoundGoodScale.fullBlockPlusProbe α β) ^ 2 ∂P ≤ Cplus α β)
(hminus :
∀ (α β : BlockCoord d),
∫ (a : RegCoeffField d), Section54.VarianceBoundGoodScale.fullBlockQuadratic
(descendantsAverageFluctuationMatrixWithNormalizer hP hStruct (↑m) S (originCube d ↑n) (n - k) a)
(Section54.VarianceBoundGoodScale.fullBlockMinusProbe α β) ^ 2 ∂P ≤ Cminus α β)
:
∫ (a : RegCoeffField d), descendantsAverageFluctuationOperatorNormSqWithNormalizer hP hStruct (↑m) S (originCube d ↑n) (n - k) a ∂P ≤ ↑(Fintype.card (BlockCoord d)) ^ 2 * (↑(Fintype.card (BlockCoord d)) * ∑ α : BlockCoord d, ↑(Fintype.card (BlockCoord d)) * ∑ β : BlockCoord d, 3 * (Ccoord α + Cplus α β + Cminus α β))