7.4. Periodic convolution layers🔗

Example7.8

Statement uses 4

Statement dependency previews

Preview

Definition Aux.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

The torus \mathbb T^d=(\mathbb R/2\pi\mathbb Z)^d with normalized Haar measure, H=L^2(\mathbb T^d;\mathbb R) and Y=L^2(\mathbb T^d), the translations (\tau_zx)(t)=x(t-z), the convolution-layer data a_y=k(y-\cdot) and b_y=\psi(\cdot-y), the constant function 1, the characters e_n(t)=e^{i\langle n,t\rangle} and Fourier coefficients \widehat f(n), and the Bessel operator (I-\Delta)^{-s}, multiplying the n-th Fourier coefficient by (1+|n|^2)^{-s}.

Let k,\psi\in L^2(\mathbb T^d;\mathbb R), a_y=k(y-\cdot), and b_y=\psi(\cdot-y). Then \langle a_y,x\rangle=(k*x)(y) (i), the layer is \mathcal F(x)=\psi*\beta(k*x) (ii), \|A\|_\infty=\|k\|_2 (iii), \int\|b_y\|\mathrm dy=\|\psi\|_2 (iv), the standing hypotheses hold (v), and \mathcal F commutes with all translations (vi) and with every isometry of \mathbb T^d fixing k and \psi (vii). If \widehat k(n)\ne0 for infinitely many n, then A has infinite rank (viii); with \varphi\equiv1, F_1(x)=\widehat\psi(0)\int_{\mathbb T^d}\beta((k*x)(y))\mathrm dy (ix), which is not cylindrical when moreover \widehat\psi(0)\ne0 (x). The operator (I-\Delta)^{-s} with s>d/2 is an injective trace-class covariance (xi) and translation invariant (xii), and for Q=P=(I-\Delta)^{-s} the transform is equivariant: R_\rho[f\circ\tau_z](a,c)=R_\rho f(\tau_za,c) (xiii).

Lean code for Example7.8●26 declarations

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_8_i (d : ℕ)
  (k x : OperatorRidgelet.TorusL2 d) (y : OperatorRidgelet.Torus d) :
  inner ℝ (OperatorRidgelet.convDirection k y) x =
    ∫ (t : OperatorRidgelet.Torus d),
      ↑↑k (y - t) * ↑↑x t ∂OperatorRidgelet.torusHaar d

theorem OperatorRidgelet.Paper.ex_7_8_i (d : ℕ)
  (k x : OperatorRidgelet.TorusL2 d)
  (y : OperatorRidgelet.Torus d) :
  inner ℝ
      (OperatorRidgelet.convDirection k y)
      x =
    ∫ (t : OperatorRidgelet.Torus d),
      ↑↑k (y - t) *
        ↑↑x
          t ∂OperatorRidgelet.torusHaar d

**Example [ex:7.8]** Periodic convolution layer.  With `a_y = k(y - ·)`,
`⟨a_y, x⟩ = (k * x)(y)`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_8_ii (d : ℕ)
  (k ψ : OperatorRidgelet.TorusL2 d) (β : ℝ → ℝ) (hβc : Continuous β)
  (hβp : OperatorRidgelet.HasPolynomialGrowth β)
  (x : OperatorRidgelet.TorusL2 d) :
  ↑↑(OperatorRidgelet.operatorLayer (OperatorRidgelet.torusHaar d)
          (OperatorRidgelet.convDirection k)
          (OperatorRidgelet.convOutput ψ) β
          x) =ᵐ[OperatorRidgelet.torusHaar d]
    fun t =>
    ∫ (y : OperatorRidgelet.Torus d),
      ↑(↑↑ψ (t - y) *
          β
            (inner ℝ (OperatorRidgelet.convDirection k y)
              x)) ∂OperatorRidgelet.torusHaar d

theorem OperatorRidgelet.Paper.ex_7_8_ii (d : ℕ)
  (k ψ : OperatorRidgelet.TorusL2 d)
  (β : ℝ → ℝ) (hβc : Continuous β)
  (hβp :
    OperatorRidgelet.HasPolynomialGrowth
      β)
  (x : OperatorRidgelet.TorusL2 d) :
  ↑↑(OperatorRidgelet.operatorLayer
          (OperatorRidgelet.torusHaar d)
          (OperatorRidgelet.convDirection
            k)
          (OperatorRidgelet.convOutput ψ)
          β
          x) =ᵐ[OperatorRidgelet.torusHaar
      d]
    fun t =>
    ∫ (y : OperatorRidgelet.Torus d),
      ↑(↑↑ψ (t - y) *
          β
            (inner ℝ
              (OperatorRidgelet.convDirection
                k y)
              x)) ∂OperatorRidgelet.torusHaar
        d

**Example [ex:7.8]** Periodic convolution layer.  With `a_y = k(y - ·)` and
`b_y = ψ(· - y)`, the layer is `ℱ(x) = ψ * β(k * x)`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_8_iii (d : ℕ)
  (k : OperatorRidgelet.TorusL2 d) :
  OperatorRidgelet.layerSupNorm (OperatorRidgelet.convDirection k) = ‖k‖

theorem OperatorRidgelet.Paper.ex_7_8_iii (d : ℕ)
  (k : OperatorRidgelet.TorusL2 d) :
  OperatorRidgelet.layerSupNorm
      (OperatorRidgelet.convDirection k) =
    ‖k‖

**Example [ex:7.8]** Periodic convolution layer.  `‖A‖_∞ = ‖k‖₂`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_8_iv (d : ℕ)
  (ψ : OperatorRidgelet.TorusL2 d) :
  ∫ (y : OperatorRidgelet.Torus d),
      ‖OperatorRidgelet.convOutput ψ y‖ ∂OperatorRidgelet.torusHaar d =
    ‖ψ‖

theorem OperatorRidgelet.Paper.ex_7_8_iv (d : ℕ)
  (ψ : OperatorRidgelet.TorusL2 d) :
  ∫ (y : OperatorRidgelet.Torus d),
      ‖OperatorRidgelet.convOutput ψ
          y‖ ∂OperatorRidgelet.torusHaar
        d =
    ‖ψ‖

**Example [ex:7.8]** Periodic convolution layer.  `∫ ‖b_y‖ dy = ‖ψ‖₂`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_8_v (d : ℕ)
  (k ψ : OperatorRidgelet.TorusL2 d) :
  OperatorRidgelet.IsLayerData (OperatorRidgelet.torusHaar d)
    (OperatorRidgelet.convDirection k) (OperatorRidgelet.convOutput ψ)

theorem OperatorRidgelet.Paper.ex_7_8_v (d : ℕ)
  (k ψ : OperatorRidgelet.TorusL2 d) :
  OperatorRidgelet.IsLayerData
    (OperatorRidgelet.torusHaar d)
    (OperatorRidgelet.convDirection k)
    (OperatorRidgelet.convOutput ψ)

**Example [ex:7.8]** Periodic convolution layer.  The convolution layer satisfies the
standing hypotheses of the neural-operator layer (`y ↦ a_y`, `y ↦ b_y` are continuous and
bounded into `L²`), so Example `ex:7.6` applies.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_8_vi (d : ℕ)
  (k ψ : OperatorRidgelet.TorusL2 d) (β : ℝ → ℝ) (hβc : Continuous β)
  (hβp : OperatorRidgelet.HasPolynomialGrowth β)
  (z : OperatorRidgelet.Torus d) (x : OperatorRidgelet.TorusL2 d) :
  OperatorRidgelet.operatorLayer (OperatorRidgelet.torusHaar d)
      (OperatorRidgelet.convDirection k) (OperatorRidgelet.convOutput ψ)
      β ((OperatorRidgelet.torusTranslate d z) x) =
    (OperatorRidgelet.torusTranslateC d z)
      (OperatorRidgelet.operatorLayer (OperatorRidgelet.torusHaar d)
        (OperatorRidgelet.convDirection k)
        (OperatorRidgelet.convOutput ψ) β x)

theorem OperatorRidgelet.Paper.ex_7_8_vi (d : ℕ)
  (k ψ : OperatorRidgelet.TorusL2 d)
  (β : ℝ → ℝ) (hβc : Continuous β)
  (hβp :
    OperatorRidgelet.HasPolynomialGrowth
      β)
  (z : OperatorRidgelet.Torus d)
  (x : OperatorRidgelet.TorusL2 d) :
  OperatorRidgelet.operatorLayer
      (OperatorRidgelet.torusHaar d)
      (OperatorRidgelet.convDirection k)
      (OperatorRidgelet.convOutput ψ) β
      ((OperatorRidgelet.torusTranslate d
          z)
        x) =
    (OperatorRidgelet.torusTranslateC d z)
      (OperatorRidgelet.operatorLayer
        (OperatorRidgelet.torusHaar d)
        (OperatorRidgelet.convDirection k)
        (OperatorRidgelet.convOutput ψ) β
        x)

**Example [ex:7.8]** Periodic convolution layer.  `ℱ` commutes with all translations
of `𝕋^d`: `ℱ(τ_z x) = τ_z ℱ(x)`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_8_vii (d : ℕ)
  (k ψ : OperatorRidgelet.TorusL2 d) (β : ℝ → ℝ) (hβc : Continuous β)
  (hβp : OperatorRidgelet.HasPolynomialGrowth β)
  (σ : OperatorRidgelet.Torus d ≃+ OperatorRidgelet.Torus d) :
  Isometry ⇑σ →
    ∀
      (hσ :
        MeasureTheory.MeasurePreserving (⇑σ)
          (OperatorRidgelet.torusHaar d)
          (OperatorRidgelet.torusHaar d)),
      (fun t => ↑↑k (σ t)) =ᵐ[OperatorRidgelet.torusHaar d] ↑↑k →
        (fun t => ↑↑ψ (σ t)) =ᵐ[OperatorRidgelet.torusHaar d] ↑↑ψ →
          ∀ (x : OperatorRidgelet.TorusL2 d),
            OperatorRidgelet.operatorLayer
                (OperatorRidgelet.torusHaar d)
                (OperatorRidgelet.convDirection k)
                (OperatorRidgelet.convOutput ψ) β
                ((MeasureTheory.Lp.compMeasurePreserving (⇑σ) hσ) x) =
              (MeasureTheory.Lp.compMeasurePreserving (⇑σ) hσ)
                (OperatorRidgelet.operatorLayer
                  (OperatorRidgelet.torusHaar d)
                  (OperatorRidgelet.convDirection k)
                  (OperatorRidgelet.convOutput ψ) β x)

theorem OperatorRidgelet.Paper.ex_7_8_vii (d : ℕ)
  (k ψ : OperatorRidgelet.TorusL2 d)
  (β : ℝ → ℝ) (hβc : Continuous β)
  (hβp :
    OperatorRidgelet.HasPolynomialGrowth
      β)
  (σ :
    OperatorRidgelet.Torus d ≃+
      OperatorRidgelet.Torus d) :
  Isometry ⇑σ →
    ∀
      (hσ :
        MeasureTheory.MeasurePreserving
          (⇑σ)
          (OperatorRidgelet.torusHaar d)
          (OperatorRidgelet.torusHaar d)),
      (fun t =>
            ↑↑k
              (σ
                t)) =ᵐ[OperatorRidgelet.torusHaar
            d]
          ↑↑k →
        (fun t =>
              ↑↑ψ
                (σ
                  t)) =ᵐ[OperatorRidgelet.torusHaar
              d]
            ↑↑ψ →
          ∀
            (x :
              OperatorRidgelet.TorusL2 d),
            OperatorRidgelet.operatorLayer
                (OperatorRidgelet.torusHaar
                  d)
                (OperatorRidgelet.convDirection
                  k)
                (OperatorRidgelet.convOutput
                  ψ)
                β
                ((MeasureTheory.Lp.compMeasurePreserving
                    (⇑σ) hσ)
                  x) =
              (MeasureTheory.Lp.compMeasurePreserving
                  (⇑σ) hσ)
                (OperatorRidgelet.operatorLayer
                  (OperatorRidgelet.torusHaar
                    d)
                  (OperatorRidgelet.convDirection
                    k)
                  (OperatorRidgelet.convOutput
                    ψ)
                  β x)

**Example [ex:7.8]** Periodic convolution layer.  `ℱ` commutes with every isometry
`σ` of `𝕋^d` (an isometric automorphism of the group, measure preserving) that fixes `k` and
`ψ`: `ℱ(x ∘ σ) = ℱ(x) ∘ σ`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_8_viii (d : ℕ)
  (k : OperatorRidgelet.TorusL2 d)
  (hk :
    {n |
        OperatorRidgelet.torusFourierCoeff (fun t => ↑(↑↑k t)) n ≠
          0}.Infinite) :
  OperatorRidgelet.HasInfiniteRank
    (OperatorRidgelet.layerA (OperatorRidgelet.torusHaar d)
      (OperatorRidgelet.convDirection k))

theorem OperatorRidgelet.Paper.ex_7_8_viii (d : ℕ)
  (k : OperatorRidgelet.TorusL2 d)
  (hk :
    {n |
        OperatorRidgelet.torusFourierCoeff
            (fun t => ↑(↑↑k t)) n ≠
          0}.Infinite) :
  OperatorRidgelet.HasInfiniteRank
    (OperatorRidgelet.layerA
      (OperatorRidgelet.torusHaar d)
      (OperatorRidgelet.convDirection k))

**Example [ex:7.8]** Periodic convolution layer.  If `k̂(n) ≠ 0` for infinitely many
`n ∈ ℤ^d`, then `A` has infinite rank.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_8_ix (d : ℕ)
  (k ψ : OperatorRidgelet.TorusL2 d) (β : ℝ → ℝ) (hβc : Continuous β)
  (hβp : OperatorRidgelet.HasPolynomialGrowth β)
  (x : OperatorRidgelet.TorusL2 d) :
  OperatorRidgelet.layerObservable (OperatorRidgelet.torusHaar d)
      (OperatorRidgelet.convDirection k) (OperatorRidgelet.convOutput ψ)
      β (OperatorRidgelet.torusOne d) x =
    OperatorRidgelet.torusFourierCoeff (fun t => ↑(↑↑ψ t)) 0 *
      ∫ (y : OperatorRidgelet.Torus d),
        ↑(β
            (inner ℝ (OperatorRidgelet.convDirection k y)
              x)) ∂OperatorRidgelet.torusHaar d

theorem OperatorRidgelet.Paper.ex_7_8_ix (d : ℕ)
  (k ψ : OperatorRidgelet.TorusL2 d)
  (β : ℝ → ℝ) (hβc : Continuous β)
  (hβp :
    OperatorRidgelet.HasPolynomialGrowth
      β)
  (x : OperatorRidgelet.TorusL2 d) :
  OperatorRidgelet.layerObservable
      (OperatorRidgelet.torusHaar d)
      (OperatorRidgelet.convDirection k)
      (OperatorRidgelet.convOutput ψ) β
      (OperatorRidgelet.torusOne d) x =
    OperatorRidgelet.torusFourierCoeff
        (fun t => ↑(↑↑ψ t)) 0 *
      ∫ (y : OperatorRidgelet.Torus d),
        ↑(β
            (inner ℝ
              (OperatorRidgelet.convDirection
                k y)
              x)) ∂OperatorRidgelet.torusHaar
          d

**Example [ex:7.8]** Periodic convolution layer.  With `φ ≡ 1` the observable is
`F_1(x) = ψ̂(0) ∫ β((k * x)(y)) dy`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_8_x (d : ℕ)
  (k ψ : OperatorRidgelet.TorusL2 d)
  (hk :
    {n |
        OperatorRidgelet.torusFourierCoeff (fun t => ↑(↑↑k t)) n ≠
          0}.Infinite)
  (hψ : OperatorRidgelet.torusFourierCoeff (fun t => ↑(↑↑ψ t)) 0 ≠ 0) :
  ¬OperatorRidgelet.IsCylindrical
      (OperatorRidgelet.layerObservable (OperatorRidgelet.torusHaar d)
        (OperatorRidgelet.convDirection k)
        (OperatorRidgelet.convOutput ψ) OperatorRidgelet.gaussianFun
        (OperatorRidgelet.torusOne d))

theorem OperatorRidgelet.Paper.ex_7_8_x (d : ℕ)
  (k ψ : OperatorRidgelet.TorusL2 d)
  (hk :
    {n |
        OperatorRidgelet.torusFourierCoeff
            (fun t => ↑(↑↑k t)) n ≠
          0}.Infinite)
  (hψ :
    OperatorRidgelet.torusFourierCoeff
        (fun t => ↑(↑↑ψ t)) 0 ≠
      0) :
  ¬OperatorRidgelet.IsCylindrical
      (OperatorRidgelet.layerObservable
        (OperatorRidgelet.torusHaar d)
        (OperatorRidgelet.convDirection k)
        (OperatorRidgelet.convOutput ψ)
        OperatorRidgelet.gaussianFun
        (OperatorRidgelet.torusOne d))

**Example [ex:7.8]** Periodic convolution layer.  If `k̂(n) ≠ 0` for infinitely many
`n` and `ψ̂(0) ≠ 0`, then the observable `F_1` of the Gaussian-activation layer is not
cylindrical.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_8_xi (d : ℕ) (s : ℝ) (hs : ↑d / 2 < s) :
  OperatorRidgelet.IsTraceClassCovariance
    (OperatorRidgelet.besselOperator d s)

theorem OperatorRidgelet.Paper.ex_7_8_xi (d : ℕ)
  (s : ℝ) (hs : ↑d / 2 < s) :
  OperatorRidgelet.IsTraceClassCovariance
    (OperatorRidgelet.besselOperator d s)

**Example [ex:7.8]** Periodic convolution layer.  For `s > d/2`, the operator
`(I - Δ)^{-s}` is injective, positive, self-adjoint, and trace class.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_8_xii (d : ℕ) (s : ℝ) (hs : ↑d / 2 < s)
  (z : OperatorRidgelet.Torus d) (x : OperatorRidgelet.TorusL2 d) :
  (OperatorRidgelet.besselOperator d s)
      ((OperatorRidgelet.torusTranslate d z) x) =
    (OperatorRidgelet.torusTranslate d z)
      ((OperatorRidgelet.besselOperator d s) x)

theorem OperatorRidgelet.Paper.ex_7_8_xii (d : ℕ)
  (s : ℝ) (hs : ↑d / 2 < s)
  (z : OperatorRidgelet.Torus d)
  (x : OperatorRidgelet.TorusL2 d) :
  (OperatorRidgelet.besselOperator d s)
      ((OperatorRidgelet.torusTranslate d
          z)
        x) =
    (OperatorRidgelet.torusTranslate d z)
      ((OperatorRidgelet.besselOperator d
          s)
        x)

**Example [ex:7.8]** Periodic convolution layer.  `(I - Δ)^{-s}` is translation
invariant: `(I - Δ)^{-s} τ_z = τ_z (I - Δ)^{-s}`.

theoremdefined in OperatorRidgelet/Paper/Examples.lean

complete

theorem OperatorRidgelet.Paper.ex_7_8_xiii (d : ℕ) (s : ℝ) (hs : ↑d / 2 < s)
  [MeasurableSpace (OperatorRidgelet.TorusL2 d)]
  [BorelSpace (OperatorRidgelet.TorusL2 d)]
  (μ : MeasureTheory.Measure (OperatorRidgelet.TorusL2 d))
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian
      (OperatorRidgelet.besselOperator d s) μ)
  (ρ : SchwartzMap ℝ ℝ) (f : OperatorRidgelet.TorusL2 d → ℂ)
  (hf : MeasureTheory.Integrable f μ) (z : OperatorRidgelet.Torus d)
  (p : OperatorRidgelet.TorusL2 d × ℝ) :
  OperatorRidgelet.ridgelet μ (⇑ρ)
      (fun x => f ((OperatorRidgelet.torusTranslate d z) x)) p =
    OperatorRidgelet.ridgelet μ (⇑ρ) f
      ((OperatorRidgelet.torusTranslate d z) p.1, p.2)

theorem OperatorRidgelet.Paper.ex_7_8_xiii (d : ℕ)
  (s : ℝ) (hs : ↑d / 2 < s)
  [MeasurableSpace
      (OperatorRidgelet.TorusL2 d)]
  [BorelSpace
      (OperatorRidgelet.TorusL2 d)]
  (μ :
    MeasureTheory.Measure
      (OperatorRidgelet.TorusL2 d))
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian
      (OperatorRidgelet.besselOperator d
        s)
      μ)
  (ρ : SchwartzMap ℝ ℝ)
  (f : OperatorRidgelet.TorusL2 d → ℂ)
  (hf : MeasureTheory.Integrable f μ)
  (z : OperatorRidgelet.Torus d)
  (p : OperatorRidgelet.TorusL2 d × ℝ) :
  OperatorRidgelet.ridgelet μ (⇑ρ)
      (fun x =>
        f
          ((OperatorRidgelet.torusTranslate
              d z)
            x))
      p =
    OperatorRidgelet.ridgelet μ (⇑ρ) f
      ((OperatorRidgelet.torusTranslate d
            z)
          p.1,
        p.2)

**Example [ex:7.8]** Periodic convolution layer.  With `Q = P = (I - Δ)^{-s}`,
`s > d/2`, the transform is equivariant: `R_ρ[f ∘ τ_z](a,c) = R_ρ f(τ_z a, c)` for every
translation `τ_z` and every `f ∈ L¹(μ_Q)`.

abbrevdefined in OperatorRidgelet/Examples/Defs.lean

complete

abbrev OperatorRidgelet.Torus (d : ℕ) : Type

abbrev OperatorRidgelet.Torus (d : ℕ) : Type

The torus `𝕋^d = (ℝ/2πℤ)^d`.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.torusHaar (d : ℕ) :
  MeasureTheory.Measure (OperatorRidgelet.Torus d)

def OperatorRidgelet.torusHaar (d : ℕ) :
  MeasureTheory.Measure
    (OperatorRidgelet.Torus d)

The normalized Haar (probability) measure on `𝕋^d`.

abbrevdefined in OperatorRidgelet/Examples/Defs.lean

complete

abbrev OperatorRidgelet.TorusL2 (d : ℕ) : Type

abbrev OperatorRidgelet.TorusL2 (d : ℕ) : Type

`L²(𝕋^d; ℝ)`, the input space of the convolution layer.

abbrevdefined in OperatorRidgelet/Examples/Defs.lean

complete

abbrev OperatorRidgelet.TorusL2C (d : ℕ) : Type

abbrev OperatorRidgelet.TorusL2C (d : ℕ) : Type

`L²(𝕋^d)`, the output space of the convolution layer.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.torusTranslate (d : ℕ) (z : OperatorRidgelet.Torus d) :
  OperatorRidgelet.TorusL2 d →ₗᵢ[ℝ] OperatorRidgelet.TorusL2 d

def OperatorRidgelet.torusTranslate (d : ℕ)
  (z : OperatorRidgelet.Torus d) :
  OperatorRidgelet.TorusL2 d →ₗᵢ[ℝ]
    OperatorRidgelet.TorusL2 d

The translation `(τ_z x)(t) = x(t - z)` on `L²(𝕋^d; ℝ)`, a linear isometry.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.torusTranslateC (d : ℕ)
  (z : OperatorRidgelet.Torus d) :
  OperatorRidgelet.TorusL2C d →ₗᵢ[ℂ] OperatorRidgelet.TorusL2C d

def OperatorRidgelet.torusTranslateC (d : ℕ)
  (z : OperatorRidgelet.Torus d) :
  OperatorRidgelet.TorusL2C d →ₗᵢ[ℂ]
    OperatorRidgelet.TorusL2C d

The translation `(τ_z u)(t) = u(t - z)` on `L²(𝕋^d)`, a linear isometry.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.convDirection {d : ℕ} (k : OperatorRidgelet.TorusL2 d)
  (y : OperatorRidgelet.Torus d) : OperatorRidgelet.TorusL2 d

def OperatorRidgelet.convDirection {d : ℕ}
  (k : OperatorRidgelet.TorusL2 d)
  (y : OperatorRidgelet.Torus d) :
  OperatorRidgelet.TorusL2 d

The direction `a_y = k(y - ·)` of the convolution layer.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.convOutput {d : ℕ} (ψ : OperatorRidgelet.TorusL2 d)
  (y : OperatorRidgelet.Torus d) : OperatorRidgelet.TorusL2C d

def OperatorRidgelet.convOutput {d : ℕ}
  (ψ : OperatorRidgelet.TorusL2 d)
  (y : OperatorRidgelet.Torus d) :
  OperatorRidgelet.TorusL2C d

The output `b_y = ψ(· - y)` of the convolution layer, as an element of `L²(𝕋^d)`.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.torusOne (d : ℕ) : OperatorRidgelet.TorusL2C d

def OperatorRidgelet.torusOne (d : ℕ) :
  OperatorRidgelet.TorusL2C d

The constant function `1` in `L²(𝕋^d)`.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.torusCharacter {d : ℕ} (n : Fin d → ℤ)
  (t : OperatorRidgelet.Torus d) : ℂ

def OperatorRidgelet.torusCharacter {d : ℕ}
  (n : Fin d → ℤ)
  (t : OperatorRidgelet.Torus d) : ℂ

The character `e_n(t) = e^{i⟨n,t⟩}` of `𝕋^d`, `n ∈ ℤ^d`.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.torusFourierCoeff {d : ℕ}
  (f : OperatorRidgelet.Torus d → ℂ) (n : Fin d → ℤ) : ℂ

def OperatorRidgelet.torusFourierCoeff {d : ℕ}
  (f : OperatorRidgelet.Torus d → ℂ)
  (n : Fin d → ℤ) : ℂ

The Fourier coefficient `f̂(n) = ∫ f(t) e^{-i⟨n,t⟩} dt` of a function on `𝕋^d` (normalized
Haar measure).

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.torusFreqNormSq {d : ℕ} (n : Fin d → ℤ) : ℝ

def OperatorRidgelet.torusFreqNormSq {d : ℕ}
  (n : Fin d → ℤ) : ℝ

`|n|² = ∑ n_j²` for a frequency `n ∈ ℤ^d`.

defdefined in OperatorRidgelet/Examples/Defs.lean

complete

def OperatorRidgelet.besselOperator (d : ℕ) (s : ℝ) :
  OperatorRidgelet.TorusL2 d →L[ℝ] OperatorRidgelet.TorusL2 d

def OperatorRidgelet.besselOperator (d : ℕ)
  (s : ℝ) :
  OperatorRidgelet.TorusL2 d →L[ℝ]
    OperatorRidgelet.TorusL2 d

The Bessel operator `(I - Δ)^{-s}` on `L²(𝕋^d; ℝ)`: the bounded operator that multiplies the
`n`-th Fourier coefficient by `(1 + |n|²)^{-s}` (chosen among the operators with this
property, which determines it; `0` if there is none).

Proof for Example 7.8

uses 1

With normalized Haar measure \|a_y\|=\|k\|_2 and \|b_y\|=\|\psi\|_2, convolutions commute with translations and with isometries fixing their kernels, \beta acts pointwise, A is diagonal in the Fourier basis with entries \widehat k(n), w_1=\widehat\psi(0) is a nonzero constant so Example 7.6 (iv) applies, and (I-\Delta)^{-s} has eigenvalues (1+|n|^2)^{-s}, summable for s>d/2.