Coarse-graining support: #
Support.Book.Ch05.Theorems.Section56.VarianceEstimateQuadratic.ErrorBounds
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.Book.Ch05.Section56.restrictsTo_descendantsDomainPartition_of_aelocallyUniformlyEllipticField
{d : ℕ}
{a : RegCoeffField d}
(ha : Ch04.AELocallyUniformlyEllipticField a)
(Q : TriadicCube d)
(j : ℕ)
:
have F := Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha;
let Pcell := Ch02.descendantsDomainPartition Q j;
∀ (i : Pcell.Cell), (F.coeffOn Q).RestrictsTo (F.coeffOn ↑i)
theorem
HCPolySupport.Book.Ch05.Section56.normalizedPositiveError_trace_le_two_upperBlockJTraceAverage
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P)
(m : ℕ)
(Q : TriadicCube d)
(j : ℕ)
{a : RegCoeffField d}
(ha : Ch04.AELocallyUniformlyEllipticField a)
:
Ch02.fullBlockTrace (normalizedCoarseAveragePositiveErrorMatrix hP hStruct (↑m) Q j a) ≤ 2 * normalizedUpperBlockJTraceAverage hP hStruct (↑m) Q j a
theorem
HCPolySupport.Book.Ch05.Section56.positiveErrorWithNormalizer_trace_le_two_blockJTraceAverageWithNormalizers
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(center : ℤ)
(S T : FullBlockMat d)
(Q : TriadicCube d)
(j : ℕ)
{a : RegCoeffField d}
(ha : Ch04.AELocallyUniformlyEllipticField a)
:
Ch02.fullBlockTrace (coarseAveragePositiveErrorMatrixWithNormalizer hP hStruct center S Q j a) ≤ 2 * blockJTraceAverageWithNormalizers S T Q j a
theorem
HCPolySupport.Book.Ch05.Section56.normalizedCoarseAveragePositiveErrorMatrix_posSemidef
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(center : ℤ)
(Q : TriadicCube d)
(j : ℕ)
{a : RegCoeffField d}
(ha : Ch04.AELocallyUniformlyEllipticField a)
:
Matrix.PosSemidef (normalizedCoarseAveragePositiveErrorMatrix hP hStruct center Q j a)
theorem
HCPolySupport.Book.Ch05.Section56.coarseAveragePositiveErrorMatrixWithNormalizer_posSemidef
{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}
(ha : Ch04.AELocallyUniformlyEllipticField a)
:
Matrix.PosSemidef (coarseAveragePositiveErrorMatrixWithNormalizer hP hStruct center S Q j a)
theorem
HCPolySupport.Book.Ch05.Section56.coarseAverageErrorOperatorNormSqWithNormalizer_le_four_blockJTraceAverageSqWithNormalizers
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(center : ℤ)
(S T : FullBlockMat d)
(Q : TriadicCube d)
(j : ℕ)
{a : RegCoeffField d}
(ha : Ch04.AELocallyUniformlyEllipticField a)
:
coarseAverageErrorOperatorNormSqWithNormalizer hP hStruct center S Q j a ≤ 4 * blockJTraceAverageSqWithNormalizers S T Q j a
theorem
HCPolySupport.Book.Ch05.Section56.coarseAverageErrorOperatorNormSqWithNormalizer_le_four_blockJTraceAverageSqWithNormalizers_ae
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(center : ℤ)
(S T : FullBlockMat d)
(Q : TriadicCube d)
(j : ℕ)
:
(fun (a : RegCoeffField d) => coarseAverageErrorOperatorNormSqWithNormalizer hP hStruct center S Q j a) ≤ᵐ[P]
fun (a : RegCoeffField d) => 4 * blockJTraceAverageSqWithNormalizers S T Q j a
theorem
HCPolySupport.Book.Ch05.Section56.normalizedCoarseAverageErrorOperatorNormSq_le_four_normalizedBlockJTraceAverageSq
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P)
(m : ℕ)
(Q : TriadicCube d)
(j : ℕ)
{a : RegCoeffField d}
(ha : Ch04.AELocallyUniformlyEllipticField a)
:
normalizedCoarseAverageErrorOperatorNormSq hP hStruct (↑m) Q j a ≤ 4 * normalizedBlockJTraceAverageSq hP hStruct (↑m) Q j a
theorem
HCPolySupport.Book.Ch05.Section56.normalizedCoarseAverageErrorOperatorNormSq_le_four_normalizedBlockJTraceAverageSq_ae
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P)
(m : ℕ)
(Q : TriadicCube d)
(j : ℕ)
:
(fun (a : RegCoeffField d) => normalizedCoarseAverageErrorOperatorNormSq hP hStruct (↑m) Q j a) ≤ᵐ[P]
fun (a : RegCoeffField d) => 4 * normalizedBlockJTraceAverageSq hP hStruct (↑m) Q j a