RegCoeffFieldOperations

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

Value operations on regular coefficient fields

This module supplies measurable constant value scaling and negation for CoarseGraining's RegCoeffField carrier. It also packages the value-scaled triadic spatial dilation used by multiscale field layers.

def Algsuperdiff.Probability.scaleReg {d : ℕ} (c : ℝ) (a : HCPolySupport.RegCoeffField d) : HCPolySupport.RegCoeffField d

Scale every matrix value of a regular coefficient field by a fixed real constant.

Equations

• Algsuperdiff.Probability.scaleReg c a = c • a

def Algsuperdiff.Probability.negReg {d : ℕ} (a : HCPolySupport.RegCoeffField d) : HCPolySupport.RegCoeffField d

Negate every matrix value of a regular coefficient field.

Equations

• Algsuperdiff.Probability.negReg a = Algsuperdiff.Probability.scaleReg (-1) a

@[simp]

theorem Algsuperdiff.Probability.negReg_apply {d : ℕ} (a : HCPolySupport.RegCoeffField d) (x : HCPolySupport.Vec d) : (negReg a).toFun x = -a.toFun x

noncomputable def Algsuperdiff.Probability.triadicLayerScaleReg {d : ℕ} (γ : ℝ) (k : ℤ) (a : HCPolySupport.RegCoeffField d) : HCPolySupport.RegCoeffField d

Apply the triadic spatial dilation at index k and scale the resulting field values by 3 ^ (γ k).

Equations

• Algsuperdiff.Probability.triadicLayerScaleReg γ k a = Algsuperdiff.Probability.scaleReg (Real.rpow 3 (γ * ↑k)) (HCPolySupport.dilateReg k a)