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

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

Limiting full-block normalization

This file packages the full-block diagonal normalizers associated with the limiting scalar annealed matrix \overline A. These are the Lean objects appearing in the first quenched estimate as \overline A^{-1/2} e and \overline A^{1/2} e.

noncomputable def HCPolySupport.Book.Ch05.Section57.scalarLimitInvSqrtMatrix {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) : FullBlockMat d

Diagonal full-block matrix representing \overline A^{-1/2} in the scalarized limiting normalization.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section57.scalarLimitSqrtMatrix {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) : FullBlockMat d

Diagonal full-block matrix representing \overline A^{1/2} in the scalarized limiting normalization.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section57.scalarLimitInvSqrtBlockVec {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (e : FullBlockVec d) : BlockVec d

The first block vector in J(Q,\overline A^{-1/2}e,\overline A^{1/2}e).

Equations

• HCPolySupport.Book.Ch05.Section57.scalarLimitInvSqrtBlockVec hP hStruct e = HCPolySupport.ofFullBlockVec (Matrix.mulVec (HCPolySupport.Book.Ch05.Section57.scalarLimitInvSqrtMatrix hP hStruct) e)

noncomputable def HCPolySupport.Book.Ch05.Section57.scalarLimitSqrtBlockVec {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (e : FullBlockVec d) : BlockVec d

The second block vector in J(Q,\overline A^{-1/2}e,\overline A^{1/2}e).

Equations

• HCPolySupport.Book.Ch05.Section57.scalarLimitSqrtBlockVec hP hStruct e = HCPolySupport.ofFullBlockVec (Matrix.mulVec (HCPolySupport.Book.Ch05.Section57.scalarLimitSqrtMatrix hP hStruct) e)

noncomputable def HCPolySupport.Book.Ch05.Section57.limitNormalizedBlockJObservable {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (Q : TriadicCube d) (e : FullBlockVec d) : RegCoeffField d → ℝ

The Section 5.7 normalized block-response observable with the limiting annealed normalization.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section57.limitWeightedUnitEllipticityObservable {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (sUpper sLower : ℝ) : RegCoeffField d → ℝ

Unit-cube ellipticity observable with the limiting scalar normalization. This is the pointwise factor produced after replacing \overline A_0 by \overline A.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section57.limitWeightedUnitEllipticityObservableOnCube {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (Q : TriadicCube d) (sUpper sLower : ℝ) : RegCoeffField d → ℝ

Unit-cube ellipticity observable on an arbitrary cube, with the limiting scalar normalization. The origin version above is the special case used by the Γσ assumption; this localized version is the one needed for descendant unit cubes inside a larger cube.

Equations

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

@[simp]

theorem HCPolySupport.Book.Ch05.Section57.limitWeightedUnitEllipticityObservableOnCube_originCube_zero {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (sUpper sLower : ℝ) : limitWeightedUnitEllipticityObservableOnCube hP hStruct (originCube d 0) sUpper sLower = limitWeightedUnitEllipticityObservable hP hStruct sUpper sLower

theorem HCPolySupport.Book.Ch05.Section57.GammaSigmaCoarseGrainedEllipticity.scalarLimit_normalizers_pairing_eq_dotProduct {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} {hP : Ch04.RestrictionLawCarrier P} {hStruct : Ch04.RestrictionStructuralLaw P} (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) (e : FullBlockVec d) : blockVecDot (scalarLimitInvSqrtBlockVec hP hStruct e) (scalarLimitSqrtBlockVec hP hStruct e) = e ⬝ᵥ e

The two limiting scalar normalizers are dual: their pairing preserves the Euclidean square norm of the full-block vector.

theorem HCPolySupport.Book.Ch05.Section57.GammaSigmaCoarseGrainedEllipticity.limitWeightedUnitEllipticityObservable_le_thetaAtScale_zero_mul_unit {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} {hP : Ch04.RestrictionLawCarrier P} {hStruct : Ch04.RestrictionStructuralLaw P} (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) (a : RegCoeffField d) : limitWeightedUnitEllipticityObservable hP hStruct hΓ.params.sUpper hΓ.params.sLower a ≤ thetaAtScale hP hStruct 0 * gammaSigmaUnitEllipticityObservable hP hStruct hΓ.params.sUpper hΓ.params.sLower a

Replacing the unit-scale scalar normalizer by the limiting scalar normalizer costs at most the initial scalar contrast.

theorem HCPolySupport.Book.Ch05.Section57.GammaSigmaCoarseGrainedEllipticity.limitWeightedUnitEllipticityObservableOnCube_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} {hP : Ch04.RestrictionLawCarrier P} {hStruct : Ch04.RestrictionStructuralLaw P} (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) (Q : TriadicCube d) (a : RegCoeffField d) : 0 ≤ limitWeightedUnitEllipticityObservableOnCube hP hStruct Q hΓ.params.sUpper hΓ.params.sLower a

Pointwise nonnegativity of the localized limiting-normalized unit ellipticity observable.

theorem HCPolySupport.Book.Ch05.Section57.GammaSigmaCoarseGrainedEllipticity.limitWeightedUnitEllipticityObservable_isBigO {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} {hP : Ch04.RestrictionLawCarrier P} {hStruct : Ch04.RestrictionStructuralLaw P} (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) : IndependentSums.IsBigO P (IndependentSums.gammaSigma hΓ.sigma) (limitWeightedUnitEllipticityObservable hP hStruct hΓ.params.sUpper hΓ.params.sLower) (thetaAtScale hP hStruct 0 * hΓ.thetaHat)

The limiting-normalized unit ellipticity observable inherits the Γσ tail from the unit-scale Γσ assumption.