Polarize

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

Centered second moments of the block matrix

From the scalar estimate scalar_block_variance we pass to the centered block matrix A_m − Ā_m, where Ā_m = annealedBlockMatrixAtScale L m is the entrywise annealed matrix.

• integrable_blockMatEntry_coarse — each entry of the coarse block matrix is integrable (its a.s. symmetry turns the C4 quadratic bounds at blockBasis vectors into an a.s. entry bound).
• mean_zero_coarse_blockQuadratic — 𝔼[w·A_m w] = w·Ā_m w (integral linearity of the finite block quadratic form).
• centered_quadratic_second_moment — for arbitrary w, 𝔼[(w·(A_m − Ā_m)w)²] = Var[w·A_m w] ≤ Cd·(Θ|w.1|²+|w.2|²)²·min{1, Θ²3^{-βm}}.

theorem HCPolySupport.integrable_blockMatEntry_coarse {d : ℕ} [NeZero d] {L : Book.Ch04.RestrictionCoeffLaw d} {Θ : ℝ} (hΘ : 1 ≤ Θ) (hP : Book.Ch04.RestrictionLawCarrier L) (hLaw : ThetaEllipticLaw Θ L) (m : ℤ) (α β : BlockCoord d) : MeasureTheory.Integrable (fun (a : RegCoeffField d) => blockMatEntry (coarseBlockMatrix (cubeSet (originCube d m)) a.toFun) α β) L

Entrywise integrability of the coarse block matrix. Uses a.s. symmetry plus the C4 quadratic bounds at the blockBasis vectors.

theorem HCPolySupport.mean_zero_coarse_blockQuadratic {d : ℕ} [NeZero d] {L : Book.Ch04.RestrictionCoeffLaw d} {Θ : ℝ} (hΘ : 1 ≤ Θ) (hP : Book.Ch04.RestrictionLawCarrier L) (hLaw : ThetaEllipticLaw Θ L) (m : ℤ) (w : BlockVec d) : ∫ (a : RegCoeffField d), blockVecDot w (blockMatVecMul (coarseBlockMatrix (cubeSet (originCube d m)) a.toFun) w) ∂L = blockVecDot w (blockMatVecMul (Book.Ch04.annealedBlockMatrixAtScale L m) w)

Mean-zero. 𝔼[w·A_m w] = w·Ā_m w.

theorem HCPolySupport.centered_quadratic_second_moment {d : ℕ} [NeZero d] (hd : 3 ≤ d) : ∃ (Cd : ℝ), 0 ≤ Cd ∧ ∀ {m : ℤ}, 0 ≤ m → ∀ {Θ : ℝ}, 1 ≤ Θ → ∀ {L : Book.Ch04.RestrictionCoeffLaw d} [MeasureTheory.IsProbabilityMeasure L], Book.Ch04.RestrictionLawCarrier L → IsRestrictionUnitRangeDependentR L → ThetaEllipticLaw Θ L → ∀ (w : BlockVec d), ∫ (a : RegCoeffField d), blockVecDot w (blockMatVecMul (ofFullBlockMat (toFullBlockMat (coarseBlockMatrix (cubeSet (originCube d m)) a.toFun) - toFullBlockMat (Book.Ch04.annealedBlockMatrixAtScale L m))) w) ^ 2 ∂L ≤ Cd * (Θ * vecNormSq w.1 + vecNormSq w.2) ^ 2 * min 1 (Θ ^ 2 * (3 ^ m) ^ (-(↑d - 2) / (↑d - 1)))

Centered second moment for an arbitrary doubled vector. Equal to Var[w·A_m w], hence bounded by the scalar estimate. The constant is the one from scalar_block_variance, uniform in all parameters.