Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section5.Field.ScaleDecomposition

ScaleDecomposition #

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

The low- and high-frequency parts of the stream field #

The normalized stream matrix is split at shell index zero. The negative shells form the rough, locally bounded part streamFieldSmall; the nonnegative shells form the differentiable part streamFieldLarge. Both series use the same normalization at the origin as streamField.

source
noncomputable def Algsuperdiff.Section5.Field.streamFieldSmall {d : ℕ} {gamma : ℝ} (omega : FullSample d gamma) (x : HCPolySupport.Vec d) :
HCPolySupport.Mat d

The normalized contribution of the shells with index strictly below zero.

Equations
Instances For
    source
    noncomputable def Algsuperdiff.Section5.Field.streamFieldLarge {d : ℕ} {gamma : ℝ} (omega : FullSample d gamma) (x : HCPolySupport.Vec d) :
    HCPolySupport.Mat d

    The normalized contribution of the shells with nonnegative index.

    Equations
    Instances For
      source
      @[simp]
      theorem Algsuperdiff.Section5.Field.streamFieldSmall_apply_entry {d : ℕ} {gamma : ℝ} (omega : FullSample d gamma) (x : HCPolySupport.Vec d) (i k : Fin d) :
      streamFieldSmall omega x i k = ∑' (r : ℕ), ((↑(↑↑omega (-1 - ↑r))).1 x i k - (↑(↑↑omega (-1 - ↑r))).1 0 i k)
      source
      @[simp]
      theorem Algsuperdiff.Section5.Field.streamFieldLarge_apply_entry {d : ℕ} {gamma : ℝ} (omega : FullSample d gamma) (x : HCPolySupport.Vec d) (i k : Fin d) :
      streamFieldLarge omega x i k = ∑' (r : ℕ), ((↑(↑↑omega ↑r)).1 x i k - (↑(↑↑omega ↑r)).1 0 i k)
      source
      theorem Algsuperdiff.Section5.Field.streamField_eq_small_add_large {d : ℕ} {gamma : ℝ} (omega : FullSample d gamma) (x : HCPolySupport.Vec d) :
      streamField omega x = streamFieldSmall omega x + streamFieldLarge omega x

      The normalized field is exactly the sum of its negative- and nonnegative-shell parts.

      source
      @[simp]
      theorem Algsuperdiff.Section5.Field.streamFieldSmall_zero {d : ℕ} {gamma : ℝ} (omega : FullSample d gamma) :
      streamFieldSmall omega 0 = 0
      source
      @[simp]
      theorem Algsuperdiff.Section5.Field.streamFieldLarge_zero {d : ℕ} {gamma : ℝ} (omega : FullSample d gamma) :
      streamFieldLarge omega 0 = 0
      source
      theorem Algsuperdiff.Section5.Field.streamFieldSmall_skew {d : ℕ} {gamma : ℝ} (omega : FullSample d gamma) (x : HCPolySupport.Vec d) :
      Matrix.transpose (streamFieldSmall omega x) = -streamFieldSmall omega x

      Every value of the negative-shell part is skew-symmetric.

      source
      theorem Algsuperdiff.Section5.Field.streamFieldLarge_skew {d : ℕ} {gamma : ℝ} (omega : FullSample d gamma) (x : HCPolySupport.Vec d) :
      Matrix.transpose (streamFieldLarge omega x) = -streamFieldLarge omega x

      Every value of the nonnegative-shell part is skew-symmetric.