4.1. Regularized synthesis🔗

Definition4.1.1

uses 1

Used by 3

Reverse dependency previews

Preview

Definition 4.1.2

Loading preview

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

✓L∃∀N

A tempered distribution \beta\in\mathcal S'(\mathbb R) is a polynomial, equivalently \beta=0 in \mathcal S'/\mathcal P, when it acts by integration against some polynomial. The Schwartz function with prescribed values is obtained by choice when one exists. The standard activations \tanh, the Gaussian distribution function \Phi, and the Gaussian e^{-u^2/2} are realized as tempered distributions acting by integration against the function; ReLU is treated in Corollary 4.1.4.

Lean code for Definition4.1.1●5 definitions

defdefined in OperatorRidgelet/Tempered/Defs.lean

complete

def OperatorRidgelet.IsPolynomialDistribution
  (β : TemperedDistribution ℝ ℂ) : Prop

def OperatorRidgelet.IsPolynomialDistribution
  (β : TemperedDistribution ℝ ℂ) : Prop

`β ∈ 𝒮'(ℝ)` is a polynomial (`β = 0` in `𝒮'/𝒫`): it acts by integration against the
evaluation of some `p : ℂ[X]`.

defdefined in OperatorRidgelet/Tempered/Defs.lean

complete

def OperatorRidgelet.schwartzOfFun (f : ℝ → ℂ) : SchwartzMap ℝ ℂ

def OperatorRidgelet.schwartzOfFun
  (f : ℝ → ℂ) : SchwartzMap ℝ ℂ

The Schwartz function with the values `f`, when one exists; `0` otherwise.

defdefined in OperatorRidgelet/Tempered/Defs.lean

complete

def OperatorRidgelet.tanhDistribution : TemperedDistribution ℝ ℂ

def OperatorRidgelet.tanhDistribution :
  TemperedDistribution ℝ ℂ

`tanh ∈ 𝒮'(ℝ)`, the vendored realization `tanhTemperedDistribution` (weight exponent
`t = 2`), which acts by integration against `tanh`.

defdefined in OperatorRidgelet/Tempered/Defs.lean

complete

def OperatorRidgelet.gaussianCdfDistribution : TemperedDistribution ℝ ℂ

def OperatorRidgelet.gaussianCdfDistribution :
  TemperedDistribution ℝ ℂ

`Φ ∈ 𝒮'(ℝ)`, the weighted realization of the Gaussian distribution function.

defdefined in OperatorRidgelet/Tempered/Defs.lean

complete

def OperatorRidgelet.gaussianDistribution : TemperedDistribution ℝ ℂ

def OperatorRidgelet.gaussianDistribution :
  TemperedDistribution ℝ ℂ

`e^{-u²/2} ∈ 𝒮'(ℝ)`, the weighted realization of the Gaussian activation.

Definition4.1.2

Statement uses 5

Statement dependency previews

Preview

Definition 2.2.1

Loading preview

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

used by 1✓L∃∀N

Let \beta\in\mathcal S'(\mathbb R) be real, that is, fixed by distributional conjugation, and let \rho be a band-pass filter. Choose an even \chi\in C_c^\infty(\mathbb R\setminus\{0\}) equal to one on a neighbourhood of \operatorname{supp}\widehat\rho (i) and an even, compactly supported, smooth approximate identity (\eta_\varepsilon)_{\varepsilon>0} (ii), and define the real Schwartz functions \beta_\varepsilon by \widehat{\beta_\varepsilon}=\chi\,(\widehat\beta*\eta_\varepsilon)\in C_c^\infty(\mathbb R\setminus\{0\}) (iii–v: membership, existence, and uniqueness of \beta_\varepsilon). For \gamma\in\operatorname{Ran}R_\rho, the regularized synthesis is S_{\beta_\varepsilon}\gamma=R_{\beta_\varepsilon}'\gamma\in\mathcal E_\alpha' (vi), and the synthesis with \beta is S_\beta\gamma=\lim_{\varepsilon\downarrow0}S_{\beta_\varepsilon}\gamma in \mathcal E_\alpha', whenever the limit exists.

Lean code for Definition4.1.2●14 declarations

defdefined in OperatorRidgelet/Tempered/Defs.lean

complete

def OperatorRidgelet.IsRealDistribution (β : TemperedDistribution ℝ ℂ) :
  Prop

def OperatorRidgelet.IsRealDistribution
  (β : TemperedDistribution ℝ ℂ) : Prop

`β ∈ 𝒮'(ℝ)` is real: it is fixed by the distributional conjugation
`conj u [φ] = conj (u [conj φ])`; equivalently, `β` pairs real test functions to real numbers.

structure(5 fields)defined in OperatorRidgelet/Tempered/Defs.lean

complete

structure OperatorRidgelet.IsCutoff (ρ : SchwartzMap ℝ ℝ) (χ : ℝ → ℝ) : Prop

structure OperatorRidgelet.IsCutoff
  (ρ : SchwartzMap ℝ ℝ) (χ : ℝ → ℝ) : Prop

An even `χ ∈ C_c^∞(ℝ ∖ {0})` equal to one on a neighbourhood of `supp ρ̂`.

Fields

contDiff : ContDiff ℝ (↑⊤) χ

`χ` is smooth.

hasCompactSupport : HasCompactSupport χ

`χ` has compact support.

zero_notMem_tsupport : 0 ∉ tsupport χ

The support of `χ` stays away from the origin.

even : ∀ (ω : ℝ), χ (-ω) = χ ω

`χ` is even.

eventuallyEq_one : ∀ᶠ (ω : ℝ) in nhdsSet (tsupport (OperatorRidgelet.filterFourier ⇑ρ)), χ ω = 1

`χ = 1` on a neighbourhood of `supp ρ̂`.

structure(6 fields)defined in OperatorRidgelet/Tempered/Defs.lean

complete

structure OperatorRidgelet.IsApproximateIdentity (η : ℝ → ℝ → ℝ) : Prop

structure OperatorRidgelet.IsApproximateIdentity
  (η : ℝ → ℝ → ℝ) : Prop

An even, compactly supported, smooth approximate identity `(η_ε)_{ε>0}`: for every `ε > 0`
the function `η_ε` is smooth, compactly supported, even, nonnegative, with integral one, and the
supports shrink to `{0}` as `ε ↓ 0`.  (The values of `η` at `ε ≤ 0` are irrelevant.)

Fields

contDiff : ∀ (ε : ℝ), 0 < ε → ContDiff ℝ (↑⊤) (η ε)

Each `η_ε` is smooth.

hasCompactSupport : ∀ (ε : ℝ), 0 < ε → HasCompactSupport (η ε)

Each `η_ε` has compact support.

even : ∀ (ε : ℝ), 0 < ε → ∀ (x : ℝ), η ε (-x) = η ε x

Each `η_ε` is even.

nonneg : ∀ (ε : ℝ), 0 < ε → ∀ (x : ℝ), 0 ≤ η ε x

Each `η_ε` is nonnegative.

integral_eq_one : ∀ (ε : ℝ), 0 < ε → ∫ (x : ℝ), η ε x = 1

Each `η_ε` has integral one.

tendsto_tsupport : Filter.Tendsto (fun ε => tsupport (η ε)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0).smallSets

The supports of `η_ε` shrink to `{0}` as `ε ↓ 0`.

defdefined in OperatorRidgelet/Tempered/Defs.lean

complete

def OperatorRidgelet.distributionConvolution (u : TemperedDistribution ℝ ℂ)
  (η : ℝ → ℝ) (ω : ℝ) : ℂ

def OperatorRidgelet.distributionConvolution
  (u : TemperedDistribution ℝ ℂ)
  (η : ℝ → ℝ) (ω : ℝ) : ℂ

The convolution `(u * η)(ω) = ⟨u, η(ω - ·)⟩` of a tempered distribution `u` with a test
function `η` (smooth and compactly supported in the applications).

defdefined in OperatorRidgelet/Tempered/Defs.lean

complete

def OperatorRidgelet.regularizedSpectrum (β : TemperedDistribution ℝ ℂ)
  (χ : ℝ → ℝ) (η : ℝ → ℝ → ℝ) (ε ω : ℝ) : ℂ

def OperatorRidgelet.regularizedSpectrum
  (β : TemperedDistribution ℝ ℂ)
  (χ : ℝ → ℝ) (η : ℝ → ℝ → ℝ) (ε ω : ℝ) :
  ℂ

The regularized spectrum `β̂_ε = χ (β̂ * η_ε)` of a tempered activation `β`.

defdefined in OperatorRidgelet/Tempered/Defs.lean

complete

def OperatorRidgelet.regularizedActivation (β : TemperedDistribution ℝ ℂ)
  (χ : ℝ → ℝ) (η : ℝ → ℝ → ℝ) (ε : ℝ) : SchwartzMap ℝ ℝ

def OperatorRidgelet.regularizedActivation
  (β : TemperedDistribution ℝ ℂ)
  (χ : ℝ → ℝ) (η : ℝ → ℝ → ℝ) (ε : ℝ) :
  SchwartzMap ℝ ℝ

The regularized activation `β_ε`: the real Schwartz function with `β̂_ε = χ (β̂ * η_ε)`
(unique by Fourier injectivity), and `0` if there is none.

defdefined in OperatorRidgelet/Tempered/Defs.lean

complete

def OperatorRidgelet.regularizedSynthesis.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [OpensMeasurableSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ] (β : TemperedDistribution ℝ ℂ)
  (χ : ℝ → ℝ) (η : ℝ → ℝ → ℝ) (ε : ℝ)
  (γ : ↥(MeasureTheory.Lp ℂ 2 (OperatorRidgelet.parameterMeasure ν))) :
  OperatorRidgelet.SpectralAntiDual μ ν

def OperatorRidgelet.regularizedSynthesis.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  [OpensMeasurableSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ]
  (β : TemperedDistribution ℝ ℂ)
  (χ : ℝ → ℝ) (η : ℝ → ℝ → ℝ) (ε : ℝ)
  (γ :
    ↥(MeasureTheory.Lp ℂ 2
        (OperatorRidgelet.parameterMeasure
          ν))) :
  OperatorRidgelet.SpectralAntiDual μ ν

The regularized synthesis `S_{β_ε} γ := R'_{β_ε} γ ∈ 𝓔_α'`, the synthesis operator
`synthesis` of Section 4 with the regularized activation `β_ε` as filter.

defdefined in OperatorRidgelet/Tempered/Defs.lean

complete

def OperatorRidgelet.temperedSynthesis.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [OpensMeasurableSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ] (β : TemperedDistribution ℝ ℂ)
  (χ : ℝ → ℝ) (η : ℝ → ℝ → ℝ)
  (γ : ↥(MeasureTheory.Lp ℂ 2 (OperatorRidgelet.parameterMeasure ν))) :
  OperatorRidgelet.SpectralAntiDual μ ν

def OperatorRidgelet.temperedSynthesis.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H]
  [OpensMeasurableSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsFiniteMeasure μ]
  (β : TemperedDistribution ℝ ℂ)
  (χ : ℝ → ℝ) (η : ℝ → ℝ → ℝ)
  (γ :
    ↥(MeasureTheory.Lp ℂ 2
        (OperatorRidgelet.parameterMeasure
          ν))) :
  OperatorRidgelet.SpectralAntiDual μ ν

The synthesis with the tempered activation `β`, `S_β γ := lim_{ε ↓ 0} S_{β_ε} γ` in
`𝓔_α'`, whenever the limit exists (and `0` otherwise).

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.def_regularized_synthesis_i (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) :
  ∃ χ, OperatorRidgelet.IsCutoff ρ χ

theorem OperatorRidgelet.Paper.def_regularized_synthesis_i
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) :
  ∃ χ, OperatorRidgelet.IsCutoff ρ χ

**Definition [def:regularized-synthesis]** Regularized synthesis.  For a band-pass `ρ` there
is an even `χ ∈ C_c^∞(ℝ ∖ {0})` equal to one on a neighbourhood of `supp ρ̂`.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.def_regularized_synthesis_ii :
  ∃ η, OperatorRidgelet.IsApproximateIdentity η

theorem OperatorRidgelet.Paper.def_regularized_synthesis_ii :
  ∃ η,
    OperatorRidgelet.IsApproximateIdentity
      η

**Definition [def:regularized-synthesis]** Regularized synthesis.  There is an even,
compactly supported, smooth approximate identity `(η_ε)_{ε>0}`.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.def_regularized_synthesis_iii
  (β : TemperedDistribution ℝ ℂ)
  (hβ : OperatorRidgelet.IsRealDistribution β) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (χ : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ) (η : ℝ → ℝ → ℝ)
  (hη : OperatorRidgelet.IsApproximateIdentity η) (ε : ℝ) (hε : 0 < ε) :
  ContDiff ℝ (↑⊤) (OperatorRidgelet.regularizedSpectrum β χ η ε) ∧
    HasCompactSupport (OperatorRidgelet.regularizedSpectrum β χ η ε) ∧
      0 ∉ tsupport (OperatorRidgelet.regularizedSpectrum β χ η ε)

theorem OperatorRidgelet.Paper.def_regularized_synthesis_iii
  (β : TemperedDistribution ℝ ℂ)
  (hβ :
    OperatorRidgelet.IsRealDistribution β)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (χ : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ)
  (η : ℝ → ℝ → ℝ)
  (hη :
    OperatorRidgelet.IsApproximateIdentity
      η)
  (ε : ℝ) (hε : 0 < ε) :
  ContDiff ℝ (↑⊤)
      (OperatorRidgelet.regularizedSpectrum
        β χ η ε) ∧
    HasCompactSupport
        (OperatorRidgelet.regularizedSpectrum
          β χ η ε) ∧
      0 ∉
        tsupport
          (OperatorRidgelet.regularizedSpectrum
            β χ η ε)

**Definition [def:regularized-synthesis]** Regularized synthesis.  For real `β`, band-pass
`ρ`, a cutoff `χ`, and an approximate identity `(η_ε)`, the regularized spectrum
`β̂_ε = χ (β̂ * η_ε)` belongs to `C_c^∞(ℝ ∖ {0})` for every `ε > 0`.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.def_regularized_synthesis_iv
  (β : TemperedDistribution ℝ ℂ)
  (hβ : OperatorRidgelet.IsRealDistribution β) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (χ : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ) (η : ℝ → ℝ → ℝ)
  (hη : OperatorRidgelet.IsApproximateIdentity η) (ε : ℝ) (hε : 0 < ε)
  (ω : ℝ) :
  OperatorRidgelet.filterFourier
      (⇑(OperatorRidgelet.regularizedActivation β χ η ε)) ω =
    OperatorRidgelet.regularizedSpectrum β χ η ε ω

theorem OperatorRidgelet.Paper.def_regularized_synthesis_iv
  (β : TemperedDistribution ℝ ℂ)
  (hβ :
    OperatorRidgelet.IsRealDistribution β)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (χ : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ)
  (η : ℝ → ℝ → ℝ)
  (hη :
    OperatorRidgelet.IsApproximateIdentity
      η)
  (ε : ℝ) (hε : 0 < ε) (ω : ℝ) :
  OperatorRidgelet.filterFourier
      (⇑(OperatorRidgelet.regularizedActivation
          β χ η ε))
      ω =
    OperatorRidgelet.regularizedSpectrum β
      χ η ε ω

**Definition [def:regularized-synthesis]** Regularized synthesis.  There is a real Schwartz
function `β_ε` with `β̂_ε = χ (β̂ * η_ε)`: the chosen `regularizedActivation` has this Fourier
transform.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.def_regularized_synthesis_v
  (β : TemperedDistribution ℝ ℂ)
  (hβ : OperatorRidgelet.IsRealDistribution β) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (χ : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ) (η : ℝ → ℝ → ℝ)
  (hη : OperatorRidgelet.IsApproximateIdentity η) (ε : ℝ) (hε : 0 < ε)
  (b : SchwartzMap ℝ ℝ) :
  (∀ (ω : ℝ),
      OperatorRidgelet.filterFourier (⇑b) ω =
        OperatorRidgelet.regularizedSpectrum β χ η ε ω) →
    b = OperatorRidgelet.regularizedActivation β χ η ε

theorem OperatorRidgelet.Paper.def_regularized_synthesis_v
  (β : TemperedDistribution ℝ ℂ)
  (hβ :
    OperatorRidgelet.IsRealDistribution β)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (χ : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ)
  (η : ℝ → ℝ → ℝ)
  (hη :
    OperatorRidgelet.IsApproximateIdentity
      η)
  (ε : ℝ) (hε : 0 < ε)
  (b : SchwartzMap ℝ ℝ) :
  (∀ (ω : ℝ),
      OperatorRidgelet.filterFourier (⇑b)
          ω =
        OperatorRidgelet.regularizedSpectrum
          β χ η ε ω) →
    b =
      OperatorRidgelet.regularizedActivation
        β χ η ε

**Definition [def:regularized-synthesis]** Regularized synthesis.  The real Schwartz function
`β_ε` with `β̂_ε = χ (β̂ * η_ε)` is unique.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.def_regularized_synthesis_vi.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
  (hν : OperatorRidgelet.IsHomogeneous α ν)
  (β : TemperedDistribution ℝ ℂ)
  (hβ : OperatorRidgelet.IsRealDistribution β) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (χ : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ) (η : ℝ → ℝ → ℝ)
  (hη : OperatorRidgelet.IsApproximateIdentity η) (ε : ℝ) (hε : 0 < ε)
  (γ : ↥(MeasureTheory.Lp ℂ 2 (OperatorRidgelet.parameterMeasure ν)))
  (hγ : γ ∈ OperatorRidgelet.ridgeletRange μ ν ⇑ρ)
  (g : ↥(OperatorRidgelet.spectralRange μ ν)) :
  (OperatorRidgelet.regularizedSynthesis μ ν β χ η ε γ) g =
    inner ℂ
      ((OperatorRidgelet.ridgeletExtension μ ν
          ⇑(OperatorRidgelet.regularizedActivation β χ η ε))
        g)
      γ

theorem OperatorRidgelet.Paper.def_regularized_synthesis_vi.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (β : TemperedDistribution ℝ ℂ)
  (hβ :
    OperatorRidgelet.IsRealDistribution β)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (χ : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ)
  (η : ℝ → ℝ → ℝ)
  (hη :
    OperatorRidgelet.IsApproximateIdentity
      η)
  (ε : ℝ) (hε : 0 < ε)
  (γ :
    ↥(MeasureTheory.Lp ℂ 2
        (OperatorRidgelet.parameterMeasure
          ν)))
  (hγ :
    γ ∈
      OperatorRidgelet.ridgeletRange μ ν
        ⇑ρ)
  (g :
    ↥(OperatorRidgelet.spectralRange μ
        ν)) :
  (OperatorRidgelet.regularizedSynthesis μ
        ν β χ η ε γ)
      g =
    inner ℂ
      ((OperatorRidgelet.ridgeletExtension
          μ ν
          ⇑(OperatorRidgelet.regularizedActivation
              β χ η ε))
        g)
      γ

**Definition [def:regularized-synthesis]** Regularized synthesis.  For `γ ∈ Ran R_ρ` the
regularized synthesis `S_{β_ε} γ = R'_{β_ε} γ` is a well-defined element of `𝓔_α'`: it is the
continuous anti-linear functional `g ↦ ⟨γ, R_{β_ε} g⟩_{L²(λ)}` (in the representation of
`OperatorRidgelet.Reconstruction.Defs`, where `S_ρ` is the transpose of the bounded extension
`R_ρ`, this holds by definition).

Theorem4.1.3

Statement uses 5

Statement dependency previews

Preview

Theorem 2.4.2

Loading preview

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

Used by 3

Reverse dependency previews

Preview

Corollary 4.1.4

Loading preview

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

✓L∃∀N

Let \beta\in\mathcal S'(\mathbb R) be real and let \rho be a band-pass filter. For every f\in\mathcal E_\alpha the limit defining S_\beta R_\rho f exists (i), does not depend on \chi or (\eta_\varepsilon) (ii), and S_\beta R_\rho f=C_{\beta,\rho}^{(\alpha)}T_\alpha f (iii). If C_{\beta,\rho}^{(\alpha)}\ne0, then f=(C_{\beta,\rho}^{(\alpha)})^{-1}T_\alpha^{-1}S_\beta R_\rho f for f\in\mathcal E_\alpha (iv) and g=(C_{\beta,\rho}^{(\alpha)})^{-1}S_\beta(R_\rho T_\alpha^{-1}g) for g\in\mathcal E_\alpha' (v). If \beta is not a polynomial, then a band-pass \rho with C_{\beta,\rho}^{(\alpha)}\ne0 exists (vi).

Lean code for Theorem4.1.3●6 theorems

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.thm_tempered_reconstruction_i.{u_1}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
  (hν : OperatorRidgelet.IsHomogeneous α ν)
  (β : TemperedDistribution ℝ ℂ)
  (hβ : OperatorRidgelet.IsRealDistribution β) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (χ : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ) (η : ℝ → ℝ → ℝ)
  (hη : OperatorRidgelet.IsApproximateIdentity η)
  (f : ↥(OperatorRidgelet.spectralRange μ ν)) :
  ∃ F,
    Filter.Tendsto
      (fun ε =>
        OperatorRidgelet.regularizedSynthesis μ ν β χ η ε
          ((OperatorRidgelet.ridgeletExtension μ ν ⇑ρ) f))
      (nhdsWithin 0 (Set.Ioi 0)) (nhds F)

theorem OperatorRidgelet.Paper.thm_tempered_reconstruction_i.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (β : TemperedDistribution ℝ ℂ)
  (hβ :
    OperatorRidgelet.IsRealDistribution β)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (χ : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ)
  (η : ℝ → ℝ → ℝ)
  (hη :
    OperatorRidgelet.IsApproximateIdentity
      η)
  (f :
    ↥(OperatorRidgelet.spectralRange μ
        ν)) :
  ∃ F,
    Filter.Tendsto
      (fun ε =>
        OperatorRidgelet.regularizedSynthesis
          μ ν β χ η ε
          ((OperatorRidgelet.ridgeletExtension
              μ ν ⇑ρ)
            f))
      (nhdsWithin 0 (Set.Ioi 0)) (nhds F)

**Theorem [thm:tempered-reconstruction]** Reconstruction with a tempered activation.  For
every `f ∈ 𝓔_α` the limit `S_β R_ρ f = lim_{ε ↓ 0} S_{β_ε} R_ρ f` exists in `𝓔_α'`.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.thm_tempered_reconstruction_ii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
  (hν : OperatorRidgelet.IsHomogeneous α ν)
  (β : TemperedDistribution ℝ ℂ)
  (hβ : OperatorRidgelet.IsRealDistribution β) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (χ χ' : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ)
  (hχ' : OperatorRidgelet.IsCutoff ρ χ') (η η' : ℝ → ℝ → ℝ)
  (hη : OperatorRidgelet.IsApproximateIdentity η)
  (hη' : OperatorRidgelet.IsApproximateIdentity η')
  (f : ↥(OperatorRidgelet.spectralRange μ ν)) :
  OperatorRidgelet.temperedSynthesis μ ν β χ η
      ((OperatorRidgelet.ridgeletExtension μ ν ⇑ρ) f) =
    OperatorRidgelet.temperedSynthesis μ ν β χ' η'
      ((OperatorRidgelet.ridgeletExtension μ ν ⇑ρ) f)

theorem OperatorRidgelet.Paper.thm_tempered_reconstruction_ii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (β : TemperedDistribution ℝ ℂ)
  (hβ :
    OperatorRidgelet.IsRealDistribution β)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (χ χ' : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ)
  (hχ' : OperatorRidgelet.IsCutoff ρ χ')
  (η η' : ℝ → ℝ → ℝ)
  (hη :
    OperatorRidgelet.IsApproximateIdentity
      η)
  (hη' :
    OperatorRidgelet.IsApproximateIdentity
      η')
  (f :
    ↥(OperatorRidgelet.spectralRange μ
        ν)) :
  OperatorRidgelet.temperedSynthesis μ ν β
      χ η
      ((OperatorRidgelet.ridgeletExtension
          μ ν ⇑ρ)
        f) =
    OperatorRidgelet.temperedSynthesis μ ν
      β χ' η'
      ((OperatorRidgelet.ridgeletExtension
          μ ν ⇑ρ)
        f)

**Theorem [thm:tempered-reconstruction]** Reconstruction with a tempered activation.  The
limit `S_β R_ρ f` does not depend on the cutoff `χ` or on the approximate identity `(η_ε)`.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.thm_tempered_reconstruction_iii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
  (hν : OperatorRidgelet.IsHomogeneous α ν)
  (β : TemperedDistribution ℝ ℂ)
  (hβ : OperatorRidgelet.IsRealDistribution β) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (χ : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ) (η : ℝ → ℝ → ℝ)
  (hη : OperatorRidgelet.IsApproximateIdentity η)
  (f : ↥(OperatorRidgelet.spectralRange μ ν)) :
  OperatorRidgelet.temperedSynthesis μ ν β χ η
      ((OperatorRidgelet.ridgeletExtension μ ν ⇑ρ) f) =
    OperatorRidgelet.temperedAdmissibilityConst α β ρ •
      (OperatorRidgelet.rieszMap μ ν) f

theorem OperatorRidgelet.Paper.thm_tempered_reconstruction_iii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (β : TemperedDistribution ℝ ℂ)
  (hβ :
    OperatorRidgelet.IsRealDistribution β)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (χ : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ)
  (η : ℝ → ℝ → ℝ)
  (hη :
    OperatorRidgelet.IsApproximateIdentity
      η)
  (f :
    ↥(OperatorRidgelet.spectralRange μ
        ν)) :
  OperatorRidgelet.temperedSynthesis μ ν β
      χ η
      ((OperatorRidgelet.ridgeletExtension
          μ ν ⇑ρ)
        f) =
    OperatorRidgelet.temperedAdmissibilityConst
        α β ρ •
      (OperatorRidgelet.rieszMap μ ν) f

**Theorem [thm:tempered-reconstruction]** Reconstruction with a tempered activation.  The
frame identity `S_β R_ρ f = C^{(α)}_{β,ρ} T_α f` for `f ∈ 𝓔_α`.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.thm_tempered_reconstruction_iv.{u_1}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
  (hν : OperatorRidgelet.IsHomogeneous α ν)
  (β : TemperedDistribution ℝ ℂ)
  (hβ : OperatorRidgelet.IsRealDistribution β) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (χ : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ) (η : ℝ → ℝ → ℝ)
  (hη : OperatorRidgelet.IsApproximateIdentity η)
  (hC : OperatorRidgelet.temperedAdmissibilityConst α β ρ ≠ 0)
  (f : ↥(OperatorRidgelet.spectralRange μ ν)) :
  f =
    (OperatorRidgelet.temperedAdmissibilityConst α β ρ)⁻¹ •
      OperatorRidgelet.rieszInv μ ν
        (OperatorRidgelet.temperedSynthesis μ ν β χ η
          ((OperatorRidgelet.ridgeletExtension μ ν ⇑ρ) f))

theorem OperatorRidgelet.Paper.thm_tempered_reconstruction_iv.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (β : TemperedDistribution ℝ ℂ)
  (hβ :
    OperatorRidgelet.IsRealDistribution β)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (χ : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ)
  (η : ℝ → ℝ → ℝ)
  (hη :
    OperatorRidgelet.IsApproximateIdentity
      η)
  (hC :
    OperatorRidgelet.temperedAdmissibilityConst
        α β ρ ≠
      0)
  (f :
    ↥(OperatorRidgelet.spectralRange μ
        ν)) :
  f =
    (OperatorRidgelet.temperedAdmissibilityConst
          α β ρ)⁻¹ •
      OperatorRidgelet.rieszInv μ ν
        (OperatorRidgelet.temperedSynthesis
          μ ν β χ η
          ((OperatorRidgelet.ridgeletExtension
              μ ν ⇑ρ)
            f))

**Theorem [thm:tempered-reconstruction]** Reconstruction with a tempered activation.  If
`C^{(α)}_{β,ρ} ≠ 0`, then `f = (C^{(α)}_{β,ρ})⁻¹ T_α⁻¹ S_β R_ρ f` for `f ∈ 𝓔_α`.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.thm_tempered_reconstruction_v.{u_1}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [CompleteSpace H] [SecondCountableTopology H] [MeasurableSpace H]
  [BorelSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
  (hν : OperatorRidgelet.IsHomogeneous α ν)
  (β : TemperedDistribution ℝ ℂ)
  (hβ : OperatorRidgelet.IsRealDistribution β) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (χ : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ) (η : ℝ → ℝ → ℝ)
  (hη : OperatorRidgelet.IsApproximateIdentity η)
  (hC : OperatorRidgelet.temperedAdmissibilityConst α β ρ ≠ 0)
  (g : OperatorRidgelet.SpectralAntiDual μ ν) :
  g =
    (OperatorRidgelet.temperedAdmissibilityConst α β ρ)⁻¹ •
      OperatorRidgelet.temperedSynthesis μ ν β χ η
        ((OperatorRidgelet.ridgeletExtension μ ν ⇑ρ)
          (OperatorRidgelet.rieszInv μ ν g))

theorem OperatorRidgelet.Paper.thm_tempered_reconstruction_v.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (β : TemperedDistribution ℝ ℂ)
  (hβ :
    OperatorRidgelet.IsRealDistribution β)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (χ : ℝ → ℝ)
  (hχ : OperatorRidgelet.IsCutoff ρ χ)
  (η : ℝ → ℝ → ℝ)
  (hη :
    OperatorRidgelet.IsApproximateIdentity
      η)
  (hC :
    OperatorRidgelet.temperedAdmissibilityConst
        α β ρ ≠
      0)
  (g :
    OperatorRidgelet.SpectralAntiDual μ
      ν) :
  g =
    (OperatorRidgelet.temperedAdmissibilityConst
          α β ρ)⁻¹ •
      OperatorRidgelet.temperedSynthesis μ
        ν β χ η
        ((OperatorRidgelet.ridgeletExtension
            μ ν ⇑ρ)
          (OperatorRidgelet.rieszInv μ ν
            g))

**Theorem [thm:tempered-reconstruction]** Reconstruction with a tempered activation.  If
`C^{(α)}_{β,ρ} ≠ 0`, then `g = (C^{(α)}_{β,ρ})⁻¹ S_β (R_ρ T_α⁻¹ g)` for `g ∈ 𝓔_α'`.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.thm_tempered_reconstruction_vi {α : ℝ}
  (hα : 0 < α) (β : TemperedDistribution ℝ ℂ)
  (hβ : OperatorRidgelet.IsRealDistribution β)
  (hpoly : ¬OperatorRidgelet.IsPolynomialDistribution β) :
  ∃ ρ,
    OperatorRidgelet.IsBandPass ρ ∧
      OperatorRidgelet.temperedAdmissibilityConst α β ρ ≠ 0

theorem OperatorRidgelet.Paper.thm_tempered_reconstruction_vi
  {α : ℝ} (hα : 0 < α)
  (β : TemperedDistribution ℝ ℂ)
  (hβ :
    OperatorRidgelet.IsRealDistribution β)
  (hpoly :
    ¬OperatorRidgelet.IsPolynomialDistribution
        β) :
  ∃ ρ,
    OperatorRidgelet.IsBandPass ρ ∧
      OperatorRidgelet.temperedAdmissibilityConst
          α β ρ ≠
        0

**Theorem [thm:tempered-reconstruction]** Reconstruction with a tempered activation.  If
`β` is not a polynomial (equivalently `β ≠ 0` in `𝒮'/𝒫`), then a band-pass `ρ` with
`C^{(α)}_{β,ρ} ≠ 0` exists.

Proof for Theorem 4.1.3

uses 0

Each \beta_\varepsilon is an admissible real filter, so the Plancherel identity gives S_{\beta_\varepsilon}R_\rho f=C_{\beta_\varepsilon,\rho}^{(\alpha)}T_\alpha f; distributional convergence of \widehat\beta*\eta_\varepsilon against the fixed test function \widehat\rho(-\omega)|\omega|^{-\alpha} gives convergence of the constants, and T_\alpha is an isometry, so the functionals converge in \mathcal E_\alpha'. The existence of \rho with nonzero constant is the last step of the proof of Theorem 3.1.5.

Corollary4.1.4

Statement uses 5

Statement dependency previews

Preview

Definition 2.2.2

Loading preview

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

used by 0✓L∃∀N

Let \beta=\operatorname{ReLU}, \operatorname{ReLU}(t)=\max(t,0). Then \widehat{\operatorname{ReLU}}=-\operatorname{fp}(\omega^{-2})+i\pi\delta_0' (i), which equals -\omega^{-2} away from the origin (ii). If \widehat\rho\in C_c^\infty(\mathbb R\setminus\{0\}) is nonzero, even, and nonpositive, then C_{\operatorname{ReLU},\rho}^{(\alpha)}=-\frac1{2\pi}\int_{\mathbb R}\widehat\rho(\omega)|\omega|^{-\alpha-2}\,\mathrm d\omega (iii), which is positive (iv). After rescaling \rho the constant is one (v), and the two reconstruction formulas of Theorem 4.1.3 (vi, vii) and Theorem 3.1.5 (iii) (viii) hold with ReLU synthesis for every \alpha>0.

Lean code for Corollary4.1.4●11 declarations

defdefined in OperatorRidgelet/Tempered/Defs.lean

complete

def OperatorRidgelet.reluDistribution : TemperedDistribution ℝ ℂ

def OperatorRidgelet.reluDistribution :
  TemperedDistribution ℝ ℂ

`ReLU ∈ 𝒮'(ℝ)`, the vendored realization `reluTemperedDistribution` (weight exponent
`t = 2`), which acts by integration against `ReLU(t) = max(t, 0)`.

defdefined in OperatorRidgelet/Tempered/Defs.lean

complete

def OperatorRidgelet.reluAdmissibilityScale (α : ℝ) (ρ : SchwartzMap ℝ ℝ) :
  ℝ

def OperatorRidgelet.reluAdmissibilityScale
  (α : ℝ) (ρ : SchwartzMap ℝ ℝ) : ℝ

The ReLU admissibility constant `-(2π)⁻¹ ∫ ρ̂(ω) |ω|^{-α-2} dω` of a filter with real `ρ̂`.

defdefined in OperatorRidgelet/Tempered/Defs.lean

complete

def OperatorRidgelet.reluNormalizedFilter (α : ℝ) (ρ : SchwartzMap ℝ ℝ) :
  SchwartzMap ℝ ℝ

def OperatorRidgelet.reluNormalizedFilter
  (α : ℝ) (ρ : SchwartzMap ℝ ℝ) :
  SchwartzMap ℝ ℝ

The filter `ρ` rescaled so that `C^{(α)}_{ReLU,ρ} = 1`.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.cor_relu_admissible_i (φ : SchwartzMap ℝ ℂ) :
  Filter.Tendsto
    (fun ε => (∫ (ω : ℝ) in {ω | ε < |ω|}, φ ω / ↑ω ^ 2) - 2 * φ 0 / ↑ε)
    (nhdsWithin 0 (Set.Ioi 0))
    (nhds
      (-(LeanRidgelet.Fourier.angularFourierDistribution
              OperatorRidgelet.reluDistribution)
            φ -
        ↑Real.pi * Complex.I * deriv (⇑φ) 0))

theorem OperatorRidgelet.Paper.cor_relu_admissible_i
  (φ : SchwartzMap ℝ ℂ) :
  Filter.Tendsto
    (fun ε =>
      (∫ (ω : ℝ) in {ω | ε < |ω|},
          φ ω / ↑ω ^ 2) -
        2 * φ 0 / ↑ε)
    (nhdsWithin 0 (Set.Ioi 0))
    (nhds
      (-(LeanRidgelet.Fourier.angularFourierDistribution
              OperatorRidgelet.reluDistribution)
            φ -
        ↑Real.pi * Complex.I *
          deriv (⇑φ) 0))

**Corollary [cor:relu-admissible]** ReLU is admissible.  Under the manuscript's convention
`ReLU^ = -fp(ω^{-2}) + iπ δ₀'`: tested against a Schwartz function `φ`, the Hadamard finite part
`⟨fp(ω^{-2}), φ⟩ = lim_{ε ↓ 0} (∫_{|ω|>ε} φ(ω) ω^{-2} dω - 2 φ(0)/ε)` equals
`-⟨ReLU^, φ⟩ - iπ φ'(0)`.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.cor_relu_admissible_ii (φ : SchwartzMap ℝ ℂ) :
  0 ∉ tsupport ⇑φ →
    (LeanRidgelet.Fourier.angularFourierDistribution
          OperatorRidgelet.reluDistribution)
        φ =
      ∫ (ω : ℝ), -(↑ω ^ 2)⁻¹ * φ ω

theorem OperatorRidgelet.Paper.cor_relu_admissible_ii
  (φ : SchwartzMap ℝ ℂ) :
  0 ∉ tsupport ⇑φ →
    (LeanRidgelet.Fourier.angularFourierDistribution
          OperatorRidgelet.reluDistribution)
        φ =
      ∫ (ω : ℝ), -(↑ω ^ 2)⁻¹ * φ ω

**Corollary [cor:relu-admissible]** ReLU is admissible.  Away from the origin `ReLU^` equals
`-ω^{-2}`: `⟨ReLU^, φ⟩ = ∫ (-ω^{-2}) φ(ω) dω` for every Schwartz `φ` supported away from `0`.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.cor_relu_admissible_iii {α : ℝ} (hα : 0 < α)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsBandPass ρ)
  (hρ_real : ∀ (ω : ℝ), (OperatorRidgelet.filterFourier (⇑ρ) ω).im = 0)
  (hρ_even :
    ∀ (ω : ℝ),
      OperatorRidgelet.filterFourier (⇑ρ) (-ω) =
        OperatorRidgelet.filterFourier (⇑ρ) ω)
  (hρ_nonpos :
    ∀ (ω : ℝ), (OperatorRidgelet.filterFourier (⇑ρ) ω).re ≤ 0) :
  OperatorRidgelet.temperedAdmissibilityConst α
      OperatorRidgelet.reluDistribution ρ =
    ↑(OperatorRidgelet.reluAdmissibilityScale α ρ)

theorem OperatorRidgelet.Paper.cor_relu_admissible_iii
  {α : ℝ} (hα : 0 < α)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (hρ_real :
    ∀ (ω : ℝ),
      (OperatorRidgelet.filterFourier (⇑ρ)
            ω).im =
        0)
  (hρ_even :
    ∀ (ω : ℝ),
      OperatorRidgelet.filterFourier (⇑ρ)
          (-ω) =
        OperatorRidgelet.filterFourier
          (⇑ρ) ω)
  (hρ_nonpos :
    ∀ (ω : ℝ),
      (OperatorRidgelet.filterFourier (⇑ρ)
            ω).re ≤
        0) :
  OperatorRidgelet.temperedAdmissibilityConst
      α OperatorRidgelet.reluDistribution
      ρ =
    ↑(OperatorRidgelet.reluAdmissibilityScale
        α ρ)

**Corollary [cor:relu-admissible]** ReLU is admissible.  If `ρ̂ ∈ C_c^∞(ℝ ∖ {0})` is
nonzero, even, and nonpositive, then `C^{(α)}_{ReLU,ρ} = -(2π)⁻¹ ∫ ρ̂(ω) |ω|^{-α-2} dω`.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.cor_relu_admissible_iv {α : ℝ} (hα : 0 < α)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsBandPass ρ)
  (hρ_real : ∀ (ω : ℝ), (OperatorRidgelet.filterFourier (⇑ρ) ω).im = 0)
  (hρ_even :
    ∀ (ω : ℝ),
      OperatorRidgelet.filterFourier (⇑ρ) (-ω) =
        OperatorRidgelet.filterFourier (⇑ρ) ω)
  (hρ_nonpos :
    ∀ (ω : ℝ), (OperatorRidgelet.filterFourier (⇑ρ) ω).re ≤ 0) :
  0 < OperatorRidgelet.reluAdmissibilityScale α ρ

theorem OperatorRidgelet.Paper.cor_relu_admissible_iv
  {α : ℝ} (hα : 0 < α)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (hρ_real :
    ∀ (ω : ℝ),
      (OperatorRidgelet.filterFourier (⇑ρ)
            ω).im =
        0)
  (hρ_even :
    ∀ (ω : ℝ),
      OperatorRidgelet.filterFourier (⇑ρ)
          (-ω) =
        OperatorRidgelet.filterFourier
          (⇑ρ) ω)
  (hρ_nonpos :
    ∀ (ω : ℝ),
      (OperatorRidgelet.filterFourier (⇑ρ)
            ω).re ≤
        0) :
  0 <
    OperatorRidgelet.reluAdmissibilityScale
      α ρ

**Corollary [cor:relu-admissible]** ReLU is admissible.  Under the same hypotheses the
constant `-(2π)⁻¹ ∫ ρ̂(ω) |ω|^{-α-2} dω` is positive.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.cor_relu_admissible_v {α : ℝ} (hα : 0 < α)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsBandPass ρ)
  (hρ_real : ∀ (ω : ℝ), (OperatorRidgelet.filterFourier (⇑ρ) ω).im = 0)
  (hρ_even :
    ∀ (ω : ℝ),
      OperatorRidgelet.filterFourier (⇑ρ) (-ω) =
        OperatorRidgelet.filterFourier (⇑ρ) ω)
  (hρ_nonpos :
    ∀ (ω : ℝ), (OperatorRidgelet.filterFourier (⇑ρ) ω).re ≤ 0) :
  OperatorRidgelet.IsBandPass
      (OperatorRidgelet.reluNormalizedFilter α ρ) ∧
    OperatorRidgelet.temperedAdmissibilityConst α
        OperatorRidgelet.reluDistribution
        (OperatorRidgelet.reluNormalizedFilter α ρ) =
      1

theorem OperatorRidgelet.Paper.cor_relu_admissible_v
  {α : ℝ} (hα : 0 < α)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (hρ_real :
    ∀ (ω : ℝ),
      (OperatorRidgelet.filterFourier (⇑ρ)
            ω).im =
        0)
  (hρ_even :
    ∀ (ω : ℝ),
      OperatorRidgelet.filterFourier (⇑ρ)
          (-ω) =
        OperatorRidgelet.filterFourier
          (⇑ρ) ω)
  (hρ_nonpos :
    ∀ (ω : ℝ),
      (OperatorRidgelet.filterFourier (⇑ρ)
            ω).re ≤
        0) :
  OperatorRidgelet.IsBandPass
      (OperatorRidgelet.reluNormalizedFilter
        α ρ) ∧
    OperatorRidgelet.temperedAdmissibilityConst
        α
        OperatorRidgelet.reluDistribution
        (OperatorRidgelet.reluNormalizedFilter
          α ρ) =
      1

**Corollary [cor:relu-admissible]** ReLU is admissible.  After rescaling, `ρ` is still
band-pass and `C^{(α)}_{ReLU,ρ} = 1`.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.cor_relu_admissible_vi.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsBandPass ρ)
  (hρ_real : ∀ (ω : ℝ), (OperatorRidgelet.filterFourier (⇑ρ) ω).im = 0)
  (hρ_even :
    ∀ (ω : ℝ),
      OperatorRidgelet.filterFourier (⇑ρ) (-ω) =
        OperatorRidgelet.filterFourier (⇑ρ) ω)
  (hρ_nonpos :
    ∀ (ω : ℝ), (OperatorRidgelet.filterFourier (⇑ρ) ω).re ≤ 0)
  (χ : ℝ → ℝ)
  (hχ :
    OperatorRidgelet.IsCutoff
      (OperatorRidgelet.reluNormalizedFilter α ρ) χ)
  (η : ℝ → ℝ → ℝ) (hη : OperatorRidgelet.IsApproximateIdentity η)
  (f : ↥(OperatorRidgelet.spectralRange μ ν)) :
  f =
    OperatorRidgelet.rieszInv μ ν
      (OperatorRidgelet.temperedSynthesis μ ν
        OperatorRidgelet.reluDistribution χ η
        ((OperatorRidgelet.ridgeletExtension μ ν
            ⇑(OperatorRidgelet.reluNormalizedFilter α ρ))
          f))

theorem OperatorRidgelet.Paper.cor_relu_admissible_vi.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (hρ_real :
    ∀ (ω : ℝ),
      (OperatorRidgelet.filterFourier (⇑ρ)
            ω).im =
        0)
  (hρ_even :
    ∀ (ω : ℝ),
      OperatorRidgelet.filterFourier (⇑ρ)
          (-ω) =
        OperatorRidgelet.filterFourier
          (⇑ρ) ω)
  (hρ_nonpos :
    ∀ (ω : ℝ),
      (OperatorRidgelet.filterFourier (⇑ρ)
            ω).re ≤
        0)
  (χ : ℝ → ℝ)
  (hχ :
    OperatorRidgelet.IsCutoff
      (OperatorRidgelet.reluNormalizedFilter
        α ρ)
      χ)
  (η : ℝ → ℝ → ℝ)
  (hη :
    OperatorRidgelet.IsApproximateIdentity
      η)
  (f :
    ↥(OperatorRidgelet.spectralRange μ
        ν)) :
  f =
    OperatorRidgelet.rieszInv μ ν
      (OperatorRidgelet.temperedSynthesis
        μ ν
        OperatorRidgelet.reluDistribution
        χ η
        ((OperatorRidgelet.ridgeletExtension
            μ ν
            ⇑(OperatorRidgelet.reluNormalizedFilter
                α ρ))
          f))

**Corollary [cor:relu-admissible]** ReLU is admissible.  With the rescaled filter the first
reconstruction formula holds with ReLU synthesis for every `α > 0`:
`f = T_α⁻¹ S_{ReLU} R_ρ f` for `f ∈ 𝓔_α`.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.cor_relu_admissible_vii.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H) [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsBandPass ρ)
  (hρ_real : ∀ (ω : ℝ), (OperatorRidgelet.filterFourier (⇑ρ) ω).im = 0)
  (hρ_even :
    ∀ (ω : ℝ),
      OperatorRidgelet.filterFourier (⇑ρ) (-ω) =
        OperatorRidgelet.filterFourier (⇑ρ) ω)
  (hρ_nonpos :
    ∀ (ω : ℝ), (OperatorRidgelet.filterFourier (⇑ρ) ω).re ≤ 0)
  (χ : ℝ → ℝ)
  (hχ :
    OperatorRidgelet.IsCutoff
      (OperatorRidgelet.reluNormalizedFilter α ρ) χ)
  (η : ℝ → ℝ → ℝ) (hη : OperatorRidgelet.IsApproximateIdentity η)
  (g : OperatorRidgelet.SpectralAntiDual μ ν) :
  g =
    OperatorRidgelet.temperedSynthesis μ ν
      OperatorRidgelet.reluDistribution χ η
      ((OperatorRidgelet.ridgeletExtension μ ν
          ⇑(OperatorRidgelet.reluNormalizedFilter α ρ))
        (OperatorRidgelet.rieszInv μ ν g))

theorem OperatorRidgelet.Paper.cor_relu_admissible_vii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (hρ_real :
    ∀ (ω : ℝ),
      (OperatorRidgelet.filterFourier (⇑ρ)
            ω).im =
        0)
  (hρ_even :
    ∀ (ω : ℝ),
      OperatorRidgelet.filterFourier (⇑ρ)
          (-ω) =
        OperatorRidgelet.filterFourier
          (⇑ρ) ω)
  (hρ_nonpos :
    ∀ (ω : ℝ),
      (OperatorRidgelet.filterFourier (⇑ρ)
            ω).re ≤
        0)
  (χ : ℝ → ℝ)
  (hχ :
    OperatorRidgelet.IsCutoff
      (OperatorRidgelet.reluNormalizedFilter
        α ρ)
      χ)
  (η : ℝ → ℝ → ℝ)
  (hη :
    OperatorRidgelet.IsApproximateIdentity
      η)
  (g :
    OperatorRidgelet.SpectralAntiDual μ
      ν) :
  g =
    OperatorRidgelet.temperedSynthesis μ ν
      OperatorRidgelet.reluDistribution χ
      η
      ((OperatorRidgelet.ridgeletExtension
          μ ν
          ⇑(OperatorRidgelet.reluNormalizedFilter
              α ρ))
        (OperatorRidgelet.rieszInv μ ν g))

**Corollary [cor:relu-admissible]** ReLU is admissible.  With the rescaled filter the second
reconstruction formula holds with ReLU synthesis for every `α > 0`:
`g = S_{ReLU} (R_ρ T_α⁻¹ g)` for `g ∈ 𝓔_α'`.

theoremdefined in OperatorRidgelet/Paper/Tempered.lean

complete

theorem OperatorRidgelet.Paper.cor_relu_admissible_viii.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H) [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ} (hα : 0 < α)
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (hρ_real : ∀ (ω : ℝ), (OperatorRidgelet.filterFourier (⇑ρ) ω).im = 0)
  (hρ_even :
    ∀ (ω : ℝ),
      OperatorRidgelet.filterFourier (⇑ρ) (-ω) =
        OperatorRidgelet.filterFourier (⇑ρ) ω)
  (hρ_nonpos :
    ∀ (ω : ℝ), (OperatorRidgelet.filterFourier (⇑ρ) ω).re ≤ 0)
  (I : Set ℝ) (hI : OperatorRidgelet.IsFrequencyWindow (⇑ρ) I)
  (G : H → ℂ) (hG : OperatorRidgelet.IsRegularAlongRays ν I G) (x : H) :
  (∀ᵐ (a : H) ∂ν,
      MeasureTheory.Integrable
        (fun c =>
          OperatorRidgelet.coefficientFormula
              (⇑(OperatorRidgelet.reluNormalizedFilter α ρ)) G (a, c) *
            ↑(LeanRidgelet.relu (inner ℝ a x + c)))
        MeasureTheory.volume) ∧
    MeasureTheory.Integrable
        (fun a =>
          ∫ (c : ℝ),
            OperatorRidgelet.coefficientFormula
                (⇑(OperatorRidgelet.reluNormalizedFilter α ρ)) G
                (a, c) *
              ↑(LeanRidgelet.relu (inner ℝ a x + c)))
        ν ∧
      ∫ (a : H),
          ∫ (c : ℝ),
            OperatorRidgelet.coefficientFormula
                (⇑(OperatorRidgelet.reluNormalizedFilter α ρ)) G
                (a, c) *
              ↑(LeanRidgelet.relu (inner ℝ a x + c)) ∂ν =
        OperatorRidgelet.spectralTarget ν G x

theorem OperatorRidgelet.Paper.cor_relu_admissible_viii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  [ν.IsOpenPosMeasure] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (hρ_real :
    ∀ (ω : ℝ),
      (OperatorRidgelet.filterFourier (⇑ρ)
            ω).im =
        0)
  (hρ_even :
    ∀ (ω : ℝ),
      OperatorRidgelet.filterFourier (⇑ρ)
          (-ω) =
        OperatorRidgelet.filterFourier
          (⇑ρ) ω)
  (hρ_nonpos :
    ∀ (ω : ℝ),
      (OperatorRidgelet.filterFourier (⇑ρ)
            ω).re ≤
        0)
  (I : Set ℝ)
  (hI :
    OperatorRidgelet.IsFrequencyWindow
      (⇑ρ) I)
  (G : H → ℂ)
  (hG :
    OperatorRidgelet.IsRegularAlongRays ν
      I G)
  (x : H) :
  (∀ᵐ (a : H) ∂ν,
      MeasureTheory.Integrable
        (fun c =>
          OperatorRidgelet.coefficientFormula
              (⇑(OperatorRidgelet.reluNormalizedFilter
                  α ρ))
              G (a, c) *
            ↑(LeanRidgelet.relu
                (inner ℝ a x + c)))
        MeasureTheory.volume) ∧
    MeasureTheory.Integrable
        (fun a =>
          ∫ (c : ℝ),
            OperatorRidgelet.coefficientFormula
                (⇑(OperatorRidgelet.reluNormalizedFilter
                    α ρ))
                G (a, c) *
              ↑(LeanRidgelet.relu
                  (inner ℝ a x + c)))
        ν ∧
      ∫ (a : H),
          ∫ (c : ℝ),
            OperatorRidgelet.coefficientFormula
                (⇑(OperatorRidgelet.reluNormalizedFilter
                    α ρ))
                G (a, c) *
              ↑(LeanRidgelet.relu
                  (inner ℝ a x + c)) ∂ν =
        OperatorRidgelet.spectralTarget ν
          G x

**Corollary [cor:relu-admissible]** ReLU is admissible.  With the rescaled filter Theorem
A(iii) holds with ReLU synthesis for every `α > 0`: for `G` regular along rays and every `x`,
the inner integral `∫ γ_G(a,c) ReLU(⟪a,x⟫ + c) dc` converges absolutely for `ν`-almost every
`a`, its `ν`-integral converges absolutely, and it equals `g_G(x)`.

Proof for Corollary 4.1.4

uses 0

From \operatorname{ReLU}(t)=(|t|+t)/2, the identities \widehat{|t|}=-2\operatorname{fp}(\omega^{-2}) and \widehat t=2\pi i\delta_0' give the Fourier transform; the test function is supported away from zero, so the \delta_0' term vanishes and the finite part is ordinary multiplication by \omega^{-2}, and evenness and the sign of \widehat\rho give the constant.