ScalarBounds

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Scalar normalization bounds for the fluctuation bridge

The fluctuation observable normalizes the centered coarse block matrix by the diagonal D = diag(scalarFullBlockInvSqrtDiag b c), where b = barSigmaAtScale and c = barSigmaStarAtScale are the structural-law scalars.

Here we pin down the two-sided bounds on b and c that make the diagonal normalization uniformly bounded:

• ae_coarseBlockQuadratic_lower_of_thetaEllipticLaw — the a.s. lower C1 Loewner bound (mirroring the upper bound ae_coarseBlockQuadratic_bounds_...).
• half_le_barSigmaAtScale — 1/2 ≤ b.
• barSigmaStarAtScale_pos / barSigmaStarAtScale_le_two_mul_Theta — 0 < c and c ≤ 2Θ.

The b and c values are read off the isotropic annealed block matrix (annealedBlockMatrixAtScale_eq_scalarAnnealedBlockMatrixAtScale), whose diagonal basis pairings equal b and c⁻¹, integrated against the a.s. C1′ sandwich (mean_zero_coarse_blockQuadratic).

theorem HCPolySupport.ae_coarseBlockQuadratic_lower_of_thetaEllipticLaw {d : ℕ} [NeZero d] {L : Book.Ch04.RestrictionCoeffLaw d} {Θ : ℝ} (hΘ : 1 ≤ Θ) (hell : ThetaEllipticLaw Θ L) (m : ℤ) (P : BlockVec d) : ∀ᵐ (a : RegCoeffField d) ∂L, 1 / 2 * vecNormSq P.1 + (2 * Θ)⁻¹ * vecNormSq P.2 ≤ blockVecDot P (blockMatVecMul (coarseBlockMatrix (cubeSet (originCube d m)) a.toFun) P)

C1 (lower, a.s.). Under the amended ThetaEllipticLaw Θ L, the coarse block observable a.s. dominates the lower diagonal quadratic form ½|p|² + (2Θ)⁻¹|q|². Proved by routing each realization through the C2 truncation bridge to an everywhere-(1,Θ)-elliptic representative and applying the deterministic lower Loewner sandwich, exactly as ae_coarseBlockQuadratic_bounds_of_thetaEllipticLaw does for the upper bound.

theorem HCPolySupport.integrable_coarseBlockQuadratic_of_thetaEllipticLaw {d : ℕ} [NeZero d] {L : Book.Ch04.RestrictionCoeffLaw d} {Θ : ℝ} (hΘ : 1 ≤ Θ) (hP : Book.Ch04.RestrictionLawCarrier L) (hLaw : ThetaEllipticLaw Θ L) (m : ℤ) (P : BlockVec d) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => blockVecDot P (blockMatVecMul (coarseBlockMatrix (cubeSet (originCube d m)) a.toFun) P)) L

Integrability of the coarse block quadratic form for a fixed probe vector, under any ThetaEllipticLaw on a probability law.

theorem HCPolySupport.half_le_barSigmaAtScale {d : ℕ} [NeZero d] {L : Book.Ch04.RestrictionCoeffLaw d} {Θ : ℝ} (hΘ : 1 ≤ Θ) (hP : Book.Ch04.RestrictionLawCarrier L) (hStruct : Book.Ch04.RestrictionStructuralLaw L) (hLaw : ThetaEllipticLaw Θ L) (m : ℤ) : 1 / 2 ≤ hP.barSigmaAtScale hStruct m

1/2 ≤ b. The structural-law scalar \bar\sigma_m is at least 1/2: it is the annealed diagonal upper-left entry, which the integrated lower C1 sandwich bounds below by 1/2.

theorem HCPolySupport.barSigmaStarAtScale_pos {d : ℕ} [NeZero d] {L : Book.Ch04.RestrictionCoeffLaw d} {Θ : ℝ} (hΘ : 1 ≤ Θ) (hP : Book.Ch04.RestrictionLawCarrier L) (hStruct : Book.Ch04.RestrictionStructuralLaw L) (hLaw : ThetaEllipticLaw Θ L) (m : ℤ) : 0 < hP.barSigmaStarAtScale hStruct m

0 < c.

theorem HCPolySupport.barSigmaStarAtScale_le_two_mul_Theta {d : ℕ} [NeZero d] {L : Book.Ch04.RestrictionCoeffLaw d} {Θ : ℝ} (hΘ : 1 ≤ Θ) (hP : Book.Ch04.RestrictionLawCarrier L) (hStruct : Book.Ch04.RestrictionStructuralLaw L) (hLaw : ThetaEllipticLaw Θ L) (m : ℤ) : hP.barSigmaStarAtScale hStruct m ≤ 2 * Θ

c ≤ 2Θ.