Coarse-graining support: Support.Book.Ch05.Theorems.Section56.VarianceEstimateQuadratic.Triangle #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.Book.Ch05.Section56.descendantsAverageFullBlockMat_operatorNormSq_le_descendantsAverage_operatorNormSq
{d : ℕ}
(Q : TriadicCube d)
(j : ℕ)
(F : TriadicCube d → FullBlockMat d)
:
‖Matrix.toEuclideanCLM (descendantsAverageFullBlockMat Q j F)‖ ^ 2 ≤ descendantsAverage Q j fun (R : TriadicCube d) => ‖Matrix.toEuclideanCLM (F R)‖ ^ 2
theorem
HCPolySupport.Book.Ch05.Section56.descendantsAverageNormalizedFluctuationOperatorNormSq_le_descendantsAverage
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(center : ℤ)
(Q : TriadicCube d)
(j : ℕ)
(a : RegCoeffField d)
:
descendantsAverageNormalizedFluctuationOperatorNormSq hP hStruct center Q j a ≤ descendantsAverage Q j fun (R : TriadicCube d) =>
Ch04.fullBlockNormalizedFluctuationOperatorNormSq hP hStruct center (cubeSet R) a.toFun
Jensen/convexity bound for the squared operator norm of the normalized descendant-average fluctuation.
theorem
HCPolySupport.Book.Ch05.Section56.aemeasurable_fullBlockNormalizedFluctuationMatrix_cubeSet
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(center : ℤ)
(Q : TriadicCube d)
:
AEMeasurable
(fun (a : RegCoeffField d) =>
Section54.VarianceBoundGoodScale.normalizedFluctuationMatrix hP hStruct center (cubeSet Q) a.toFun)
P
theorem
HCPolySupport.Book.Ch05.Section56.aemeasurable_descendantsAverageNormalizedFluctuationMatrix
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(center : ℤ)
(Q : TriadicCube d)
(j : ℕ)
:
AEMeasurable (fun (a : RegCoeffField d) => descendantsAverageNormalizedFluctuationMatrix hP hStruct center Q j a) P
theorem
HCPolySupport.Book.Ch05.Section56.aemeasurable_descendantsAverageNormalizedFluctuationOperatorNormSq
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(center : ℤ)
(Q : TriadicCube d)
(j : ℕ)
:
AEMeasurable
(fun (a : RegCoeffField d) => descendantsAverageNormalizedFluctuationOperatorNormSq hP hStruct center Q j a) P
theorem
HCPolySupport.Book.Ch05.Section56.integrable_descendantsAverageNormalizedFluctuationOperatorNormSq_from_P4_of_stationary
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P)
(m n k : ℕ)
(_hk : k ≤ n)
:
MeasureTheory.Integrable
(descendantsAverageNormalizedFluctuationOperatorNormSq hP hStruct (↑m) (originCube d ↑n) (n - k)) P
theorem
HCPolySupport.Book.Ch05.Section56.descendantsAverageFluctuationOperatorNormSqWithNormalizer_le_descendantsAverage
{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)
:
descendantsAverageFluctuationOperatorNormSqWithNormalizer hP hStruct center S Q j a ≤ descendantsAverage Q j fun (R : TriadicCube d) =>
fullBlockFluctuationOperatorNormSqWithNormalizer hP hStruct center S (cubeSet R) a
Jensen/convexity bound for the squared operator norm of the arbitrary-normalizer descendant-average fluctuation.
theorem
HCPolySupport.Book.Ch05.Section56.fullBlockFluctuationNormSq_le_two_descendantMean_add_two_error
{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)
:
fullBlockFluctuationOperatorNormSqAtScaleWithNormalizer hP hStruct center S Q a ≤ 2 * descendantsAverageFluctuationOperatorNormSqWithNormalizer hP hStruct center S Q j a + 2 * coarseAverageErrorOperatorNormSqWithNormalizer hP hStruct center S Q j a
Pointwise variance triangle for an arbitrary deterministic normalizer.
theorem
HCPolySupport.Book.Ch05.Section56.fullBlockFluctuationOperatorNormSqAtScaleWithNormalizer_le_two_descendantsAverage_add_two_error
{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)
:
fullBlockFluctuationOperatorNormSqAtScaleWithNormalizer hP hStruct center S Q a ≤ (2 * descendantsAverage Q j fun (R : TriadicCube d) =>
fullBlockFluctuationOperatorNormSqWithNormalizer hP hStruct center S (cubeSet R) a) + 2 * coarseAverageErrorOperatorNormSqWithNormalizer hP hStruct center S Q j a
A version whose first term is the descendant average of the arbitrary-normalizer fluctuation observable.
theorem
HCPolySupport.Book.Ch05.Section56.fullBlockFluctuationNormSq_le_two_childMean_add_eight_JTraceAverageSq_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) => fullBlockFluctuationOperatorNormSqAtScaleWithNormalizer hP hStruct center S Q a) ≤ᵐ[P]
fun (a : RegCoeffField d) =>
2 * descendantsAverageFluctuationOperatorNormSqWithNormalizer hP hStruct center S Q j a + 8 * blockJTraceAverageSqWithNormalizers S T Q j a
Section 5.6 variance estimate with quadratic J error and arbitrary
deterministic normalizers. The manuscript specialization is
S = B^{-1/2} and T = B^{1/2}.
theorem
HCPolySupport.Book.Ch05.Section56.fullBlockFluctuationNormSq_le_two_childMean_add_eight_JTraceAverageSq_of_eight
{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) => fullBlockFluctuationOperatorNormSqAtScaleWithNormalizer hP hStruct center S Q a) ≤ᵐ[P]
fun (a : RegCoeffField d) =>
(2 * descendantsAverage Q j fun (R : TriadicCube d) =>
fullBlockFluctuationOperatorNormSqWithNormalizer hP hStruct center S (cubeSet R) a) + 8 * blockJTraceAverageSqWithNormalizers S T Q j a
Jensen-relaxed version of the arbitrary-normalizer variance estimate.