PrincipalResponsePSqrt

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

Provider: the annealed limit block matrix and its two square roots

Source displays in ABK26:

• e.homs.defs (label; display) defines the deterministic infinite-volume annealed doubled matrix bfAhom_m = ((shom_m, 0), (0, shom_m^{-1})), where rules that shom_m is a scalar matrix, "a positive scalar matrix, or a positive real number, whichever is convenient".
• e.homs.defs.U.diag (label) is the finite-volume block diagonality that the limit inherits; it is already realized in this repository by Provider.Annealed.coefficientCutoffLaw_annealedBlockMatrixAtScale_eq_blockDiag.
• e.recurrence.P.def (label) and e.Pz.def (label) apply the inverse square root bfAhom_{m-h}^{-1/2} to a doubled load applies the square root bfAhom_{m-h}^{1/2}. This module builds those two matrices and pins them down; the loads themselves are built downstream.

Why no matrix functional calculus is needed

Because shom_m is a positive real, bfAhom_m is the scalar block diagonal blockDiag (sigma . 1) (sigma^{-1} . 1), so its square root and inverse square root are the elementary blockDiag (sqrt sigma . 1) ((sqrt sigma)^{-1} . 1) and blockDiag ((sqrt sigma)^{-1} . 1) (sqrt sigma . 1). Nothing here uses a spectral decomposition: the two matrices are pinned down by their action on a doubled load, which at a scalar block diagonal is elementary.

The carrier of the positive real is the repository's own running diffusivity type Algsuperdiff.Section3.Observable.PositiveScalar, on which positivity is part of the type; annealedLimitBlock_sigmaBar_characterization records that annealedLimitBlock (sigmaBar M m) really is the infinite-volume annealed limit of the genuine coefficient cutoff, and that no other positive scalar has that limit.

Main results

• annealedLimitBlock, annealedLimitBlockSqrt, annealedLimitBlockInvSqrt
• annealedLimitBlock_sigmaBar_characterization
• blockMatVecMul_annealedLimitBlockInvSqrt, blockMatVecMul_annealedLimitBlockSqrt: the two square roots act on a doubled load by the scalar loads inverseSqrtLoad and sqrtLoad.

The three matrices

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.annealedLimitBlock {d : ℕ} (sigma : Observable.PositiveScalar) : HCPolySupport.BlockMat d

e.homs.defs. The deterministic infinite-volume annealed doubled matrix bfAhom_m = ((shom_m, 0), (0, shom_m^{-1})) at a positive scalar shom_m.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.annealedLimitBlock sigma = HCPolySupport.Book.Ch02.blockDiag (↑sigma • 1) ((↑sigma)⁻¹ • 1)

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.annealedLimitBlockSqrt {d : ℕ} (sigma : Observable.PositiveScalar) : HCPolySupport.BlockMat d

The square root bfAhom_m^{1/2} used.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.annealedLimitBlockSqrt sigma = HCPolySupport.Book.Ch02.blockDiag (√↑sigma • 1) ((√↑sigma)⁻¹ • 1)

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.annealedLimitBlockInvSqrt {d : ℕ} (sigma : Observable.PositiveScalar) : HCPolySupport.BlockMat d

The inverse square root bfAhom_m^{-1/2} used at e.recurrence.P.def and e.Pz.def.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.annealedLimitBlockInvSqrt sigma = HCPolySupport.Book.Ch02.blockDiag ((√↑sigma)⁻¹ • 1) (√↑sigma • 1)

The annealed limit really is the infinite-volume annealed limit

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.annealedLimitBlock_sigmaBar_characterization {d : ℕ} (M : ABKModel d) (m : ℤ) : Filter.Tendsto (fun (n : ℕ) => HCPolySupport.toFullBlockMat (HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale (Cutoff.coefficientCutoffLaw M m) ↑n)) Filter.atTop (nhds (HCPolySupport.toFullBlockMat (annealedLimitBlock (Annealed.sigmaBar M m)))) ∧ ∀ (other : Observable.PositiveScalar), Filter.Tendsto (fun (n : ℕ) => HCPolySupport.toFullBlockMat (HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale (Cutoff.coefficientCutoffLaw M m) ↑n)) Filter.atTop (nhds (HCPolySupport.toFullBlockMat (annealedLimitBlock other))) → other = Annealed.sigmaBar M m

e.homs.defs at the genuine cutoff. The doubled annealed matrices of the genuine coefficient cutoff converge to annealedLimitBlock (sigmaBar M m), and no other positive scalar produces that limit. This is Annealed.sigmaBar_characterization read through annealedLimitBlock.

Elementary block algebra of the scalar block diagonals

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.matVecMul_smul_one {d : ℕ} (c : ℝ) (x : HCPolySupport.Vec d) : HCPolySupport.matVecMul (c • 1) x = c • x

A scalar multiple of the identity acts on a vector by that scalar.

The defining property: the square is the inverse

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.blockMatVecMul_blockMatMul {d : ℕ} (A B : HCPolySupport.BlockMat d) (X : HCPolySupport.BlockVec d) : HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.blockMatMul A B) X = HCPolySupport.blockMatVecMul A (HCPolySupport.blockMatVecMul B X)

Doubled matrix-vector multiplication is compatible with doubled matrix multiplication.

Symmetry and positivity

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.blockMatVecMul_blockDiag_smul_one {d : ℕ} (a b : ℝ) (X : HCPolySupport.BlockVec d) : HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.blockDiag (a • 1) (b • 1)) X = (a • X.1, b • X.2)

The action of a scalar block diagonal on a doubled vector.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.blockVecDot_blockMatVecMul_blockDiag_smul_one {d : ℕ} (a b : ℝ) (X : HCPolySupport.BlockVec d) : HCPolySupport.blockVecDot X (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.blockDiag (a • 1) (b • 1)) X) = a * HCPolySupport.vecNormSq X.1 + b * HCPolySupport.vecNormSq X.2

The doubled quadratic form of a scalar block diagonal.

The inverse square root acting on a doubled load

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.blockMatVecMul_annealedLimitBlockInvSqrt {d : ℕ} (sigma : Observable.PositiveScalar) (u v : HCPolySupport.Vec d) : HCPolySupport.blockMatVecMul (annealedLimitBlockInvSqrt sigma) (u, v) = (Observable.inverseSqrtLoad sigma u, Observable.sqrtLoad sigma v)

The inverse square root acts on a doubled load by the two scalar loads of Observable.inverseSqrtLoad and Observable.sqrtLoad.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.blockMatVecMul_annealedLimitBlockSqrt {d : ℕ} (sigma : Observable.PositiveScalar) (u v : HCPolySupport.Vec d) : HCPolySupport.blockMatVecMul (annealedLimitBlockSqrt sigma) (u, v) = (Observable.sqrtLoad sigma u, Observable.inverseSqrtLoad sigma v)

The square root acts on a doubled load by the two scalar loads, swapped.