Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Cutoff.Finite

Finite #

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

Finite infrared cutoff increments #

This module contains only the finite part of the infrared construction. The lower-infinite cutoff is not defined here: finiteLowerCutoff m q is the honest truncation over (m - q, m] and will later be sent to the lower infinite limit on the full-measure carrier.

source
@[reducible, inline]
abbrev Algsuperdiff.Section3.Cutoff.ShellSeq (d : ℕ) :
Type

The canonical sample carrier for the integer-indexed shell sequence.

Equations
Instances For
    source
    def Algsuperdiff.Section3.Cutoff.shellReg {d : ℕ} (omega : ShellSeq d) (n : ℤ) :
    HCPolySupport.RegCoeffField d

    The regular coefficient-field realization of one shell coordinate.

    Equations
    Instances For
      source
      theorem Algsuperdiff.Section3.Cutoff.measurable_shellReg {d : ℕ} (n : ℤ) :
      Measurable fun (omega : ShellSeq d) => shellReg omega n

      One shell coordinate, realized as a regular coefficient field, is measurable on the canonical sequence carrier.

      source
      def Algsuperdiff.Section3.Cutoff.finiteShellIncrement {d : ℕ} (omega : ShellSeq d) (n m : ℤ) :
      HCPolySupport.RegCoeffField d

      The finite stream increment \mathbf{k}_m-\mathbf{k}_n, namely the literal sum of shells with indices in (n,m].

      Equations
      Instances For
        source
        @[simp]
        theorem Algsuperdiff.Section3.Cutoff.finiteShellIncrement_apply {d : ℕ} (omega : ShellSeq d) (n m : ℤ) (x : HCPolySupport.Vec d) :
        (finiteShellIncrement omega n m).toFun x = ∑ k ∈ Finset.Ioc n m, (shellReg omega k).toFun x

        Matrix-valued evaluation formula for a finite stream increment.

        source
        @[simp]
        theorem Algsuperdiff.Section3.Cutoff.finiteShellIncrement_apply_entry {d : ℕ} (omega : ShellSeq d) (n m : ℤ) (x : HCPolySupport.Vec d) (i j : Fin d) :
        (finiteShellIncrement omega n m).toFun x i j = ∑ k ∈ Finset.Ioc n m, (↑(omega k)).1 x i j

        Entrywise evaluation formula for a finite stream increment.

        source
        theorem Algsuperdiff.Section3.Cutoff.measurable_finiteShellIncrement {d : ℕ} (n m : ℤ) :
        Measurable fun (omega : ShellSeq d) => finiteShellIncrement omega n m

        Finite stream increments are measurable as regular coefficient fields.

        source
        theorem Algsuperdiff.Section3.Cutoff.finiteShellIncrement_skew {d : ℕ} (omega : ShellSeq d) (n m : ℤ) (x : HCPolySupport.Vec d) :
        Matrix.transpose ((finiteShellIncrement omega n m).toFun x) = -(finiteShellIncrement omega n m).toFun x

        Every finite stream increment is antisymmetric.

        source
        def Algsuperdiff.Section3.Cutoff.finiteLowerCutoff {d : ℕ} (m : ℤ) (q : ℕ) (omega : ShellSeq d) :
        HCPolySupport.RegCoeffField d

        The finite lower truncation of the manuscript cutoff at scale m: the sum over (m-q,m]. It is finite data, not a lower-infinite replacement.

        Equations
        Instances For
          source
          @[simp]
          theorem Algsuperdiff.Section3.Cutoff.finiteLowerCutoff_apply {d : ℕ} (m : ℤ) (q : ℕ) (omega : ShellSeq d) (x : HCPolySupport.Vec d) :
          (finiteLowerCutoff m q omega).toFun x = ∑ k ∈ Finset.Ioc (m - ↑q) m, (shellReg omega k).toFun x

          Matrix-valued evaluation formula for the finite lower truncation.

          source
          @[simp]
          theorem Algsuperdiff.Section3.Cutoff.finiteLowerCutoff_apply_entry {d : ℕ} (m : ℤ) (q : ℕ) (omega : ShellSeq d) (x : HCPolySupport.Vec d) (i j : Fin d) :
          (finiteLowerCutoff m q omega).toFun x i j = ∑ k ∈ Finset.Ioc (m - ↑q) m, (↑(omega k)).1 x i j

          Entrywise evaluation formula for the finite lower truncation.

          source
          theorem Algsuperdiff.Section3.Cutoff.measurable_finiteLowerCutoff {d : ℕ} (m : ℤ) (q : ℕ) :
          Measurable fun (omega : ShellSeq d) => finiteLowerCutoff m q omega

          Finite lower truncations are measurable as regular coefficient fields.

          source
          theorem Algsuperdiff.Section3.Cutoff.finiteLowerCutoff_eq_sum_range_desc {d : ℕ} (m : ℤ) (q : ℕ) (omega : ShellSeq d) :
          finiteLowerCutoff m q omega = ∑ r ∈ Finset.range q, shellReg omega (m - ↑r)

          The finite lower cutoff is the descending partial sum \sum_{r < q} \mathbf j_{m-r}.

          source
          theorem Algsuperdiff.Section3.Cutoff.finiteLowerCutoff_apply_entry_eq_sum_range_desc {d : ℕ} (m : ℤ) (q : ℕ) (omega : ShellSeq d) (x : HCPolySupport.Vec d) (i j : Fin d) :
          (finiteLowerCutoff m q omega).toFun x i j = ∑ r ∈ Finset.range q, (↑(omega (m - ↑r))).1 x i j

          Entrywise descending-partial-sum formula for the finite lower cutoff.