Infinite-dimensional operator ridgelet transform

7.5. Dirichlet solution layers🔗

Example7.9
Statement uses 3
Statement dependency previews
Preview
Definition Aux.11
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

The interval \Omega=(0,1) with Lebesgue measure, H=Y=L^2(0,1), the Green kernel g(y,t)=\sinh(\min(y,t))\sinh(1-\max(y,t))/\sinh1, the layer data a_y=b_y=g(y,\cdot), the Dirichlet solution operator \mathsf G=(I-\partial_t^2)^{-1} as the integral operator with kernel g, its eigenvalues \lambda_n=(1+\pi^2n^2)^{-1} and eigenfunctions e_n(t)=\sqrt2\sin(n\pi t), and the 2N-neuron ReLU truncation \mathsf G_Nx=\sum_{n=1}^N\lambda_n[\operatorname{ReLU}(\langle e_n,x\rangle)-\operatorname{ReLU}(-\langle e_n,x\rangle)]e_n.

(\mathsf Gx)(y)=\int_0^1g(y,t)x(t)\,\mathrm dt (i) and u=\mathsf Gx solves -u''+u=x, u(0)=u(1)=0 (ii); \mathsf Ge_n=\lambda_ne_n (iii), so \mathsf G is an injective trace-class covariance (iv) of infinite rank (v), and \|A\|_\infty\le\sup_y\|g(y,\cdot)\|_2<\infty (vi). With a_y=b_y=g(y,\cdot) the neural-operator layer example applies (vii) and the layer is \mathcal F(x)=\mathsf G\,\beta(\mathsf Gx) (viii), one Picard step for the semilinear equation -u''+u=\beta(u)+x. The linear operator is an exact ReLU network, \mathsf Gx=\sum_n\lambda_ne_n[\operatorname{ReLU}(\langle e_n,x\rangle)-\operatorname{ReLU}(-\langle e_n,x\rangle)] (ix), whose 2N-neuron truncation has error at most \lambda_{N+1}\|x\| (x) with \lambda_{N+1}\le\pi^{-2}(N+1)^{-2} (xi).

Lean code for Example7.9●24 declarations
  • theoremdefined in OperatorRidgelet/Paper/Examples.lean
    complete
    theorem OperatorRidgelet.Paper.ex_7_9_i (x : OperatorRidgelet.UnitL2) :
  ↑↑(OperatorRidgelet.dirichletOperator x) =ᵐ[MeasureTheory.volume]
    fun y =>
    ∫ (t : OperatorRidgelet.UnitOpenInterval),
      OperatorRidgelet.dirichletKernel ↑y ↑t * ↑↑x t
    theorem OperatorRidgelet.Paper.ex_7_9_i
  (x : OperatorRidgelet.UnitL2) :
  ↑↑(OperatorRidgelet.dirichletOperator
          x) =ᵐ[MeasureTheory.volume]
    fun y =>
    ∫ (t :
      OperatorRidgelet.UnitOpenInterval),
      OperatorRidgelet.dirichletKernel ↑y
          ↑t *
        ↑↑x t
    **Example [ex:7.9]** Dirichlet solution operator with a pointwise nonlinearity.  `𝖦` is
the integral operator with kernel `g`: `(𝖦x)(y) = ∫₀¹ g(y,t) x(t) dt`.
  • theoremdefined in OperatorRidgelet/Paper/Examples.lean
    complete
    theorem OperatorRidgelet.Paper.ex_7_9_ii (x : ℝ → ℝ) (hx : Continuous x) :
  OperatorRidgelet.dirichletSolution x 0 = 0 ∧
    OperatorRidgelet.dirichletSolution x 1 = 0 ∧
      (∀ y ∈ Set.Ioo 0 1,
          DifferentiableAt ℝ (OperatorRidgelet.dirichletSolution x) y) ∧
        ∀ y ∈ Set.Ioo 0 1,
          HasDerivAt (deriv (OperatorRidgelet.dirichletSolution x))
            (OperatorRidgelet.dirichletSolution x y - x y) y
    theorem OperatorRidgelet.Paper.ex_7_9_ii
  (x : ℝ → ℝ) (hx : Continuous x) :
  OperatorRidgelet.dirichletSolution x 0 =
      0 ∧
    OperatorRidgelet.dirichletSolution x
          1 =
        0 ∧
      (∀ y ∈ Set.Ioo 0 1,
          DifferentiableAt ℝ
            (OperatorRidgelet.dirichletSolution
              x)
            y) ∧
        ∀ y ∈ Set.Ioo 0 1,
          HasDerivAt
            (deriv
              (OperatorRidgelet.dirichletSolution
                x))
            (OperatorRidgelet.dirichletSolution
                x y -
              x y)
            y
    **Example [ex:7.9]** Dirichlet solution operator with a pointwise nonlinearity.  For a
continuous source `x`, `u = 𝖦x` solves `-u'' + u = x` on `(0,1)` with `u(0) = u(1) = 0`.
  • theoremdefined in OperatorRidgelet/Paper/Examples.lean
    complete
    theorem OperatorRidgelet.Paper.ex_7_9_iii (n : ℕ) :
  1 ≤ n →
    OperatorRidgelet.dirichletOperator
        (OperatorRidgelet.dirichletEigenfunction n) =
      OperatorRidgelet.dirichletEigenvalue n •
        OperatorRidgelet.dirichletEigenfunction n
    theorem OperatorRidgelet.Paper.ex_7_9_iii
  (n : ℕ) :
  1 ≤ n →
    OperatorRidgelet.dirichletOperator
        (OperatorRidgelet.dirichletEigenfunction
          n) =
      OperatorRidgelet.dirichletEigenvalue
          n •
        OperatorRidgelet.dirichletEigenfunction
          n
    **Example [ex:7.9]** Dirichlet solution operator with a pointwise nonlinearity.  `𝖦` has
the eigenpairs `λ_n = (1 + π²n²)⁻¹`, `e_n(t) = √2 sin(nπt)`, `n ≥ 1`.
  • theoremdefined in OperatorRidgelet/Paper/Examples.lean
    complete
    theorem OperatorRidgelet.Paper.ex_7_9_iv :
  OperatorRidgelet.IsTraceClassCovariance
    OperatorRidgelet.dirichletOperator
    theorem OperatorRidgelet.Paper.ex_7_9_iv :
  OperatorRidgelet.IsTraceClassCovariance
    OperatorRidgelet.dirichletOperator
    **Example [ex:7.9]** Dirichlet solution operator with a pointwise nonlinearity.  `𝖦` is
injective, positive, self-adjoint, and trace class.
  • theoremdefined in OperatorRidgelet/Paper/Examples.lean
    complete
    theorem OperatorRidgelet.Paper.ex_7_9_v :
  OperatorRidgelet.HasInfiniteRank ↑OperatorRidgelet.dirichletOperator
    theorem OperatorRidgelet.Paper.ex_7_9_v :
  OperatorRidgelet.HasInfiniteRank
    ↑OperatorRidgelet.dirichletOperator
    **Example [ex:7.9]** Dirichlet solution operator with a pointwise nonlinearity.  `𝖦` has
infinite rank.
  • theoremdefined in OperatorRidgelet/Paper/Examples.lean
    complete
    theorem OperatorRidgelet.Paper.ex_7_9_vi :
  BddAbove (Set.range fun y => ‖OperatorRidgelet.dirichletDirection y‖)
    theorem OperatorRidgelet.Paper.ex_7_9_vi :
  BddAbove
    (Set.range fun y =>
      ‖OperatorRidgelet.dirichletDirection
          y‖)
    **Example [ex:7.9]** Dirichlet solution operator with a pointwise nonlinearity.
`‖A‖_∞ ≤ sup_y ‖g(y,·)‖₂ < ∞`: the directions `a_y = g(y,·)` are bounded in `L²(0,1)`.
  • theoremdefined in OperatorRidgelet/Paper/Examples.lean
    complete
    theorem OperatorRidgelet.Paper.ex_7_9_vii :
  OperatorRidgelet.IsLayerData MeasureTheory.volume
    OperatorRidgelet.dirichletDirection OperatorRidgelet.dirichletOutput
    theorem OperatorRidgelet.Paper.ex_7_9_vii :
  OperatorRidgelet.IsLayerData
    MeasureTheory.volume
    OperatorRidgelet.dirichletDirection
    OperatorRidgelet.dirichletOutput
    **Example [ex:7.9]** Dirichlet solution operator with a pointwise nonlinearity.  With
`a_y = b_y = g(y,·)` the standing hypotheses of the neural-operator layer hold, so Example
`ex:7.6` applies.
  • theoremdefined in OperatorRidgelet/Paper/Examples.lean
    complete
    theorem OperatorRidgelet.Paper.ex_7_9_viii (β : ℝ → ℝ) (hβc : Continuous β)
  (hβp : OperatorRidgelet.HasPolynomialGrowth β)
  (x : OperatorRidgelet.UnitL2) :
  OperatorRidgelet.operatorLayer MeasureTheory.volume
      OperatorRidgelet.dirichletDirection
      OperatorRidgelet.dirichletOutput β x =
    Complex.ofRealCLM.compLp
      (OperatorRidgelet.dirichletOperator
        (OperatorRidgelet.toLpOrZero 2 MeasureTheory.volume fun t =>
          β (↑↑(OperatorRidgelet.dirichletOperator x) t)))
    theorem OperatorRidgelet.Paper.ex_7_9_viii
  (β : ℝ → ℝ) (hβc : Continuous β)
  (hβp :
    OperatorRidgelet.HasPolynomialGrowth
      β)
  (x : OperatorRidgelet.UnitL2) :
  OperatorRidgelet.operatorLayer
      MeasureTheory.volume
      OperatorRidgelet.dirichletDirection
      OperatorRidgelet.dirichletOutput β
      x =
    Complex.ofRealCLM.compLp
      (OperatorRidgelet.dirichletOperator
        (OperatorRidgelet.toLpOrZero 2
          MeasureTheory.volume fun t =>
          β
            (↑↑(OperatorRidgelet.dirichletOperator
                    x)
              t)))
    **Example [ex:7.9]** Dirichlet solution operator with a pointwise nonlinearity.  With
`a_y = b_y = g(y,·)` the layer is `ℱ(x) = 𝖦 β(𝖦x)`.
  • theoremdefined in OperatorRidgelet/Paper/Examples.lean
    complete
    theorem OperatorRidgelet.Paper.ex_7_9_ix (x : OperatorRidgelet.UnitL2) :
  HasSum
    (fun n =>
      (OperatorRidgelet.dirichletEigenvalue n *
          (LeanRidgelet.relu
              (inner ℝ (OperatorRidgelet.dirichletEigenfunction n) x) -
            LeanRidgelet.relu
              (-inner ℝ (OperatorRidgelet.dirichletEigenfunction n)
                  x))) •
        OperatorRidgelet.dirichletEigenfunction n)
    (OperatorRidgelet.dirichletOperator x)
    theorem OperatorRidgelet.Paper.ex_7_9_ix
  (x : OperatorRidgelet.UnitL2) :
  HasSum
    (fun n =>
      (OperatorRidgelet.dirichletEigenvalue
            n *
          (LeanRidgelet.relu
              (inner ℝ
                (OperatorRidgelet.dirichletEigenfunction
                  n)
                x) -
            LeanRidgelet.relu
              (-inner ℝ
                  (OperatorRidgelet.dirichletEigenfunction
                    n)
                  x))) •
        OperatorRidgelet.dirichletEigenfunction
          n)
    (OperatorRidgelet.dirichletOperator x)
    **Example [ex:7.9]** Dirichlet solution operator with a pointwise nonlinearity.  `𝖦` is
the exact ReLU network `𝖦x = ∑_n λ_n e_n [ReLU(⟨e_n,x⟩) - ReLU(-⟨e_n,x⟩)]`.
  • theoremdefined in OperatorRidgelet/Paper/Examples.lean
    complete
    theorem OperatorRidgelet.Paper.ex_7_9_x (n : ℕ) (x : OperatorRidgelet.UnitL2) :
  ‖OperatorRidgelet.dirichletOperator x -
        OperatorRidgelet.dirichletReLUTruncation n x‖ ≤
    OperatorRidgelet.dirichletEigenvalue (n + 1) * ‖x‖
    theorem OperatorRidgelet.Paper.ex_7_9_x (n : ℕ)
  (x : OperatorRidgelet.UnitL2) :
  ‖OperatorRidgelet.dirichletOperator x -
        OperatorRidgelet.dirichletReLUTruncation
          n x‖ ≤
    OperatorRidgelet.dirichletEigenvalue
        (n + 1) *
      ‖x‖
    **Example [ex:7.9]** Dirichlet solution operator with a pointwise nonlinearity.  The
`2N`-neuron truncation has error `‖𝖦x - 𝖦_N x‖ ≤ λ_{N+1} ‖x‖`, uniformly on bounded sets.
  • theoremdefined in OperatorRidgelet/Paper/Examples.lean
    complete
    theorem OperatorRidgelet.Paper.ex_7_9_xi (n : ℕ) :
  OperatorRidgelet.dirichletEigenvalue (n + 1) ≤
    (Real.pi ^ 2 * (↑n + 1) ^ 2)⁻¹
    theorem OperatorRidgelet.Paper.ex_7_9_xi (n : ℕ) :
  OperatorRidgelet.dirichletEigenvalue
      (n + 1) ≤
    (Real.pi ^ 2 * (↑n + 1) ^ 2)⁻¹
    **Example [ex:7.9]** Dirichlet solution operator with a pointwise nonlinearity.  The
truncation error is `O(N^{-2})`: `λ_{N+1} ≤ π⁻² (N+1)⁻²`.
  • abbrevdefined in OperatorRidgelet/Examples/Defs.lean
    complete
    abbrev OperatorRidgelet.UnitOpenInterval : Type
    abbrev OperatorRidgelet.UnitOpenInterval : Type
    The open interval `(0,1)` as a measure space (Lebesgue measure).
  • abbrevdefined in OperatorRidgelet/Examples/Defs.lean
    complete
    abbrev OperatorRidgelet.UnitL2 : Type
    abbrev OperatorRidgelet.UnitL2 : Type
    `L²(0,1)`, real valued: the input space of the Dirichlet example.
  • abbrevdefined in OperatorRidgelet/Examples/Defs.lean
    complete
    abbrev OperatorRidgelet.UnitL2C : Type
    abbrev OperatorRidgelet.UnitL2C : Type
    `L²(0,1)`, complex valued: the output space of the Dirichlet example.
  • defdefined in OperatorRidgelet/Examples/Defs.lean
    complete
    def OperatorRidgelet.dirichletKernel (y t : ℝ) : ℝ
    def OperatorRidgelet.dirichletKernel
  (y t : ℝ) : ℝ
    The Green kernel `g(y,t) = sinh(min(y,t)) sinh(1 - max(y,t)) / sinh 1` of
`(I - ∂_t²)^{-1}` with Dirichlet boundary conditions.
  • defdefined in OperatorRidgelet/Examples/Defs.lean
    complete
    def OperatorRidgelet.dirichletKernelFn (y : ℝ) : OperatorRidgelet.UnitL2
    def OperatorRidgelet.dirichletKernelFn
  (y : ℝ) : OperatorRidgelet.UnitL2
    `g(y, ·)` as an element of `L²(0,1)`.
  • defdefined in OperatorRidgelet/Examples/Defs.lean
    complete
    def OperatorRidgelet.dirichletDirection
  (y : OperatorRidgelet.UnitOpenInterval) : OperatorRidgelet.UnitL2
    def OperatorRidgelet.dirichletDirection
  (y :
    OperatorRidgelet.UnitOpenInterval) :
  OperatorRidgelet.UnitL2
    The direction `a_y = g(y,·)` of the Dirichlet layer, `y ∈ (0,1)`.
  • defdefined in OperatorRidgelet/Examples/Defs.lean
    complete
    def OperatorRidgelet.dirichletOutput
  (y : OperatorRidgelet.UnitOpenInterval) : OperatorRidgelet.UnitL2C
    def OperatorRidgelet.dirichletOutput
  (y :
    OperatorRidgelet.UnitOpenInterval) :
  OperatorRidgelet.UnitL2C
    The output `b_y = g(y,·)` of the Dirichlet layer, as an element of `L²(0,1)` (complex).
  • defdefined in OperatorRidgelet/Examples/Defs.lean
    complete
    def OperatorRidgelet.dirichletSolution (x : ℝ → ℝ) (y : ℝ) : ℝ
    def OperatorRidgelet.dirichletSolution
  (x : ℝ → ℝ) (y : ℝ) : ℝ
    The solution `u(y) = ∫₀¹ g(y,t) x(t) dt` of `-u'' + u = x`, `u(0) = u(1) = 0`, for a
function `x`.
  • defdefined in OperatorRidgelet/Examples/Defs.lean
    complete
    def OperatorRidgelet.integralOperator.{u_1} {α : Type u_1}
  [MeasurableSpace α] (m : MeasureTheory.Measure α) (k : α → α → ℝ) :
  ↥(MeasureTheory.Lp ℝ 2 m) →L[ℝ] ↥(MeasureTheory.Lp ℝ 2 m)
    def OperatorRidgelet.integralOperator.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  (m : MeasureTheory.Measure α)
  (k : α → α → ℝ) :
  ↥(MeasureTheory.Lp ℝ 2 m) →L[ℝ]
    ↥(MeasureTheory.Lp ℝ 2 m)
    The integral operator on `L²(m)` with kernel `k`: the bounded operator `T` with
`(Tx)(y) = ∫ k(y,t) x(t) m(dt)` a.e. (which determines it; `0` if there is none).
  • defdefined in OperatorRidgelet/Examples/Defs.lean
    complete
    def OperatorRidgelet.dirichletOperator :
  OperatorRidgelet.UnitL2 →L[ℝ] OperatorRidgelet.UnitL2
    def OperatorRidgelet.dirichletOperator :
  OperatorRidgelet.UnitL2 →L[ℝ]
    OperatorRidgelet.UnitL2
    The Dirichlet solution operator `𝖦 = (I - ∂_t²)^{-1}` on `L²(0,1)`, the integral operator
with kernel `g`.
  • defdefined in OperatorRidgelet/Examples/Defs.lean
    complete
    def OperatorRidgelet.dirichletEigenvalue (n : ℕ) : ℝ
    def OperatorRidgelet.dirichletEigenvalue
  (n : ℕ) : ℝ
    The eigenvalues `λ_n = (1 + π²n²)⁻¹` of `𝖦`.
  • defdefined in OperatorRidgelet/Examples/Defs.lean
    complete
    def OperatorRidgelet.dirichletEigenfunction (n : ℕ) :
  OperatorRidgelet.UnitL2
    def OperatorRidgelet.dirichletEigenfunction
  (n : ℕ) : OperatorRidgelet.UnitL2
    The eigenfunctions `e_n(t) = √2 sin(nπt)` of `𝖦`, as elements of `L²(0,1)` (`e_0 = 0`).
  • defdefined in OperatorRidgelet/Examples/Defs.lean
    complete
    def OperatorRidgelet.dirichletReLUTruncation (N : ℕ)
  (x : OperatorRidgelet.UnitL2) : OperatorRidgelet.UnitL2
    def OperatorRidgelet.dirichletReLUTruncation
  (N : ℕ) (x : OperatorRidgelet.UnitL2) :
  OperatorRidgelet.UnitL2
    The `2N`-neuron ReLU truncation
`𝖦_N x = ∑_{n=1}^N λ_n [ReLU(⟨e_n,x⟩) - ReLU(-⟨e_n,x⟩)] e_n` of the exact ReLU network of
`𝖦`.
Proof for Example 7.9
uses 1

Direct differentiation shows that g(y,\cdot) solves the boundary value problem with a unit jump of the derivative at t=y, the eigenpairs are checked by -e_n''+e_n=(1+\pi^2n^2)e_n, the kernel is continuous and bounded so Example 7.6 applies, the ReLU expansion is the spectral theorem with u=\operatorname{ReLU}(u)-\operatorname{ReLU}(-u), and orthogonality gives \|\mathsf Gx-\mathsf G_Nx\|^2=\sum_{n>N}\lambda_n^2\langle e_n,x\rangle^2\le\lambda_{N+1}^2\|x\|^2.