Monotonicity

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Loewner monotonicity of the annealed cutoff cube matrices

ABK26: by subadditivity, the matrices bfAhom_m(cu_n) are monotone nonincreasing in n in the Loewner (positive semidefinite) order. The paper places no sign restriction on n, and the consumers instantiate the statement at every n ∈ ℤ, so the monotonicity below is stated for all n ≤ k in ℤ.

Three inputs go into the proof.

• The deterministic a.e. block subadditivity comparison Ch04.RestrictionLawCarrier.coarseBlockMatrix_le_descendantsAverageBlockMat_ae and the block quadratic-form machinery of Ch04.blockMatLoewnerLE_of_integral_quadratic_mono are supplied by CoarseGraining and are scale-free.
• Entrywise integrability of the coarse block matrix on the parent cube and on each of its descendants is discharged from the proved cutoff moment layer: integrable_LambdaSqCoeffField_pow_cutoffLaw and integrable_lambdaSqCoeffField_inv_pow_cutoffLaw hold for the unnormalized cutoff law on an arbitrary triadic cube, so CoarseGraining's factor-moment route Ch04.RestrictionLawCarrier.integrable_coarseFullBlockMatrixAtCube_of_integrable_factor_observables applies verbatim. No (P4) record and no structural-law hypothesis is needed.
• The stationary transfer identifying the expectation on a descendant cube with the expectation on the origin cube at the descendant scale. This is the only step that is not scale-free in CoarseGraining: Ch04.RestrictionLawCarrier.blockMatLoewnerLE_annealedBlockMatrixAtScale routes it through RestrictionStationaryLaw = IsStationaryR, which only sees integer translations, whereas a descendant offset 3 ^ n * z is an integer vector only for n ≥ 0. The genuine cutoff law is invariant under every real translation, so this repository reroutes the transfer through Algsuperdiff.Section3.Cutoff.coefficientCutoffLaw_stationary_real and the scale-free geometry of Provider.Annealed.RealStationaryTransfer. That removes the sign restriction entirely.

Main results

• coefficientCutoffLaw_integrable_coarseFullBlockMatrixAtCube
• coefficientCutoffLaw_integrable_blockMatEntry_coarseBlockMatrix
• coefficientCutoffLaw_blockMatLoewnerLE_annealedBlockMatrixAtScale
• coefficientCutoffLaw_matLoewnerLE_annealedBAtScale
• coefficientCutoffLaw_matLoewnerLE_annealedSigmaStarInvAtScale

theorem Algsuperdiff.Section3.Provider.Annealed.coefficientCutoffLaw_integrable_coarseFullBlockMatrixAtCube {d : ℕ} [NeZero d] (M : ABKModel d) (m : ℤ) (Q : HCPolySupport.TriadicCube d) : MeasureTheory.Integrable (HCPolySupport.Book.Ch04.coarseFullBlockMatrixAtCube Q) (Cutoff.coefficientCutoffLaw M m)

The full unfolded coarse block observable of the genuine cutoff is integrable on every triadic cube. Both factor moments are the proved cutoff moments at exponent one.

theorem Algsuperdiff.Section3.Provider.Annealed.coefficientCutoffLaw_integrable_blockMatEntry_coarseBlockMatrix {d : ℕ} [NeZero d] (M : ABKModel d) (m : ℤ) (Q : HCPolySupport.TriadicCube d) (alpha beta : HCPolySupport.BlockCoord d) : MeasureTheory.Integrable (fun (a : HCPolySupport.RegCoeffField d) => HCPolySupport.blockMatEntry (HCPolySupport.coarseBlockMatrix (HCPolySupport.cubeSet Q) a.toFun) alpha beta) (Cutoff.coefficientCutoffLaw M m)

Every entry of the doubled coarse block matrix of the genuine cutoff is integrable on every triadic cube.

theorem Algsuperdiff.Section3.Provider.Annealed.coefficientCutoffLaw_isStationaryRealR {d : ℕ} (M : ABKModel d) (m : ℤ) : IsStationaryRealR (Cutoff.coefficientCutoffLaw M m)

Real-translation invariance of the genuine cutoff law, in the form consumed by the scale-free transfer layer.

Descendant averages of the coarse block entries

The Loewner monotonicity

theorem Algsuperdiff.Section3.Provider.Annealed.coefficientCutoffLaw_blockMatLoewnerLE_annealedBlockMatrixAtScale {d : ℕ} [NeZero d] (M : ABKModel d) (m : ℤ) {n k : ℤ} (hnk : n ≤ k) : HCPolySupport.BlockMatLoewnerLE (HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale (Cutoff.coefficientCutoffLaw M m) k) (HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale (Cutoff.coefficientCutoffLaw M m) n)

ABK26. The annealed cutoff block matrices on origin cubes are nonincreasing in the cube scale in the Loewner order, at every pair of integer scales n ≤ k.

theorem Algsuperdiff.Section3.Provider.Annealed.coefficientCutoffLaw_matLoewnerLE_annealedBAtScale {d : ℕ} [NeZero d] (M : ABKModel d) (m : ℤ) {n k : ℤ} (hnk : n ≤ k) : HCPolySupport.MatLoewnerLE (HCPolySupport.Book.Ch04.annealedBAtScale (Cutoff.coefficientCutoffLaw M m) k) (HCPolySupport.Book.Ch04.annealedBAtScale (Cutoff.coefficientCutoffLaw M m) n)

The annealed upper-left blocks of the genuine cutoff are nonincreasing in the cube scale.

theorem Algsuperdiff.Section3.Provider.Annealed.coefficientCutoffLaw_matLoewnerLE_annealedSigmaStarInvAtScale {d : ℕ} [NeZero d] (M : ABKModel d) (m : ℤ) {n k : ℤ} (hnk : n ≤ k) : HCPolySupport.MatLoewnerLE (HCPolySupport.Book.Ch04.annealedSigmaStarInvAtScale (Cutoff.coefficientCutoffLaw M m) k) (HCPolySupport.Book.Ch04.annealedSigmaStarInvAtScale (Cutoff.coefficientCutoffLaw M m) n)

The annealed inverse-star blocks of the genuine cutoff are nonincreasing in the cube scale.