Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch05.Theorems.Section54.Pigeonhole.ScalarChain

Coarse-graining support: Support.Book.Ch05.Theorems.Section54.Pigeonhole.ScalarChain #

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

Scalar-chain input for the Section 5.4 pigeonhole lemma #

The manuscript pigeonhole argument uses monotonicity of the scalar annealed coefficients. The current Ch4 endpoint proves this from full coarse-block integrability; this file records the exact Section 5.4-facing consequence without making it part of the public pigeonhole theorem statement.

source
theorem HCPolySupport.Book.Ch05.Section54.Pigeonhole.scalarChain_of_integrable_coarseFullBlockMatrixAtCube {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) {n m : ℤ} (hn_nonneg : 0 ≤ n) (hnm : n ≤ m) (hParentBlockInt : MeasureTheory.Integrable (Ch04.coarseFullBlockMatrixAtCube (originCube d m)) P) (hChildBlockInt : MeasureTheory.Integrable (Ch04.coarseFullBlockMatrixAtCube (originCube d n)) P) (hDescBlockInt : ∀ R ∈ descendantsAtScale (originCube d m) n, MeasureTheory.Integrable (Ch04.coarseFullBlockMatrixAtCube R) P) :
hP.barSigmaStarAtScale hStruct n ≤ hP.barSigmaStarAtScale hStruct m ∧ (hP.barSigmaStarAtScale hStruct m)⁻¹ ≤ (hP.barSigmaStarAtScale hStruct n)⁻¹ ∧ hP.barSigmaAtScale hStruct m ≤ hP.barSigmaAtScale hStruct n

Component-wise scalar-chain monotonicity obtained from the existing Ch4 full-block integrability endpoint.

source
theorem HCPolySupport.Book.Ch05.Section54.Pigeonhole.scalarChain_of_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {n m : ℕ} (hnm : n ≤ m) :
hP.barSigmaStarAtScale hStruct ↑n ≤ hP.barSigmaStarAtScale hStruct ↑m ∧ (hP.barSigmaStarAtScale hStruct ↑m)⁻¹ ≤ (hP.barSigmaStarAtScale hStruct ↑n)⁻¹ ∧ hP.barSigmaAtScale hStruct ↑m ≤ hP.barSigmaAtScale hStruct ↑n

Component-wise scalar-chain monotonicity with the full-block integrability supplied by (P4).

source
theorem HCPolySupport.Book.Ch05.Section54.Pigeonhole.barSigmaStarAtScale_pos_of_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) :
0 < hP.barSigmaStarAtScale hStruct ↑m

Under (P4), the starred scalar coefficient is positive at every nonnegative scale.

source
theorem HCPolySupport.Book.Ch05.Section54.Pigeonhole.barSigmaStarAtScale_inv_pos_of_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) :
0 < (hP.barSigmaStarAtScale hStruct ↑m)⁻¹

Under (P4), the inverse starred scalar coefficient is positive at every nonnegative scale.

source
theorem HCPolySupport.Book.Ch05.Section54.Pigeonhole.barSigmaAtScale_pos_of_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) :
0 < hP.barSigmaAtScale hStruct ↑m

Under (P4), the upper scalar coefficient is positive at every nonnegative scale.