ResponseJ

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

Section 3 normalized response observable

This file defines the genuine scalar response observable on the centered cube square_m. For a positive comparator sigma and a direction e, its loads are exactly sigma^(-1/2) e and sigma^(1/2) e. The coefficient argument is an actual CoarseGraining RegCoeffField; later cutoff-specific declarations merely compose this map with the genuine cutoff field.

References

• ABK26, (2.4), definition of J(U,p,q;a).
• ABK26, Section 2.5 and Section 3 response normalizations.

noncomputable def Algsuperdiff.Section3.Observable.responseJAtScale {d : ℕ} (m : ℤ) (sigma : PositiveScalar) (e : HCPolySupport.Vec d) : HCPolySupport.RegCoeffField d → ℝ

The response observable a ↦ J(square_m, sigma^(-1/2)e, sigma^(1/2)e; a).

Equations

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

theorem Algsuperdiff.Section3.Observable.responseJAtScale_nonneg {d : ℕ} (m : ℤ) (sigma : PositiveScalar) (e : HCPolySupport.Vec d) (a : HCPolySupport.RegCoeffField d) : 0 ≤ responseJAtScale m sigma e a

The normalized scalar response is pointwise nonnegative.