ProbeMoment

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

Per-probe second moments of the normalized fluctuation matrix

The observable is controlled a.s. by finitely many quadratic probes of the normalized fluctuation matrix H = D·(A_m − Ā_m)·D (fullBlock_operatorNorm_sq_le_probeSqBudget). Here we bound the second moment of each such probe by the centered-second-moment estimate (centered_quadratic_second_moment).

• fluctuation_probe_eq_centered_blockQuadratic — the deterministic identity turning a probe of H into the centered block quadratic form of the diagonally rescaled probe vector.
• probe_sq_integral_le — for any probe q with ⟪q,q⟫ ≤ 2, the second moment of fullBlockQuadratic H q is at most 16·Cd·Θ⁶·(3^m)^{-β}.

theorem HCPolySupport.fluctuation_probe_eq_centered_blockQuadratic {d : ℕ} [NeZero d] {L : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier L) (hStruct : Book.Ch04.RestrictionStructuralLaw L) (m : ℤ) (q : FullBlockVec d) (a : RegCoeffField d) : Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockQuadratic (Book.Ch05.Section54.VarianceBoundGoodScale.normalizedFluctuationMatrix hP hStruct m (cubeSet (originCube d m)) a.toFun) q = blockVecDot (ofFullBlockVec ((Matrix.diagonal (Book.Ch04.scalarFullBlockInvSqrtDiag (hP.barSigmaAtScale hStruct m) (hP.barSigmaStarAtScale hStruct m))).mulVec q)) (blockMatVecMul (ofFullBlockMat (toFullBlockMat (coarseBlockMatrix (cubeSet (originCube d m)) a.toFun) - toFullBlockMat (Book.Ch04.annealedBlockMatrixAtScale L m))) (ofFullBlockVec ((Matrix.diagonal (Book.Ch04.scalarFullBlockInvSqrtDiag (hP.barSigmaAtScale hStruct m) (hP.barSigmaStarAtScale hStruct m))).mulVec q)))

Probe → centered block quadratic. A quadratic probe of the normalized fluctuation matrix H = D·(A_m − Ā_m)·D equals the centered block quadratic form of the diagonally rescaled probe vector w = ofFullBlockVec (D q).

theorem HCPolySupport.probe_sq_integral_le {d : ℕ} [NeZero d] (hd : 3 ≤ d) : ∃ (Cd : ℝ), 0 ≤ Cd ∧ ∀ {m : ℤ}, 0 ≤ m → ∀ {Θ : ℝ}, 1 ≤ Θ → ∀ {L : Book.Ch04.RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure L] (hP : Book.Ch04.RestrictionLawCarrier L) (hStruct : Book.Ch04.RestrictionStructuralLaw L), ThetaEllipticLaw Θ L → ∀ (q : FullBlockVec d), q ⬝ᵥ q ≤ 4 → ∫ (a : RegCoeffField d), Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockQuadratic (Book.Ch05.Section54.VarianceBoundGoodScale.normalizedFluctuationMatrix hP hStruct m (cubeSet (originCube d m)) a.toFun) q ^ 2 ∂L ≤ 64 * Cd * Θ ^ 6 * (3 ^ m) ^ (-(↑d - 2) / (↑d - 1))

Per-probe second moment. For any full-block probe q with ⟪q,q⟫ ≤ 4, the second moment of fullBlockQuadratic H q is at most 64·Cd·Θ⁶·(3^m)^{-β}, with Cd the dimension-only centered-moment constant.

theorem HCPolySupport.integrable_fluctuation_probe_sq {d : ℕ} [NeZero d] {L : Book.Ch04.RestrictionCoeffLaw d} {Θ : ℝ} (hΘ : 1 ≤ Θ) (hP : Book.Ch04.RestrictionLawCarrier L) (hStruct : Book.Ch04.RestrictionStructuralLaw L) (hLaw : ThetaEllipticLaw Θ L) (m : ℤ) (q : FullBlockVec d) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => Book.Ch05.Section54.VarianceBoundGoodScale.fullBlockQuadratic (Book.Ch05.Section54.VarianceBoundGoodScale.normalizedFluctuationMatrix hP hStruct m (cubeSet (originCube d m)) a.toFun) q ^ 2) L

Probe second-moment integrability. Each squared probe of the normalized fluctuation matrix is integrable: it is (X − c₀)² for the a.s.-bounded coarse block quadratic X and a constant c₀.