5. Null space and the general solution🔗

Definition5.1

uses 0used by 0✓L∃∀N

Define the canonical orthogonal parameter projection by P=S_\sigma^\dagger\circ S_\sigma.

Lean code for Definition5.1●1 definition

defdefined in LeanRidgelet/Operator/Ridgelet.lean

complete

def LeanRidgelet.networkVisibleProjection (m : ℕ) [NeZero m] (s t : ℝ)
  (σ : ↥(LeanRidgelet.ActivationSpace s t)) :
  ↥(LeanRidgelet.ParameterSpace m s t) →L[ℂ]
    ↥(LeanRidgelet.ParameterSpace m s t)

def LeanRidgelet.networkVisibleProjection
  (m : ℕ) [NeZero m] (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t)) :
  ↥(LeanRidgelet.ParameterSpace m s
        t) →L[ℂ]
    ↥(LeanRidgelet.ParameterSpace m s t)

Implementation after :=

:=
  visibleProjection volume (activationFiberFunctional m s t σ)

The canonical orthogonal parameter projection `P = S^\dagger S`.

The name `networkVisibleProjection` is retained for API compatibility.

Theorem5.2

uses 0used by 0✓L∃∀N

If \sigma\ne0 then P^2=P=P^*.

Lean code for Theorem5.2●2 theorems

theoremdefined in LeanRidgelet/Operator/Ridgelet.lean

complete

theorem LeanRidgelet.isIdempotentElem_networkVisibleProjection (m : ℕ)
  [NeZero m] (s t : ℝ) {σ : ↥(LeanRidgelet.ActivationSpace s t)}
  (hσ : σ ≠ 0) :
  IsIdempotentElem (LeanRidgelet.networkVisibleProjection m s t σ)

theorem LeanRidgelet.isIdempotentElem_networkVisibleProjection
  (m : ℕ) [NeZero m] (s t : ℝ)
  {σ :
    ↥(LeanRidgelet.ActivationSpace s t)}
  (hσ : σ ≠ 0) :
  IsIdempotentElem
    (LeanRidgelet.networkVisibleProjection
      m s t σ)

theoremdefined in LeanRidgelet/Operator/Ridgelet.lean

complete

theorem LeanRidgelet.isSelfAdjoint_networkVisibleProjection (m : ℕ) [NeZero m]
  (s t : ℝ) (σ : ↥(LeanRidgelet.ActivationSpace s t)) :
  IsSelfAdjoint (LeanRidgelet.networkVisibleProjection m s t σ)

theorem LeanRidgelet.isSelfAdjoint_networkVisibleProjection
  (m : ℕ) [NeZero m] (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t)) :
  IsSelfAdjoint
    (LeanRidgelet.networkVisibleProjection
      m s t σ)

Theorem5.3

uses 0used by 0✓L∃∀N

The kernel and range of the canonical parameter projection are \ker P=\ker S_\sigma,\qquad\operatorname{ran}P=(\ker S_\sigma)^\perp.

Lean code for Theorem5.3●2 theorems

theoremdefined in LeanRidgelet/Operator/Ridgelet.lean

complete

theorem LeanRidgelet.ker_networkVisibleProjection (m : ℕ) [NeZero m] (s t : ℝ)
  {σ : ↥(LeanRidgelet.ActivationSpace s t)} (hσ : σ ≠ 0) :
  (↑(LeanRidgelet.networkVisibleProjection m s t σ)).ker =
    (↑(LeanRidgelet.networkSynthesis m s t σ)).ker

theorem LeanRidgelet.ker_networkVisibleProjection
  (m : ℕ) [NeZero m] (s t : ℝ)
  {σ :
    ↥(LeanRidgelet.ActivationSpace s t)}
  (hσ : σ ≠ 0) :
  (↑(LeanRidgelet.networkVisibleProjection
          m s t σ)).ker =
    (↑(LeanRidgelet.networkSynthesis m s t
          σ)).ker

theoremdefined in LeanRidgelet/Operator/Ridgelet.lean

complete

theorem LeanRidgelet.range_networkVisibleProjection (m : ℕ) [NeZero m] (s t : ℝ)
  {σ : ↥(LeanRidgelet.ActivationSpace s t)} (hσ : σ ≠ 0) :
  (↑(LeanRidgelet.networkVisibleProjection m s t σ)).range =
    (↑(LeanRidgelet.networkSynthesis m s t σ)).kerᗮ

theorem LeanRidgelet.range_networkVisibleProjection
  (m : ℕ) [NeZero m] (s t : ℝ)
  {σ :
    ↥(LeanRidgelet.ActivationSpace s t)}
  (hσ : σ ≠ 0) :
  (↑(LeanRidgelet.networkVisibleProjection
          m s t σ)).range =
    (↑(LeanRidgelet.networkSynthesis m s t
            σ)).kerᗮ

Theorem5.4

uses 0used by 1✓L∃∀N

A parameter \gamma belongs to the null space if and only if L_\sigma[T[\gamma](x,\cdot)]=0 for almost every x. In the current transported Lean model T=I. Equivalently, T[\ker S_\sigma]=L^2(\mathbb R^m;\ker L_\sigma).

Lean code for Theorem5.4●2 theorems

theoremdefined in LeanRidgelet/Operator/Ridgelet.lean

complete

theorem LeanRidgelet.mem_ker_networkSynthesis_iff (m : ℕ) [NeZero m] (s t : ℝ)
  (σ : ↥(LeanRidgelet.ActivationSpace s t))
  (γ : ↥(LeanRidgelet.ParameterSpace m s t)) :
  γ ∈ (↑(LeanRidgelet.networkSynthesis m s t σ)).ker ↔
    ∀ᵐ (x : LeanRidgelet.InputSpace m),
      (LeanRidgelet.activationFiberFunctional m s t σ) (↑↑γ x) = 0

theorem LeanRidgelet.mem_ker_networkSynthesis_iff
  (m : ℕ) [NeZero m] (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t))
  (γ :
    ↥(LeanRidgelet.ParameterSpace m s
        t)) :
  γ ∈
      (↑(LeanRidgelet.networkSynthesis m s
            t σ)).ker ↔
    ∀ᵐ (x : LeanRidgelet.InputSpace m),
      (LeanRidgelet.activationFiberFunctional
            m s t σ)
          (↑↑γ x) =
        0

Pointwise characterization of the null space in unitary coordinates.

theoremdefined in LeanRidgelet/Operator/Ridgelet.lean

complete

theorem LeanRidgelet.mem_ker_networkSynthesis_iff_fourierDilation (m : ℕ)
  [NeZero m] (s t : ℝ) (σ : ↥(LeanRidgelet.ActivationSpace s t))
  (γ : ↥(LeanRidgelet.ParameterSpace m s t)) :
  γ ∈ (↑(LeanRidgelet.networkSynthesis m s t σ)).ker ↔
    ∀ᵐ (x : LeanRidgelet.InputSpace m),
      (LeanRidgelet.activationFiberFunctional m s t σ)
          (↑↑((LeanRidgelet.fourierDilationTransform m s t) γ) x) =
        0

theorem LeanRidgelet.mem_ker_networkSynthesis_iff_fourierDilation
  (m : ℕ) [NeZero m] (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t))
  (γ :
    ↥(LeanRidgelet.ParameterSpace m s
        t)) :
  γ ∈
      (↑(LeanRidgelet.networkSynthesis m s
            t σ)).ker ↔
    ∀ᵐ (x : LeanRidgelet.InputSpace m),
      (LeanRidgelet.activationFiberFunctional
            m s t σ)
          (↑↑((LeanRidgelet.fourierDilationTransform
                    m s t)
                  γ)
            x) =
        0

The null-space characterization with the manuscript unitary coordinate transform explicit.

Theorem5.5

uses 0used by 1✓L∃∀N

Assume \sigma\ne0. The complete solution set of S_\sigma[\gamma]=f is S_\sigma^\dagger[f]+\ker S_\sigma.

Lean code for Theorem5.5●1 theorem

theoremdefined in LeanRidgelet/Operator/Ridgelet.lean

complete

theorem LeanRidgelet.networkSolution_iff_kernel_translate (m : ℕ) [NeZero m]
  (s t : ℝ) {σ : ↥(LeanRidgelet.ActivationSpace s t)} (hσ : σ ≠ 0)
  (f : ↥(LeanRidgelet.TargetSpace m))
  (γ : ↥(LeanRidgelet.ParameterSpace m s t)) :
  (LeanRidgelet.networkSynthesis m s t σ) γ = f ↔
    γ - (LeanRidgelet.normalizedNetworkRightInverse m s t σ) f ∈
      (↑(LeanRidgelet.networkSynthesis m s t σ)).ker

theorem LeanRidgelet.networkSolution_iff_kernel_translate
  (m : ℕ) [NeZero m] (s t : ℝ)
  {σ :
    ↥(LeanRidgelet.ActivationSpace s t)}
  (hσ : σ ≠ 0)
  (f : ↥(LeanRidgelet.TargetSpace m))
  (γ :
    ↥(LeanRidgelet.ParameterSpace m s
        t)) :
  (LeanRidgelet.networkSynthesis m s t σ)
        γ =
      f ↔
    γ -
        (LeanRidgelet.normalizedNetworkRightInverse
            m s t σ)
          f ∈
      (↑(LeanRidgelet.networkSynthesis m s
            t σ)).ker

Every solution is the normalized-adjoint solution plus a null component.

Theorem5.6

uses 0used by 1✓L∃∀N

S_\sigma^\dagger[f] is the unique minimum-norm solution of S_\sigma[\gamma]=f.

Lean code for Theorem5.6●1 theorem

theoremdefined in LeanRidgelet/Operator/Ridgelet.lean

complete

theorem LeanRidgelet.normalizedNetworkRightInverse_unique_minimal (m : ℕ)
  [NeZero m] (s t : ℝ) {σ : ↥(LeanRidgelet.ActivationSpace s t)}
  (hσ : σ ≠ 0) (f : ↥(LeanRidgelet.TargetSpace m))
  (γ : ↥(LeanRidgelet.ParameterSpace m s t)) :
  (LeanRidgelet.networkSynthesis m s t σ) γ = f →
    ‖(LeanRidgelet.normalizedNetworkRightInverse m s t σ) f‖ ≤ ‖γ‖ ∧
      (‖(LeanRidgelet.normalizedNetworkRightInverse m s t σ) f‖ = ‖γ‖ →
        (LeanRidgelet.normalizedNetworkRightInverse m s t σ) f = γ)

theorem LeanRidgelet.normalizedNetworkRightInverse_unique_minimal
  (m : ℕ) [NeZero m] (s t : ℝ)
  {σ :
    ↥(LeanRidgelet.ActivationSpace s t)}
  (hσ : σ ≠ 0)
  (f : ↥(LeanRidgelet.TargetSpace m))
  (γ :
    ↥(LeanRidgelet.ParameterSpace m s
        t)) :
  (LeanRidgelet.networkSynthesis m s t σ)
        γ =
      f →
    ‖(LeanRidgelet.normalizedNetworkRightInverse
              m s t σ)
            f‖ ≤
        ‖γ‖ ∧
      (‖(LeanRidgelet.normalizedNetworkRightInverse
                m s t σ)
              f‖ =
          ‖γ‖ →
        (LeanRidgelet.normalizedNetworkRightInverse
              m s t σ)
            f =
          γ)

The normalized-adjoint solution is the unique minimum-norm parameter solution.

Definition5.7

uses 0used by 0✓L∃∀N

For a Hilbert basis (e_i) of L^2(\mathbb R^m), define the coefficient vector h_i[\gamma] of a parameter by a Bochner integral.

Lean code for Definition5.7●1 definition

defdefined in LeanRidgelet/Operator/GeneralSolution.lean

complete

def LeanRidgelet.fiberCoefficient.{u_1, u_2} {α : Type u_1} {H : Type u_2}
  [MeasurableSpace α] (μ : MeasureTheory.Measure α)
  [NormedAddCommGroup H] [InnerProductSpace ℂ H]
  (e : ↥(LeanRidgelet.L2 α μ)) (γ : ↥(LeanRidgelet.BochnerL2 α H μ)) : H

def LeanRidgelet.fiberCoefficient.{u_1, u_2}
  {α : Type u_1} {H : Type u_2}
  [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  [NormedAddCommGroup H]
  [InnerProductSpace ℂ H]
  (e : ↥(LeanRidgelet.L2 α μ))
  (γ : ↥(LeanRidgelet.BochnerL2 α H μ)) :
  H

Implementation after :=

:=
  ∫ x, conj (e x) • γ x ∂μ

The `H`-valued coefficient vector `h_i[γ]` of `γ` along a scalar `L²` vector `e`.

Theorem5.8

uses 0used by 1✓L∃∀N

Every parameter distribution has the ridgelet-series expansion \gamma=\sum_i R_{h_i[\gamma]}[e_i].

Lean code for Theorem5.8●1 theorem

theoremdefined in LeanRidgelet/Operator/Ridgelet.lean

complete

theorem LeanRidgelet.hasSum_ridgeletOperator_fiberCoefficient.{u_1}
  {ι : Type u_1} (m : ℕ) [NeZero m] (s t : ℝ)
  (b : HilbertBasis ι ℂ ↥(LeanRidgelet.TargetSpace m))
  (γ : ↥(LeanRidgelet.ParameterSpace m s t)) :
  HasSum
    (fun i ↦
      (LeanRidgelet.ridgeletOperator m s t
          (LeanRidgelet.fiberCoefficient MeasureTheory.volume (b i) γ))
        (b i))
    γ

theorem LeanRidgelet.hasSum_ridgeletOperator_fiberCoefficient.{u_1}
  {ι : Type u_1} (m : ℕ) [NeZero m]
  (s t : ℝ)
  (b :
    HilbertBasis ι ℂ
      ↥(LeanRidgelet.TargetSpace m))
  (γ :
    ↥(LeanRidgelet.ParameterSpace m s
        t)) :
  HasSum
    (fun i ↦
      (LeanRidgelet.ridgeletOperator m s t
          (LeanRidgelet.fiberCoefficient
            MeasureTheory.volume (b i) γ))
        (b i))
    γ

The coefficient-vector series expansion of a parameter distribution.

Theorem5.9

uses 0used by 1✓L∃∀N

If \gamma\in\ker S_\sigma, then every coefficient vector h_i[\gamma] belongs to \ker L_\sigma.

Lean code for Theorem5.9●1 theorem

theoremdefined in LeanRidgelet/Operator/Ridgelet.lean

complete

theorem LeanRidgelet.activationFiberFunctional_fiberCoefficient_eq_zero_of_mem_ker.{u_1}
  {ι : Type u_1} (m : ℕ) [NeZero m] (s t : ℝ)
  (σ : ↥(LeanRidgelet.ActivationSpace s t))
  (b : HilbertBasis ι ℂ ↥(LeanRidgelet.TargetSpace m))
  (γ : ↥(LeanRidgelet.ParameterSpace m s t))
  (hγ : γ ∈ (↑(LeanRidgelet.networkSynthesis m s t σ)).ker) (i : ι) :
  (LeanRidgelet.activationFiberFunctional m s t σ)
      (LeanRidgelet.fiberCoefficient MeasureTheory.volume (b i) γ) =
    0

theorem LeanRidgelet.activationFiberFunctional_fiberCoefficient_eq_zero_of_mem_ker.{u_1}
  {ι : Type u_1} (m : ℕ) [NeZero m]
  (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t))
  (b :
    HilbertBasis ι ℂ
      ↥(LeanRidgelet.TargetSpace m))
  (γ :
    ↥(LeanRidgelet.ParameterSpace m s t))
  (hγ :
    γ ∈
      (↑(LeanRidgelet.networkSynthesis m s
            t σ)).ker)
  (i : ι) :
  (LeanRidgelet.activationFiberFunctional
        m s t σ)
      (LeanRidgelet.fiberCoefficient
        MeasureTheory.volume (b i) γ) =
    0

Every coefficient vector of a null parameter lies in the activation functional's kernel.

Theorem5.10

Statement uses 5

Statement dependency previews

Preview

Theorem 5.4

Loading preview

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

used by 0✓L∃∀N

Together, these results show that the null ridgelet series relative to a fixed Hilbert basis exists and is unique, and that every solution is the sum of the canonical particular solution and an arbitrary null series.

Lean code for Theorem5.10●4 theorems

theoremdefined in LeanRidgelet/Operator/Ridgelet.lean

complete

theorem LeanRidgelet.mem_ker_networkSynthesis_iff (m : ℕ) [NeZero m] (s t : ℝ)
  (σ : ↥(LeanRidgelet.ActivationSpace s t))
  (γ : ↥(LeanRidgelet.ParameterSpace m s t)) :
  γ ∈ (↑(LeanRidgelet.networkSynthesis m s t σ)).ker ↔
    ∀ᵐ (x : LeanRidgelet.InputSpace m),
      (LeanRidgelet.activationFiberFunctional m s t σ) (↑↑γ x) = 0

theorem LeanRidgelet.mem_ker_networkSynthesis_iff
  (m : ℕ) [NeZero m] (s t : ℝ)
  (σ :
    ↥(LeanRidgelet.ActivationSpace s t))
  (γ :
    ↥(LeanRidgelet.ParameterSpace m s
        t)) :
  γ ∈
      (↑(LeanRidgelet.networkSynthesis m s
            t σ)).ker ↔
    ∀ᵐ (x : LeanRidgelet.InputSpace m),
      (LeanRidgelet.activationFiberFunctional
            m s t σ)
          (↑↑γ x) =
        0

Pointwise characterization of the null space in unitary coordinates.

theoremdefined in LeanRidgelet/Operator/Ridgelet.lean

complete

theorem LeanRidgelet.hasSum_ridgeletOperator_fiberCoefficient.{u_1}
  {ι : Type u_1} (m : ℕ) [NeZero m] (s t : ℝ)
  (b : HilbertBasis ι ℂ ↥(LeanRidgelet.TargetSpace m))
  (γ : ↥(LeanRidgelet.ParameterSpace m s t)) :
  HasSum
    (fun i ↦
      (LeanRidgelet.ridgeletOperator m s t
          (LeanRidgelet.fiberCoefficient MeasureTheory.volume (b i) γ))
        (b i))
    γ

theorem LeanRidgelet.hasSum_ridgeletOperator_fiberCoefficient.{u_1}
  {ι : Type u_1} (m : ℕ) [NeZero m]
  (s t : ℝ)
  (b :
    HilbertBasis ι ℂ
      ↥(LeanRidgelet.TargetSpace m))
  (γ :
    ↥(LeanRidgelet.ParameterSpace m s
        t)) :
  HasSum
    (fun i ↦
      (LeanRidgelet.ridgeletOperator m s t
          (LeanRidgelet.fiberCoefficient
            MeasureTheory.volume (b i) γ))
        (b i))
    γ

The coefficient-vector series expansion of a parameter distribution.

theoremdefined in LeanRidgelet/Operator/Ridgelet.lean

complete

theorem LeanRidgelet.networkSolution_iff_kernel_translate (m : ℕ) [NeZero m]
  (s t : ℝ) {σ : ↥(LeanRidgelet.ActivationSpace s t)} (hσ : σ ≠ 0)
  (f : ↥(LeanRidgelet.TargetSpace m))
  (γ : ↥(LeanRidgelet.ParameterSpace m s t)) :
  (LeanRidgelet.networkSynthesis m s t σ) γ = f ↔
    γ - (LeanRidgelet.normalizedNetworkRightInverse m s t σ) f ∈
      (↑(LeanRidgelet.networkSynthesis m s t σ)).ker

theorem LeanRidgelet.networkSolution_iff_kernel_translate
  (m : ℕ) [NeZero m] (s t : ℝ)
  {σ :
    ↥(LeanRidgelet.ActivationSpace s t)}
  (hσ : σ ≠ 0)
  (f : ↥(LeanRidgelet.TargetSpace m))
  (γ :
    ↥(LeanRidgelet.ParameterSpace m s
        t)) :
  (LeanRidgelet.networkSynthesis m s t σ)
        γ =
      f ↔
    γ -
        (LeanRidgelet.normalizedNetworkRightInverse
            m s t σ)
          f ∈
      (↑(LeanRidgelet.networkSynthesis m s
            t σ)).ker

Every solution is the normalized-adjoint solution plus a null component.

theoremdefined in LeanRidgelet/Operator/Ridgelet.lean

complete

theorem LeanRidgelet.normalizedNetworkRightInverse_unique_minimal (m : ℕ)
  [NeZero m] (s t : ℝ) {σ : ↥(LeanRidgelet.ActivationSpace s t)}
  (hσ : σ ≠ 0) (f : ↥(LeanRidgelet.TargetSpace m))
  (γ : ↥(LeanRidgelet.ParameterSpace m s t)) :
  (LeanRidgelet.networkSynthesis m s t σ) γ = f →
    ‖(LeanRidgelet.normalizedNetworkRightInverse m s t σ) f‖ ≤ ‖γ‖ ∧
      (‖(LeanRidgelet.normalizedNetworkRightInverse m s t σ) f‖ = ‖γ‖ →
        (LeanRidgelet.normalizedNetworkRightInverse m s t σ) f = γ)

theorem LeanRidgelet.normalizedNetworkRightInverse_unique_minimal
  (m : ℕ) [NeZero m] (s t : ℝ)
  {σ :
    ↥(LeanRidgelet.ActivationSpace s t)}
  (hσ : σ ≠ 0)
  (f : ↥(LeanRidgelet.TargetSpace m))
  (γ :
    ↥(LeanRidgelet.ParameterSpace m s
        t)) :
  (LeanRidgelet.networkSynthesis m s t σ)
        γ =
      f →
    ‖(LeanRidgelet.normalizedNetworkRightInverse
              m s t σ)
            f‖ ≤
        ‖γ‖ ∧
      (‖(LeanRidgelet.normalizedNetworkRightInverse
                m s t σ)
              f‖ =
          ‖γ‖ →
        (LeanRidgelet.normalizedNetworkRightInverse
              m s t σ)
            f =
          γ)

The normalized-adjoint solution is the unique minimum-norm parameter solution.