Comparator

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

Positive scalar comparators for Section 3

Section 3 compares the random coefficient cutoff with the constant isotropic matrix sigmaBar_m Id. This file records that literal matrix and the two scalar load normalizations used in the response functional. Positivity is part of the scalar's type, so the inverse-square-root load is meaningful on the whole public carrier.

@[reducible, inline]

abbrev Algsuperdiff.Section3.Observable.PositiveScalar : Type

A strictly positive scalar, used for the running-diffusivity comparator.

Equations

• Algsuperdiff.Section3.Observable.PositiveScalar = { sigma : ℝ // 0 < sigma }

noncomputable def Algsuperdiff.Section3.Observable.isotropicComparatorMatrix {d : ℕ} (sigma : PositiveScalar) : HCPolySupport.Mat d

The constant isotropic coefficient sigma Id.

Equations

• Algsuperdiff.Section3.Observable.isotropicComparatorMatrix sigma = ↑sigma • 1

noncomputable def Algsuperdiff.Section3.Observable.inverseSqrtLoad {d : ℕ} (sigma : PositiveScalar) (e : HCPolySupport.Vec d) : HCPolySupport.Vec d

The primal load sigma^(-1/2) e, written using the positive square root.

Equations

• Algsuperdiff.Section3.Observable.inverseSqrtLoad sigma e = (√↑sigma)⁻¹ • e

noncomputable def Algsuperdiff.Section3.Observable.sqrtLoad {d : ℕ} (sigma : PositiveScalar) (e : HCPolySupport.Vec d) : HCPolySupport.Vec d

The dual load sigma^(1/2) e.

Equations

• Algsuperdiff.Section3.Observable.sqrtLoad sigma e = √↑sigma • e