PrincipalResponsePDef

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

Provider: the principal load P of e.recurrence.P.def, and why it collapses

Source displays in ABK26:

• e.recurrence.P.def (label; display) sets, for e, e' in R^d with |e|, |e'| <= 1,

  P := bfAhom_{m-h}^{-1/2} (e'; e)   in R^{2d} .
  

  The manuscript's column has e' on the potential leg and e on the flux leg; that order is preserved below.
• Step 6 of the proof of l.approximate.recurrence.formula opens with the identity

  (e'; e) . bfAhom_{m-h}^{-1/2} bfAhom_m bfAhom_{m-h}^{-1/2} (e'; e)
      = P . bfAhom_m P ,
  

  then splits into the two cases e = 0 and e' = 0. The reason the whole construction is set up this way is that with bfAhom_k = ((shom_k, 0), (0, shom_k^{-1})) the conjugated matrix is again a scalar block diagonal, with entries shom_m / shom_{m-h} and its reciprocal; the two cases read off one entry each. That collapse is proved here.

What is not fixed here

The manuscript's localization scale is n = m - h - 16 ceil |log_3 gamma| (e.recurrence.params, display, label). Nothing in this module mentions a localization scale, so the literal 16 appears nowhere and the buffer stays a free parameter for the modules that need it.

Main results

• principalLoad, recurrenceP
• recurrenceP_eq, recurrenceP_fst, recurrenceP_snd
• blockVecDot_recurrenceP_annealedLimitBlock
• blockVecDot_recurrenceP_annealedLimitBlock_potential_unit and ..._flux_unit, the two unit cases, returning the reciprocal diffusivity ratios shom_m / shom_{m-h} and shom_{m-h} / shom_m

The normalization map

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

The action of bfAhom^{-1/2} on a doubled load. This is the operation applied in e.recurrence.P.def, in e.Pz.def and in e.Fz.def.

Equations

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.principalLoad_eq {d : ℕ} (sigma : Observable.PositiveScalar) (X : HCPolySupport.BlockVec d) : principalLoad sigma X = (Observable.inverseSqrtLoad sigma X.1, Observable.sqrtLoad sigma X.2)

The two legs of the normalization: sigma^{-1/2} on the potential leg and sigma^{1/2} on the flux leg.

@[simp]

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.principalLoad_fst {d : ℕ} (sigma : Observable.PositiveScalar) (X : HCPolySupport.BlockVec d) : (principalLoad sigma X).1 = Observable.inverseSqrtLoad sigma X.1

@[simp]

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.principalLoad_snd {d : ℕ} (sigma : Observable.PositiveScalar) (X : HCPolySupport.BlockVec d) : (principalLoad sigma X).2 = Observable.sqrtLoad sigma X.2

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.principalLoad_add {d : ℕ} (sigma : Observable.PositiveScalar) (X Y : HCPolySupport.BlockVec d) : principalLoad sigma (X + Y) = principalLoad sigma X + principalLoad sigma Y

The normalization is additive.

The load P of e.recurrence.P.def

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.recurrenceP {d : ℕ} (sigma : Observable.PositiveScalar) (e e' : HCPolySupport.Vec d) : HCPolySupport.BlockVec d

e.recurrence.P.def. The probe load P = bfAhom_{m-h}^{-1/2} (e'; e), at the positive scalar sigma = shom_{m-h}.

The manuscript's constraint |e|, |e'| <= 1 is a constraint on the use of P in the estimates downstream, not part of the display defining it, and is therefore not a binder here.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.recurrenceP sigma e e' = Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.principalLoad sigma (e', e)

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.recurrenceP_eq {d : ℕ} (sigma : Observable.PositiveScalar) (e e' : HCPolySupport.Vec d) : recurrenceP sigma e e' = (Observable.inverseSqrtLoad sigma e', Observable.sqrtLoad sigma e)

The two legs of P.

@[simp]

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.recurrenceP_fst {d : ℕ} (sigma : Observable.PositiveScalar) (e e' : HCPolySupport.Vec d) : (recurrenceP sigma e e').1 = Observable.inverseSqrtLoad sigma e'

@[simp]

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.recurrenceP_snd {d : ℕ} (sigma : Observable.PositiveScalar) (e e' : HCPolySupport.Vec d) : (recurrenceP sigma e e').2 = Observable.sqrtLoad sigma e

The collapse

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.blockVecDot_recurrenceP_annealedLimitBlock {d : ℕ} (sigmaTop sigmaLow : Observable.PositiveScalar) (e e' : HCPolySupport.Vec d) : HCPolySupport.blockVecDot (recurrenceP sigmaLow e e') (HCPolySupport.blockMatVecMul (annealedLimitBlock sigmaTop) (recurrenceP sigmaLow e e')) = ↑sigmaTop / ↑sigmaLow * HCPolySupport.vecNormSq e' + ↑sigmaLow / ↑sigmaTop * HCPolySupport.vecNormSq e

, right-hand reading. The doubled quadratic form of bfAhom_m at the probe load P = bfAhom_{m-h}^{-1/2}(e'; e) collapses to two scalar terms with the reciprocal coefficients shom_m / shom_{m-h} and shom_{m-h} / shom_m.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.blockVecDot_recurrenceP_annealedLimitBlock_potential_unit {d : ℕ} (sigmaTop sigmaLow : Observable.PositiveScalar) {e' : HCPolySupport.Vec d} (he' : HCPolySupport.vecNormSq e' = 1) : HCPolySupport.blockVecDot (recurrenceP sigmaLow 0 e') (HCPolySupport.blockMatVecMul (annealedLimitBlock sigmaTop) (recurrenceP sigmaLow 0 e')) = ↑sigmaTop / ↑sigmaLow

, the case e = 0. Probing with a unit potential direction returns exactly the diffusivity ratio shom_m / shom_{m-h}.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.blockVecDot_recurrenceP_annealedLimitBlock_flux_unit {d : ℕ} (sigmaTop sigmaLow : Observable.PositiveScalar) {e : HCPolySupport.Vec d} (he : HCPolySupport.vecNormSq e = 1) : HCPolySupport.blockVecDot (recurrenceP sigmaLow e 0) (HCPolySupport.blockMatVecMul (annealedLimitBlock sigmaTop) (recurrenceP sigmaLow e 0)) = ↑sigmaLow / ↑sigmaTop

, the case e' = 0. Probing with a unit flux direction returns the reciprocal ratio shom_{m-h} / shom_m.