Coarse-graining support: Support.Book.Ch05.Theorems.Section57.UnitJTail

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

Unit-scale tail for the limiting-normalized block response

This file begins the deterministic unit-scale input for Corollary c.first.quenched.estimate: a Γσ tail for J(□_0,\overline A^{-1/2}e,\overline A^{1/2}e).

theorem HCPolySupport.Book.Ch05.Section57.abs_fullBlockQuadraticCh04_le_card_sq_mul_of_entry_abs_le {d : ℕ} (M : FullBlockMat d) (x : FullBlockVec d) {F : ℝ} (hF : 0 ≤ F) (hentry : ∀ (α β : BlockCoord d), |M α β| ≤ F) (hx : ∀ (α : BlockCoord d), |x α| ≤ 1) : |Ch04.fullBlockQuadraticCh04 M x| ≤ ↑(Fintype.card (BlockCoord d)) ^ 2 * F

A full-block quadratic form whose entries are uniformly bounded is controlled by a dimension-only constant on coordinatewise unit vectors.

theorem HCPolySupport.Book.Ch05.Section57.abs_invSqrtConj_toFullBlockMat_entry_le_weighted {d : ℕ} {A : BlockMat d} {L Λ I : ℝ} (hSymm : IsSymmetricBlockMat A) (hPos : Ch02.BlockPosDef A) (hL : 0 < L) (hΛ : 0 ≤ Λ) (hI : 0 ≤ I) (hUL : ∀ (i j : Fin d), |A.upperLeft i j| ≤ Λ) (hLR : ∀ (i j : Fin d), |A.lowerRight i j| ≤ I) (α β : BlockCoord d) : |(Matrix.diagonal (Ch04.scalarFullBlockInvSqrtDiag L L) * toFullBlockMat A * Matrix.diagonal (Ch04.scalarFullBlockInvSqrtDiag L L)) α β| ≤ L⁻¹ * Λ + L * I

Entrywise control of a scalar-normalized doubled block matrix by the weighted upper/lower ellipticity factors.

theorem HCPolySupport.Book.Ch05.Section57.fullBlockQuadraticCh04_diagonal_toFullBlockMat {d : ℕ} (r : BlockCoord d → ℝ) (A : BlockMat d) (q : FullBlockVec d) : Ch04.fullBlockQuadraticCh04 (toFullBlockMat A) ((Matrix.diagonal r).mulVec q) = Ch04.fullBlockQuadraticCh04 (Matrix.diagonal r * toFullBlockMat A * Matrix.diagonal r) q

Diagonal conjugation of a block matrix is the same quadratic form as evaluating the original block matrix on the diagonally normalized vector.

theorem HCPolySupport.Book.Ch05.Section57.blockPosDef_blockReflect {d : ℕ} {A : BlockMat d} (hA : Ch02.BlockPosDef A) : Ch02.BlockPosDef (blockReflect A)

Reflection preserves doubled-block positive definiteness.

theorem HCPolySupport.Book.Ch05.Section57.abs_sqrtConj_reflect_toFullBlockMat_entry_le_weighted {d : ℕ} {A : BlockMat d} {L Λ I : ℝ} (hSymm : IsSymmetricBlockMat A) (hPos : Ch02.BlockPosDef A) (hL : 0 < L) (hΛ : 0 ≤ Λ) (hI : 0 ≤ I) (hUL : ∀ (i j : Fin d), |A.upperLeft i j| ≤ Λ) (hLR : ∀ (i j : Fin d), |A.lowerRight i j| ≤ I) (α β : BlockCoord d) : |(Matrix.diagonal (Section56.scalarFullBlockSqrtDiag L L) * toFullBlockMat (blockReflect A) * Matrix.diagonal (Section56.scalarFullBlockSqrtDiag L L)) α β| ≤ L⁻¹ * Λ + L * I

Entrywise control for the reflected scalar square-root normalization.

theorem HCPolySupport.Book.Ch05.Section57.GammaSigmaCoarseGrainedEllipticity.limitNormalizedBlockJObservable_le_card_sq_mul_weighted_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} {hP : Ch04.RestrictionLawCarrier P} {hStruct : Ch04.RestrictionStructuralLaw P} (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) (e : FullBlockVec d) (he : ∀ (α : BlockCoord d), |e α| ≤ 1) : limitNormalizedBlockJObservable hP hStruct (originCube d 0) e ≤ᵐ[P] fun (a : RegCoeffField d) => ↑(Fintype.card (BlockCoord d)) ^ 2 * limitWeightedUnitEllipticityObservable hP hStruct hΓ.params.sUpper hΓ.params.sLower a

Unit-scale limiting-normalized J is pointwise dominated, a.e., by the limiting weighted unit ellipticity observable.

theorem HCPolySupport.Book.Ch05.Section57.GammaSigmaCoarseGrainedEllipticity.limitNormalizedBlockJObservable_unit_isBigO {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} {hP : Ch04.RestrictionLawCarrier P} {hStruct : Ch04.RestrictionStructuralLaw P} (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) (e : FullBlockVec d) (he : ∀ (α : BlockCoord d), |e α| ≤ 1) : IndependentSums.IsBigO P (IndependentSums.gammaSigma hΓ.sigma) (limitNormalizedBlockJObservable hP hStruct (originCube d 0) e) (↑(Fintype.card (BlockCoord d)) ^ 2 * (thetaAtScale hP hStruct 0 * hΓ.thetaHat))

The unit-cube limiting-normalized J observable inherits the Γσ tail from the strengthened unit ellipticity assumption.