PrincipalResponseSwitch

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 cube-to-annealed switch of e.use.also.for.the.upper.bound

This module supplies the matrix content of the annealed switch e.use.also.for.the.upper.bound of ABK26, whose statement is the display and whose proof is. The manuscript's display reads

  E[ | bfAhom_{m-h}^{1/2}(z + cu_n) G_{-(h)_{z+cu_n}} P_z |^2 ]
    <=  (1 + C E^2 |log gamma|^2 gamma)
          E[ | bfAhom_{m-h}^{1/2} G_{-(h)_{z+cu_n}} P_z |^2 ] ,

and its proof runs entirely through the deterministic matrix bound

  | bfAhom_{m-h}^{-1/2} bfAhom_{m-h}(cu_n) bfAhom_{m-h}^{-1/2} - I_{2d} |
    <= 2 max_{|e|=1} E[ bfJ(cu_n, bfAhom_{m-h}^{-1/2} e, bfAhom_{m-h}^{1/2} e; a_{m-h}) ] .

What is proved here is that deterministic bound, in the equivalent vector-uniform Loewner form

  bfAhom_L(cu_n)  <=  (1 + delta) bfAhom_L    (as quadratic forms on every
                                               doubled vector) ,
  delta := 2 E[ bfJ(cu_n, bfAhom_L^{-1/2} e, bfAhom_L^{1/2} e; a_L) ] ,

at the cutoff index L. The manuscript's display for the specific random vector G_{-(h)_{z+cu_n}} P_z follows from this by monotonicity of the integral, so no statement below mentions P_z; see "What is not here".

The chain, and where each printed step goes

• bfAhom_L <= bfAhom_L(cu_n) (the right half of the sandwich printed) is blockMatLoewnerLE_annealedBlockMatrixAtScale_annealedLimit of ...ApproximateRecurrence.PrincipalResponseSwitchPlateau.
• The annealed probe (bfAhom_L^{-1/2} e, bfAhom_L^{1/2} e) of ABK26 is annealedProbePotential / annealedProbeFlux; blockVecDot_annealedProbePotential_annealedProbeFlux records that the two reciprocal square roots of the block-diagonal bfAhom_L of e.homs.defs cancel in the doubled pairing, so the printed normalization |e| = 1 is exactly P . Q = 1 for that pair.
• The factor 2 of comes out of the Chapter 2 doubled-response splitting rather than out of the completed square e.bfJ.magic: on the block-diagonal annealed carrier of e.homs.defs.U.diag the splitting gives the exact identity `(x -
  1. • (y - 1) = 2 E[bfJ]withx := sigmahom_L(cu_n)/sigmahom_Landy:= sigmahom_L/sigmahom_{L,*}(cu_n), both summands nonnegative by the plateau ordering, so the nonnegative square that e.bfJ.magicdiscards is not needed. `cubeAnnealedProbeDefect_eq_two_mul_integral_blockJbelow is that identity. Its integrand is CoarseGraining'sCh04.blockJObservableCubeSetBlockVec, which is Ch02.doubledResponseJ-- the manuscript'sbfJ-- on every a.e. locally uniformly elliptic field, by CoarseGraining's `Ch04.doubledResponseJ_eq_blockJObservableCubeSetBlockVec_of_aelocallyUniformlyEllipticField`.

What is not here

The manuscript's own budget delta <=^2 |log gamma|^2 gamma is not proved here. It needs e.bound.one.cube.by.mathcalE, e.mathcalE.monotone.ordered and, crucially, the induction hypothesis e.new.induction.for.shom at t = |log gamma|^{-1} in the form of a second moment of mathcal E_{t,infinity,2}; none of those is consumed below. Nothing here therefore claims any source node, or any fraction of one. The specific random vector G_{-(h)_{z+cu_n}} P_z of the printed display is likewise absent: P_z has no definition in this repository yet, and the Loewner form below is exactly what specializes to it in one step once it does.

The cube below is the origin cube cu_n, not the translate z + cu_n printed in the display. The two annealed matrices agree by real-translation stationarity of the genuine cutoff law, which is the transfer already used inside Provider.Annealed.Monotonicity; that transfer is not re-exported here, so a consumer working at a translated cube still owes that one step.

Main results

• annealedProbePotential, annealedProbeFlux: the tex probe pair.
• cubeAnnealedProbeDefect: the annealed defect delta.
• cubeAnnealedProbeDefect_eq_two_mul_integral_blockJ: delta is twice the annealed doubled response at the probe, i.e. the manuscript's quantity at that probe.
• cubeAnnealedProbeDefect_eq_of_blockDiag: delta on a scalar block-diagonal annealed cube matrix, in the closed form (sigma^{-1} s + sigma t - 2) |E|^2.
• annealedCubeBlockQuadratic_le_annealedLimitBlockQuadratic: the switch, as a quadratic-form inequality on an arbitrary doubled vector.

References

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

The probe pair (bfAhom^{-1/2} e, bfAhom^{1/2} e)

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.annealedProbePotential {d : ℕ} (sigma : Observable.PositiveScalar) (E : HCPolySupport.BlockVec d) : HCPolySupport.BlockVec d

The doubled vector bfAhom^{-1/2} e at the block-diagonal annealed limit bfAhom = diag(sigma, sigma^{-1}) of e.homs.defs.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.annealedProbeFlux {d : ℕ} (sigma : Observable.PositiveScalar) (E : HCPolySupport.BlockVec d) : HCPolySupport.BlockVec d

The doubled vector bfAhom^{1/2} e at the block-diagonal annealed limit bfAhom = diag(sigma, sigma^{-1}) of e.homs.defs.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.blockVecDot_annealedProbePotential_annealedProbeFlux {d : ℕ} (sigma : Observable.PositiveScalar) (E : HCPolySupport.BlockVec d) : HCPolySupport.blockVecDot (annealedProbePotential sigma E) (annealedProbeFlux sigma E) = HCPolySupport.blockVecDot E E

The probe pair is dual: its doubled pairing is the squared norm of the direction, so the tex normalization |e| = 1 is exactly P . Q = 1.

The annealed defect

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.cubeAnnealedProbeDefect {d : ℕ} (M : ABKModel d) (L n : ℤ) (E : HCPolySupport.BlockVec d) : ℝ

The annealed defect delta of ABK26, at the cutoff index L, the cube scale n and the unit direction E: twice the annealed doubled response of the cube cu_n at the probe pair (bfAhom_L^{-1/2} E, bfAhom_L^{1/2} E).

It is written here through CoarseGraining's algebraic doubled-response value Ch04.blockJQuadraticFullBlockMat evaluated at the annealed block matrix, which is exactly the expectation of the Chapter 2 doubled-response splitting; cubeAnnealedProbeDefect_eq_two_mul_integral_blockJ identifies it with the expectation of the doubled response itself.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.blockJQuadraticFullBlockMat_toFullBlockMat {d : ℕ} (A : HCPolySupport.BlockMat d) (P Q : HCPolySupport.BlockVec d) : HCPolySupport.Book.Ch04.blockJQuadraticFullBlockMat (HCPolySupport.toFullBlockMat A) P Q = 1 / 2 * HCPolySupport.blockVecDot P (HCPolySupport.blockMatVecMul A P) + 1 / 2 * HCPolySupport.blockVecDot (Q.2, Q.1) (HCPolySupport.blockMatVecMul A (Q.2, Q.1)) - HCPolySupport.blockVecDot P Q

CoarseGraining's algebraic doubled-response value, written in doubled-block form. This is the Chapter 2 splitting bfJ = 1/2 P. bfA P + 1/2 Q. bfA_*^{-1} Q - P. Q, with bfA_*^{-1} the block reflection of bfA.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.cubeAnnealedProbeDefect_eq_of_blockDiag {d : ℕ} (M : ABKModel d) (L n : ℤ) {s t : ℝ} (hst : HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale (Cutoff.coefficientCutoffLaw M L) n = HCPolySupport.Book.Ch02.blockDiag (s • 1) (t • 1)) (E : HCPolySupport.BlockVec d) : cubeAnnealedProbeDefect M L n E = ((↑(Annealed.sigmaBar M L))⁻¹ * s + ↑(Annealed.sigmaBar M L) * t - 2) * HCPolySupport.blockVecDot E E

The defect on a scalar block-diagonal annealed cube matrix: with bfAhom_L(cu_n) = diag(s, t) and bfAhom_L = diag(sigma, sigma^{-1}),

delta = (sigma^{-1} s + sigma t - 2) |E|^2.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.exists_blockVecDot_self_eq_one {d : ℕ} [NeZero d] : ∃ (E : HCPolySupport.BlockVec d), HCPolySupport.blockVecDot E E = 1

Non-vacuity of the normalization |e| = 1 used below: unit doubled directions exist.

The switch

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.annealedCubeBlockQuadratic_le_annealedLimitBlockQuadratic {d : ℕ} [NeZero d] (M : ABKModel d) (L n : ℤ) {E : HCPolySupport.BlockVec d} (hE : HCPolySupport.blockVecDot E E = 1) (V : HCPolySupport.BlockVec d) : HCPolySupport.blockVecDot V (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch04.annealedBlockMatrixAtScale (Cutoff.coefficientCutoffLaw M L) n) V) ≤ (1 + cubeAnnealedProbeDefect M L n E) * HCPolySupport.blockVecDot V (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.blockDiag (↑(Annealed.sigmaBar M L) • 1) ((↑(Annealed.sigmaBar M L))⁻¹ • 1)) V)

e.use.also.for.the.upper.bound (ABK26), in the vector-uniform Loewner form.

At the cutoff index L and every cube scale n, the finite-cube annealed matrix bfAhom_L(cu_n) is dominated by (1 + delta) times the infinite-volume annealed matrix bfAhom_L = diag(sigmahom_L, sigmahom_L^{-1}) of e.homs.defs, as quadratic forms on an arbitrary doubled vector V, where delta = 2 E[bfJ(cu_n, bfAhom_L^{-1/2} E, bfAhom_L^{1/2} E; a_L)] is the defect of at any unit direction E.

Taking V := G_{-(h)_{z+cu_n}} P_z and integrating recovers the manuscript's printed display for that random vector; that specialization is not available in this repository yet, since P_z is not defined here. This theorem does not prove the manuscript's budget delta <=^2 |log gamma|^2 gamma and claims no source-node status.

The defect is the annealed doubled response of e.bfJ.magic's parent

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.cubeAnnealedProbeDefect_eq_two_mul_integral_blockJ {d : ℕ} [NeZero d] (M : ABKModel d) (L n : ℤ) (E : HCPolySupport.BlockVec d) : cubeAnnealedProbeDefect M L n E = 2 * ∫ (a : HCPolySupport.RegCoeffField d), HCPolySupport.Book.Ch04.blockJObservableCubeSetBlockVec (HCPolySupport.originCube d n) (annealedProbePotential (Annealed.sigmaBar M L) E) (annealedProbeFlux (Annealed.sigmaBar M L) E) a ∂Cutoff.coefficientCutoffLaw M L

ABK26, annealed. The defect is twice the expectation of the doubled response bfJ(cu_n, bfAhom_L^{-1/2} E, bfAhom_L^{1/2} E; a_L) under the genuine coefficient cutoff law at index L.

The proof is the Chapter 2 doubled-response splitting (the parent identity of e.bfJ.magic, ABK26) integrated entrywise; no completed square and no discarded nonnegative term appear.