PrincipalResponseSwitchPlateau

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

Binder descriptions below are an informal inventory only, NOT a source certification; certification vocabulary is reserved for frozen source-facing declarations.

Provider: the annealed limit matrix and the finite-cube plateau sandwich

This module supplies the two deterministic ingredients that the annealed switch e.use.also.for.the.upper.bound of ABK26 opens with, namely the ordering bfAhom_L <= bfAhom_L(cu_n) between the infinite-volume annealed matrix and its finite-cube counterpart, together with the identification of the constant comparator block matrix used by mathcal E with that same infinite-volume matrix.

The two objects

ABK26, e.homs.defs, defines the deterministic matrix

bfAhom_m := diag(shom_m, shom_m^{-1}) := lim_{n -> infty} E[bfA_m(cu_n)],

with shom_m the running diffusivity Annealed.sigmaBar M m, and records that the finite-cube matrices bfAhom_m(cu_n) are nonincreasing in n in the Loewner order. Combining the two gives the left half of the sandwich bfAhom_{m-h,*}(cu_n) <= bfAhom_{m-h} <= bfAhom_{m-h}(cu_n) printed.

mathcal E_{s,p,q}(cu_m; a, a_0) normalizes its one-cube probe by the constant block matrix Ch02.constantBlockMatrix a_0. At the Section 3 comparator a_0 = shom_m Id that constant block matrix is exactly bfAhom_m, which is what makes the annealed probe (bfAhom^{-1/2} e, bfAhom^{1/2} e) of ABK26 the same probe that mathcal E maximizes over; this is recorded below in constantBlockMatrix_isotropicComparatorMatrix.

Scope

Everything here is deterministic: no induction state, no bad events, no recurrence parameters.

Main results

• blockVecDot_blockDiag_smul_one_vecDot: the doubled quadratic form of a scalar block-diagonal matrix.
• blockMatLoewnerLE_annealedBlockMatrixAtScale_annealedLimit: the plateau ordering bfAhom_L <= bfAhom_L(cu_n), at every pair of integers L, n.
• sigmaBar_le_annealedCubeUpperLeft, inv_sigmaBar_le_annealedCubeLowerRight: the two scalar consequences of that ordering.

References

• ABK26, e.homs.defs.U.diag, e.homs.defs.
• ABK26 (e.use.also.for.the.upper.bound and its proof).

Scalar matrix algebra

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.blockVecDot_blockDiag_smul_one_vecDot {d : ℕ} (c c' : ℝ) (V : HCPolySupport.BlockVec d) : HCPolySupport.blockVecDot V (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.blockDiag (c • 1) (c' • 1)) V) = c * HCPolySupport.vecDot V.1 V.1 + c' * HCPolySupport.vecDot V.2 V.2

The doubled quadratic form of a scalar block-diagonal matrix.

Convergence of the doubled quadratic form

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.tendsto_blockVecDot_blockMatVecMul {d : ℕ} {A : ℕ → HCPolySupport.BlockMat d} {B : HCPolySupport.BlockMat d} (h : Filter.Tendsto (fun (k : ℕ) => HCPolySupport.toFullBlockMat (A k)) Filter.atTop (nhds (HCPolySupport.toFullBlockMat B))) (V : HCPolySupport.BlockVec d) : Filter.Tendsto (fun (k : ℕ) => HCPolySupport.blockVecDot V (HCPolySupport.blockMatVecMul (A k) V)) Filter.atTop (nhds (HCPolySupport.blockVecDot V (HCPolySupport.blockMatVecMul B V)))

Entrywise convergence of doubled block matrices passes to their doubled quadratic forms.

The plateau ordering

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.blockMatLoewnerLE_annealedBlockMatrixAtScale_annealedLimit {d : ℕ} [NeZero d] (M : ABKModel d) (m n : ℤ) : HCPolySupport.BlockMatLoewnerLE (HCPolySupport.Book.Ch02.blockDiag (↑(Annealed.sigmaBar M m) • 1) ((↑(Annealed.sigmaBar M m))⁻¹ • 1)) (HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale (Cutoff.coefficientCutoffLaw M m) n)

ABK26. The infinite-volume annealed matrix bfAhom_L = diag(shom_L, shom_L^{-1}) is below the finite-cube annealed matrix bfAhom_L(cu_n) in the Loewner order, at every cube scale n.

This is the right half of the sandwich printed; it is the Loewner monotonicity of together with the limit defining bfAhom_L in e.homs.defs.

The two scalar consequences

def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.potentialProbe {d : ℕ} (i : Fin d) : HCPolySupport.BlockVec d

The coordinate potential probe (e_i, 0).

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.potentialProbe i = (fun (j : Fin d) => if j = i then 1 else 0, fun (x : Fin d) => 0)

def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.fluxProbe {d : ℕ} (i : Fin d) : HCPolySupport.BlockVec d

The coordinate flux probe (0, e_i).

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.fluxProbe i = (fun (x : Fin d) => 0, fun (j : Fin d) => if j = i then 1 else 0)

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.sigmaBar_le_annealedCubeUpperLeft {d : ℕ} [NeZero d] (M : ABKModel d) (m n : ℤ) {s t : ℝ} (hst : HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale (Cutoff.coefficientCutoffLaw M m) n = HCPolySupport.Book.Ch02.blockDiag (s • 1) (t • 1)) : ↑(Annealed.sigmaBar M m) ≤ s

ABK26, upper-left block. The running diffusivity is below the upper-left scalar of the finite-cube annealed matrix.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.inv_sigmaBar_le_annealedCubeLowerRight {d : ℕ} [NeZero d] (M : ABKModel d) (m n : ℤ) {s t : ℝ} (hst : HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale (Cutoff.coefficientCutoffLaw M m) n = HCPolySupport.Book.Ch02.blockDiag (s • 1) (t • 1)) : (↑(Annealed.sigmaBar M m))⁻¹ ≤ t

ABK26, lower-right block. The inverse running diffusivity is below the lower-right scalar of the finite-cube annealed matrix.