Coarse-graining support: Support.Book.Ch05.Theorems.Section57.AnnealedLimit #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Limiting annealed scalar coefficients #
This file starts the Lean surface for the limiting annealed matrix
\overline{\mathbf A} used in Section 5.7. The scalarized upper coefficient
is realized as the infimum of the decreasing \bar σ_n, and the starred
coefficient as the supremum of the increasing \bar σ_{*,n}.
noncomputable def
HCPolySupport.Book.Ch05.Section57.barSigmaLimit
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
:
Candidate limiting scalar \bar σ = inf_n \bar σ_n.
Equations
- HCPolySupport.Book.Ch05.Section57.barSigmaLimit hP hStruct = sInf (Set.range fun (n : ℕ) => hP.barSigmaAtScale hStruct ↑n)
Instances For
noncomputable def
HCPolySupport.Book.Ch05.Section57.barSigmaStarLimit
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
:
Candidate limiting starred scalar \bar σ_* = sup_n \bar σ_{*,n}.
Equations
- HCPolySupport.Book.Ch05.Section57.barSigmaStarLimit hP hStruct = sSup (Set.range fun (n : ℕ) => hP.barSigmaStarAtScale hStruct ↑n)
Instances For
noncomputable def
HCPolySupport.Book.Ch05.Section57.scalarAnnealedBlockMatrixLimit
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
:
BlockMat d
Limiting scalarized annealed doubled matrix.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
HCPolySupport.Book.Ch05.Section57.GammaSigmaCoarseGrainedEllipticity.barSigmaLimit_le_barSigmaAtScale
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
{hP : Ch04.RestrictionLawCarrier P}
{hStruct : Ch04.RestrictionStructuralLaw P}
(hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct)
(m : ℕ)
:
theorem
HCPolySupport.Book.Ch05.Section57.GammaSigmaCoarseGrainedEllipticity.barSigmaStarAtScale_le_barSigmaStarLimit
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
{hP : Ch04.RestrictionLawCarrier P}
{hStruct : Ch04.RestrictionStructuralLaw P}
(hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct)
(m : ℕ)
:
theorem
HCPolySupport.Book.Ch05.Section57.GammaSigmaCoarseGrainedEllipticity.barSigmaStarAtScale_le_barSigmaLimit
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
{hP : Ch04.RestrictionLawCarrier P}
{hStruct : Ch04.RestrictionStructuralLaw P}
(hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct)
(n : ℕ)
:
theorem
HCPolySupport.Book.Ch05.Section57.GammaSigmaCoarseGrainedEllipticity.barSigmaStarLimit_le_barSigmaLimit
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
{hP : Ch04.RestrictionLawCarrier P}
{hStruct : Ch04.RestrictionStructuralLaw P}
(hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct)
:
theorem
HCPolySupport.Book.Ch05.Section57.GammaSigmaCoarseGrainedEllipticity.barSigmaStarLimit_pos
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
{hP : Ch04.RestrictionLawCarrier P}
{hStruct : Ch04.RestrictionStructuralLaw P}
(hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct)
:
theorem
HCPolySupport.Book.Ch05.Section57.GammaSigmaCoarseGrainedEllipticity.barSigmaLimit_pos
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
{hP : Ch04.RestrictionLawCarrier P}
{hStruct : Ch04.RestrictionStructuralLaw P}
(hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct)
:
theorem
HCPolySupport.Book.Ch05.Section57.GammaSigmaCoarseGrainedEllipticity.barSigmaLimit_eq_barSigmaStarLimit
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
{hP : Ch04.RestrictionLawCarrier P}
{hStruct : Ch04.RestrictionStructuralLaw P}
(hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct)
:
theorem
HCPolySupport.Book.Ch05.Section57.GammaSigmaCoarseGrainedEllipticity.scalarAnnealedBlockMatrixLimit_eq_blockDiag_barSigmaLimit
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
{hP : Ch04.RestrictionLawCarrier P}
{hStruct : Ch04.RestrictionStructuralLaw P}
(hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct)
:
scalarAnnealedBlockMatrixLimit hP hStruct = Ch02.blockDiag (barSigmaLimit hP hStruct • 1) ((barSigmaLimit hP hStruct)⁻¹ • 1)
The limiting annealed block matrix has the single scalar coefficient
\bar σ on the upper block and \bar σ^{-1} on the lower block.
theorem
HCPolySupport.Book.Ch05.Section57.GammaSigmaCoarseGrainedEllipticity.barSigmaAtScale_zero_le_thetaAtScale_zero_mul_barSigmaLimit
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
{hP : Ch04.RestrictionLawCarrier P}
{hStruct : Ch04.RestrictionStructuralLaw P}
(hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct)
:
The upper unit-scale scalar is controlled by the limiting scalar times the initial scalar contrast.
theorem
HCPolySupport.Book.Ch05.Section57.GammaSigmaCoarseGrainedEllipticity.barSigmaLimit_inv_le_thetaAtScale_zero_mul_barSigmaAtScale_zero_inv
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
{hP : Ch04.RestrictionLawCarrier P}
{hStruct : Ch04.RestrictionStructuralLaw P}
(hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct)
:
The limiting inverse upper scalar is controlled by the unit-scale inverse upper scalar times the initial scalar contrast.
theorem
HCPolySupport.Book.Ch05.Section57.GammaSigmaCoarseGrainedEllipticity.barSigmaStarAtScale_zero_inv_le_thetaAtScale_zero_mul_barSigmaLimit_inv
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
{hP : Ch04.RestrictionLawCarrier P}
{hStruct : Ch04.RestrictionStructuralLaw P}
(hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct)
:
The unit-scale inverse starred scalar is controlled by the limiting inverse scalar times the initial scalar contrast.
theorem
HCPolySupport.Book.Ch05.Section57.GammaSigmaCoarseGrainedEllipticity.thetaAtScale_zero_le_gammaMomentScale_sq
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
{hP : Ch04.RestrictionLawCarrier P}
{hStruct : Ch04.RestrictionStructuralLaw P}
(hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct)
:
The initial scalar contrast is bounded by the Γσ ellipticity scale supplied
by (P5).