2.4. Plancherel identity, closed range, and injectivity🔗

The formalization proves the Plancherel theory first for the abstract pair (\mu,\nu) (Appendix H) and then specializes to the Gaussian pair.

Theorem2.4.1

Statement uses 7

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 \mu be a Borel probability measure on H and \nu a \sigma-finite Borel measure with full support and (D_\omega)_\#\nu=|\omega|^{-\alpha}\nu for \omega\ne0; define \mathcal G_\mu, \mathcal D_{\mu,\nu}, and the completion \mathcal E_{\mu,\nu} as in the Gaussian case. Then the Fourier-slice identity, Theorem 3.1.5, Theorem 2.4.2, and Theorem 3.2.7 (i)–(iii) remain valid with (\mu_Q,\nu_\alpha) replaced by (\mu,\nu): for f\in\mathcal D_{\mu,\nu} the transform lies in L^2(\lambda) and satisfies the Plancherel identity, R_\rho has a unique bounded extension of norm at most ((\!(\rho,\rho)\!)_\alpha)^{1/2} (with equality when the core is nonzero), with closed range and R_\rho=W_\rho U, and R_\rho f=0 implies f=0. Moreover 1\in\mathcal D_{\mu,\nu} if and only if \int_H|\widehat\mu(\xi)|^2\nu(\mathrm d\xi)<\infty. The abstract-weight versions of Theorem 3.1.5 and Theorem 3.2.7 are the Lean statements of those theorems themselves. The backprojection and coefficient stability results also hold. If, in addition, \nu is finite on bounded sets, the spectral-density construction gives compact-open universality. Full support alone does not imply this local finiteness assumption. Gaussian decay and Hermite inversion retain their Gaussian hypotheses.

Lean code for Theorem2.4.1●11 theorems

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.thm_general_weights_plancherel_memLp.{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.IsAdmissible α ρ)
  (f : ↥(MeasureTheory.Lp ℂ 2 μ))
  (hf : f ∈ OperatorRidgelet.spectralCore μ ν) :
  MeasureTheory.MemLp (OperatorRidgelet.ridgelet μ ⇑ρ ↑↑f) 2
    (OperatorRidgelet.parameterMeasure ν)

theorem OperatorRidgelet.Paper.thm_general_weights_plancherel_memLp.{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.IsAdmissible α ρ)
  (f : ↥(MeasureTheory.Lp ℂ 2 μ))
  (hf :
    f ∈
      OperatorRidgelet.spectralCore μ ν) :
  MeasureTheory.MemLp
    (OperatorRidgelet.ridgelet μ ⇑ρ ↑↑f) 2
    (OperatorRidgelet.parameterMeasure ν)

**Theorem [thm:general-weights]** Abstract-weight extension.  Theorem `thm:B`(i) for the
abstract pair: `R_ρ f ∈ L²(λ)` for `f ∈ 𝒟_{μ,ν}` and `α`-admissible `ρ`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.thm_general_weights_plancherel.{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.IsAdmissible α ρ₁)
  (hρ₂ : OperatorRidgelet.IsAdmissible α ρ₂)
  (f g : ↥(MeasureTheory.Lp ℂ 2 μ))
  (hf : f ∈ OperatorRidgelet.spectralCore μ ν)
  (hg : g ∈ OperatorRidgelet.spectralCore μ ν) :
  ∫ (p : H × ℝ),
      OperatorRidgelet.ridgelet μ (⇑ρ₁) (↑↑f) p *
        (starRingEnd ℂ)
          (OperatorRidgelet.ridgelet μ (⇑ρ₂) (↑↑g)
            p) ∂OperatorRidgelet.parameterMeasure ν =
    OperatorRidgelet.crossAdmissibilityConst α ⇑ρ₁ ⇑ρ₂ *
      OperatorRidgelet.spectralInner μ ν ↑↑f ↑↑g

theorem OperatorRidgelet.Paper.thm_general_weights_plancherel.{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.IsAdmissible α ρ₁)
  (hρ₂ :
    OperatorRidgelet.IsAdmissible α ρ₂)
  (f g : ↥(MeasureTheory.Lp ℂ 2 μ))
  (hf :
    f ∈ OperatorRidgelet.spectralCore μ ν)
  (hg :
    g ∈
      OperatorRidgelet.spectralCore μ ν) :
  ∫ (p : H × ℝ),
      OperatorRidgelet.ridgelet μ (⇑ρ₁)
          (↑↑f) p *
        (starRingEnd ℂ)
          (OperatorRidgelet.ridgelet μ
            (⇑ρ₂) (↑↑g)
            p) ∂OperatorRidgelet.parameterMeasure
        ν =
    OperatorRidgelet.crossAdmissibilityConst
        α ⇑ρ₁ ⇑ρ₂ *
      OperatorRidgelet.spectralInner μ ν
        ↑↑f ↑↑g

**Theorem [thm:general-weights]** Abstract-weight extension.  Theorem `thm:B`(i) for the
abstract pair: the Plancherel identity
`⟨R_{ρ₁} f, R_{ρ₂} g⟩_{L²(λ)} = C^{(α)}_{ρ₁,ρ₂} ⟨f,g⟩_{𝓔_{μ,ν}}`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.thm_general_weights_extension.{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.IsAdmissible α ρ) :
  ∃! R,
    ∀ (f : ↥(OperatorRidgelet.spectralCore μ ν)),
      ↑↑(R
              (OperatorRidgelet.spectralEmbed μ ν
                f)) =ᵐ[OperatorRidgelet.parameterMeasure ν]
        OperatorRidgelet.ridgelet μ ⇑ρ ↑↑↑f

theorem OperatorRidgelet.Paper.thm_general_weights_extension.{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.IsAdmissible α ρ) :
  ∃! R,
    ∀
      (f :
        ↥(OperatorRidgelet.spectralCore μ
            ν)),
      ↑↑(R
              (OperatorRidgelet.spectralEmbed
                μ ν
                f)) =ᵐ[OperatorRidgelet.parameterMeasure
          ν]
        OperatorRidgelet.ridgelet μ ⇑ρ
          ↑↑↑f

**Theorem [thm:general-weights]** Abstract-weight extension.  Theorem `thm:B`(ii) for the
abstract pair: the unique bounded extension `R_ρ : 𝓔_{μ,ν} → L²(λ)`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.thm_general_weights_extension_norm.{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.IsAdmissible α ρ)
  (R :
    ↥(OperatorRidgelet.spectralRange μ ν) →L[ℂ]
      ↥(MeasureTheory.Lp ℂ 2 (OperatorRidgelet.parameterMeasure ν)))
  (hR :
    ∀ (f : ↥(OperatorRidgelet.spectralCore μ ν)),
      ↑↑(R
              (OperatorRidgelet.spectralEmbed μ ν
                f)) =ᵐ[OperatorRidgelet.parameterMeasure ν]
        OperatorRidgelet.ridgelet μ ⇑ρ ↑↑↑f)
  (G : ↥(OperatorRidgelet.spectralRange μ ν)) :
  ‖R G‖ ^ 2 = OperatorRidgelet.admissibilityConst α ⇑ρ * ‖G‖ ^ 2

theorem OperatorRidgelet.Paper.thm_general_weights_extension_norm.{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.IsAdmissible α ρ)
  (R :
    ↥(OperatorRidgelet.spectralRange μ
          ν) →L[ℂ]
      ↥(MeasureTheory.Lp ℂ 2
          (OperatorRidgelet.parameterMeasure
            ν)))
  (hR :
    ∀
      (f :
        ↥(OperatorRidgelet.spectralCore μ
            ν)),
      ↑↑(R
              (OperatorRidgelet.spectralEmbed
                μ ν
                f)) =ᵐ[OperatorRidgelet.parameterMeasure
          ν]
        OperatorRidgelet.ridgelet μ ⇑ρ
          ↑↑↑f)
  (G :
    ↥(OperatorRidgelet.spectralRange μ
        ν)) :
  ‖R G‖ ^ 2 =
    OperatorRidgelet.admissibilityConst α
        ⇑ρ *
      ‖G‖ ^ 2

**Theorem [thm:general-weights]** Abstract-weight extension.  Theorem `thm:B`(ii) for the
abstract pair: `‖R_ρ f‖² = C^{(α)}_ρ ‖f‖²_{𝓔_{μ,ν}}`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.thm_general_weights_extension_closed_range.{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.IsAdmissible α ρ)
  (R :
    ↥(OperatorRidgelet.spectralRange μ ν) →L[ℂ]
      ↥(MeasureTheory.Lp ℂ 2 (OperatorRidgelet.parameterMeasure ν)))
  (hR :
    ∀ (f : ↥(OperatorRidgelet.spectralCore μ ν)),
      ↑↑(R
              (OperatorRidgelet.spectralEmbed μ ν
                f)) =ᵐ[OperatorRidgelet.parameterMeasure ν]
        OperatorRidgelet.ridgelet μ ⇑ρ ↑↑↑f) :
  IsClosed (Set.range ⇑R)

theorem OperatorRidgelet.Paper.thm_general_weights_extension_closed_range.{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.IsAdmissible α ρ)
  (R :
    ↥(OperatorRidgelet.spectralRange μ
          ν) →L[ℂ]
      ↥(MeasureTheory.Lp ℂ 2
          (OperatorRidgelet.parameterMeasure
            ν)))
  (hR :
    ∀
      (f :
        ↥(OperatorRidgelet.spectralCore μ
            ν)),
      ↑↑(R
              (OperatorRidgelet.spectralEmbed
                μ ν
                f)) =ᵐ[OperatorRidgelet.parameterMeasure
          ν]
        OperatorRidgelet.ridgelet μ ⇑ρ
          ↑↑↑f) :
  IsClosed (Set.range ⇑R)

**Theorem [thm:general-weights]** Abstract-weight extension.  Theorem `thm:B`(ii) for the
abstract pair: the extension has closed range.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.thm_general_weights_extension_coefficient.{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.IsAdmissible α ρ)
  (R :
    ↥(OperatorRidgelet.spectralRange μ ν) →L[ℂ]
      ↥(MeasureTheory.Lp ℂ 2 (OperatorRidgelet.parameterMeasure ν)))
  (hR :
    ∀ (f : ↥(OperatorRidgelet.spectralCore μ ν)),
      ↑↑(R
              (OperatorRidgelet.spectralEmbed μ ν
                f)) =ᵐ[OperatorRidgelet.parameterMeasure ν]
        OperatorRidgelet.ridgelet μ ⇑ρ ↑↑↑f)
  (G : ↥(OperatorRidgelet.spectralRange μ ν)) :
  R G = OperatorRidgelet.spectralCoefficient ν ⇑ρ ↑↑↑G

theorem OperatorRidgelet.Paper.thm_general_weights_extension_coefficient.{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.IsAdmissible α ρ)
  (R :
    ↥(OperatorRidgelet.spectralRange μ
          ν) →L[ℂ]
      ↥(MeasureTheory.Lp ℂ 2
          (OperatorRidgelet.parameterMeasure
            ν)))
  (hR :
    ∀
      (f :
        ↥(OperatorRidgelet.spectralCore μ
            ν)),
      ↑↑(R
              (OperatorRidgelet.spectralEmbed
                μ ν
                f)) =ᵐ[OperatorRidgelet.parameterMeasure
          ν]
        OperatorRidgelet.ridgelet μ ⇑ρ
          ↑↑↑f)
  (G :
    ↥(OperatorRidgelet.spectralRange μ
        ν)) :
  R G =
    OperatorRidgelet.spectralCoefficient ν
      ⇑ρ ↑↑↑G

**Theorem [thm:general-weights]** Abstract-weight extension.  Theorem `thm:B`(ii) for the
abstract pair: `R_ρ = W_ρ U`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.thm_general_weights_injective.{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.IsAdmissible α ρ) (f : H → ℂ)
  (hf : MeasureTheory.MemLp f 2 μ)
  (h :
    OperatorRidgelet.ridgelet μ (⇑ρ)
        f =ᵐ[OperatorRidgelet.parameterMeasure ν]
      0) :
  f =ᵐ[μ] 0

theorem OperatorRidgelet.Paper.thm_general_weights_injective.{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.IsAdmissible α ρ)
  (f : H → ℂ)
  (hf : MeasureTheory.MemLp f 2 μ)
  (h :
    OperatorRidgelet.ridgelet μ (⇑ρ)
        f =ᵐ[OperatorRidgelet.parameterMeasure
        ν]
      0) :
  f =ᵐ[μ] 0

**Theorem [thm:general-weights]** Abstract-weight extension.  Theorem `thm:B`(iii) for the
abstract pair: `R_ρ f = 0` `λ`-a.e. implies `f = 0` `μ`-a.e. for `f ∈ L²(μ)`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.thm_general_weights_one_mem_iff.{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 α ν) :
  MeasureTheory.MemLp.toLp (fun x => 1) ⋯ ∈
      OperatorRidgelet.spectralCore μ ν ↔
    MeasureTheory.Integrable (fun ξ => ‖MeasureTheory.charFun μ ξ‖ ^ 2)
      ν

theorem OperatorRidgelet.Paper.thm_general_weights_one_mem_iff.{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 α ν) :
  MeasureTheory.MemLp.toLp (fun x => 1)
        ⋯ ∈
      OperatorRidgelet.spectralCore μ ν ↔
    MeasureTheory.Integrable
      (fun ξ =>
        ‖MeasureTheory.charFun μ ξ‖ ^ 2)
      ν

**Theorem [thm:general-weights]** Abstract-weight extension.  `1 ∈ 𝒟_{μ,ν}` if and only if
`∫ |μ̂(ξ)|² ν(dξ) < ∞`.

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

theorem OperatorRidgelet.Paper.thm_general_weights_dense.{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 α ν)
  (hfin : ∀ (R : ℝ), ν (Metric.closedBall 0 R) < ⊤)
  (β : TemperedDistribution ℝ ℂ) (b : ℝ → ℝ)
  (hβ : OperatorRidgelet.IsTemperedFunction β b)
  (hpoly : ¬OperatorRidgelet.IsPolynomialFun b) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (hC : OperatorRidgelet.temperedAdmissibilityConst α β ρ = 1)
  (I : Set ℝ) (hI : OperatorRidgelet.IsFrequencyWindow (⇑ρ) I)
  {f : H → ℂ} (hf : Continuous f) {K : Set H} (hK : IsCompact K) {ε : ℝ}
  (hε : 0 < ε) :
  ∃ N v a c,
    (OperatorRidgelet.compactSupNorm K fun x =>
        f x -
          OperatorRidgelet.finiteNetwork (fun t => ↑(b t)) v a c x) <
      ε

theorem OperatorRidgelet.Paper.thm_general_weights_dense.{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 α ν)
  (hfin :
    ∀ (R : ℝ),
      ν (Metric.closedBall 0 R) < ⊤)
  (β : TemperedDistribution ℝ ℂ)
  (b : ℝ → ℝ)
  (hβ :
    OperatorRidgelet.IsTemperedFunction β
      b)
  (hpoly :
    ¬OperatorRidgelet.IsPolynomialFun b)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (hC :
    OperatorRidgelet.temperedAdmissibilityConst
        α β ρ =
      1)
  (I : Set ℝ)
  (hI :
    OperatorRidgelet.IsFrequencyWindow
      (⇑ρ) I)
  {f : H → ℂ} (hf : Continuous f)
  {K : Set H} (hK : IsCompact K) {ε : ℝ}
  (hε : 0 < ε) :
  ∃ N v a c,
    (OperatorRidgelet.compactSupNorm K
        fun x =>
        f x -
          OperatorRidgelet.finiteNetwork
            (fun t => ↑(b t)) v a c x) <
      ε

**Theorem [thm:general-weights]** Bounded-set finite direction weights retain universality.

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

theorem OperatorRidgelet.Paper.thm_general_weights_backprojection.{u_1}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.SigmaFinite ν]
  {α : ℝ} (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f : ↥(OperatorRidgelet.spectralRange μ ν)) :
  OperatorRidgelet.backprojection α ν ⇑ρ
      ↑↑((OperatorRidgelet.ridgeletExtension μ ν ⇑ρ) f) =ᵐ[ν]
    fun ξ => ↑(OperatorRidgelet.admissibilityConst α ⇑ρ) * ↑↑↑f ξ

theorem OperatorRidgelet.Paper.thm_general_weights_backprojection.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f :
    ↥(OperatorRidgelet.spectralRange μ
        ν)) :
  OperatorRidgelet.backprojection α ν ⇑ρ
      ↑↑((OperatorRidgelet.ridgeletExtension
              μ ν ⇑ρ)
            f) =ᵐ[ν]
    fun ξ =>
    ↑(OperatorRidgelet.admissibilityConst
          α ⇑ρ) *
      ↑↑↑f ξ

**Theorem [thm:general-weights]** Abstract input weights retain completed backprojection.

theoremdefined in OperatorRidgelet/Paper/Revision.lean

complete

theorem OperatorRidgelet.Paper.thm_general_weights_stability.{u_1}
  {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H] (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.SigmaFinite ν]
  {α : ℝ} (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f : ↥(OperatorRidgelet.spectralRange μ ν))
  (γ : ↥(MeasureTheory.Lp ℂ 2 (OperatorRidgelet.parameterMeasure ν)))
  {δ : ℝ}
  (hδ : ‖γ - (OperatorRidgelet.ridgeletExtension μ ν ⇑ρ) f‖ ≤ δ) :
  ‖(OperatorRidgelet.coefficientDecoder α μ ν ⇑ρ) γ - f‖ ≤
    δ / √(OperatorRidgelet.admissibilityConst α ⇑ρ)

theorem OperatorRidgelet.Paper.thm_general_weights_stability.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  (μ ν : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.SigmaFinite ν] {α : ℝ}
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f :
    ↥(OperatorRidgelet.spectralRange μ ν))
  (γ :
    ↥(MeasureTheory.Lp ℂ 2
        (OperatorRidgelet.parameterMeasure
          ν)))
  {δ : ℝ}
  (hδ :
    ‖γ -
          (OperatorRidgelet.ridgeletExtension
              μ ν ⇑ρ)
            f‖ ≤
      δ) :
  ‖(OperatorRidgelet.coefficientDecoder α
            μ ν ⇑ρ)
          γ -
        f‖ ≤
    δ /
      √(OperatorRidgelet.admissibilityConst
          α ⇑ρ)

**Theorem [thm:general-weights]** Stability holds for an arbitrary probability input weight.

Proof for Theorem 2.4.1

uses 0

Since \mu is finite, f\mu is a finite complex measure and \mathcal G_\mu f is continuous; the proofs use only Fubini, the one-dimensional Plancherel and Parseval identities, and the homogeneity substitution, which holds for \nu by assumption. Completing \mathcal D_{\mu,\nu} makes \mathcal G_\mu unitary onto the closure of its range, and full support with Fourier uniqueness gives injectivity; finally \mathcal G_\mu1=\widehat\mu.

Theorem2.4.2

Statement uses 8

Statement dependency previews

Preview

Lemma 2.1.4

Loading preview

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

Used by 7

Reverse dependency previews

Preview

Corollary 2.5.2

Loading preview

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

✓L∃∀N

Let \alpha>0. (i) For f,g\in\mathcal D_\alpha and \alpha-admissible \rho_1,\rho_2, the transforms R_{\rho_1}f and R_{\rho_2}g belong to L^2(\lambda_\alpha), and \langle R_{\rho_1}f,R_{\rho_2}g\rangle_{L^2(\lambda_\alpha)}=(\!(\rho_1,\rho_2)\!)_\alpha\langle f,g\rangle_{\mathcal E_\alpha}. (ii) An \alpha-admissible \rho determines a unique bounded extension R_\rho:\mathcal E_\alpha\to L^2(\lambda_\alpha) with \|R_\rho f\|^2=(\!(\rho,\rho)\!)_\alpha\|f\|_{\mathcal E_\alpha}^2; its range is closed, and R_\rho=W_\rho U_\alpha. (iii) If \rho is \alpha-admissible and f\in L^1(H,\mu_Q), then R_\rho f=0 \lambda_\alpha-almost everywhere implies f=0 \mu_Q-almost everywhere.

Lean code for Theorem2.4.2●7 theorems

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.thm_B_i_a.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H) {P Q : H →L[ℝ] H}
  (hP : OperatorRidgelet.IsTraceClassCovariance P)
  (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN : OperatorRidgelet.IsCenteredGaussianLayers P N) {α : ℝ}
  (hα : 0 < α) (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f : ↥(MeasureTheory.Lp ℂ 2 μ))
  (hf :
    f ∈
      OperatorRidgelet.spectralCore μ
        (OperatorRidgelet.gaussianMixture N α)) :
  MeasureTheory.MemLp (OperatorRidgelet.ridgelet μ ⇑ρ ↑↑f) 2
    (OperatorRidgelet.parameterMeasure
      (OperatorRidgelet.gaussianMixture N α))

theorem OperatorRidgelet.Paper.thm_B_i_a.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {P Q : H →L[ℝ] H}
  (hP :
    OperatorRidgelet.IsTraceClassCovariance
      P)
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN :
    OperatorRidgelet.IsCenteredGaussianLayers
      P N)
  {α : ℝ} (hα : 0 < α)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f : ↥(MeasureTheory.Lp ℂ 2 μ))
  (hf :
    f ∈
      OperatorRidgelet.spectralCore μ
        (OperatorRidgelet.gaussianMixture
          N α)) :
  MeasureTheory.MemLp
    (OperatorRidgelet.ridgelet μ ⇑ρ ↑↑f) 2
    (OperatorRidgelet.parameterMeasure
      (OperatorRidgelet.gaussianMixture N
        α))

**Theorem [thm:B]** Plancherel identity and injectivity.  For `f ∈ 𝒟_α` and an
`α`-admissible `ρ`, the transform `R_ρ f` belongs to `L²(λ_α)`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.thm_B_i_b.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H) {P Q : H →L[ℝ] H}
  (hP : OperatorRidgelet.IsTraceClassCovariance P)
  (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN : OperatorRidgelet.IsCenteredGaussianLayers P N) {α : ℝ}
  (hα : 0 < α) (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ)
  (ρ₁ ρ₂ : SchwartzMap ℝ ℝ) (hρ₁ : OperatorRidgelet.IsAdmissible α ρ₁)
  (hρ₂ : OperatorRidgelet.IsAdmissible α ρ₂)
  (f g : ↥(MeasureTheory.Lp ℂ 2 μ))
  (hf :
    f ∈
      OperatorRidgelet.spectralCore μ
        (OperatorRidgelet.gaussianMixture N α))
  (hg :
    g ∈
      OperatorRidgelet.spectralCore μ
        (OperatorRidgelet.gaussianMixture N α)) :
  ∫ (p : H × ℝ),
      OperatorRidgelet.ridgelet μ (⇑ρ₁) (↑↑f) p *
        (starRingEnd ℂ)
          (OperatorRidgelet.ridgelet μ (⇑ρ₂) (↑↑g)
            p) ∂OperatorRidgelet.parameterMeasure
        (OperatorRidgelet.gaussianMixture N α) =
    OperatorRidgelet.crossAdmissibilityConst α ⇑ρ₁ ⇑ρ₂ *
      OperatorRidgelet.spectralInner μ
        (OperatorRidgelet.gaussianMixture N α) ↑↑f ↑↑g

theorem OperatorRidgelet.Paper.thm_B_i_b.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {P Q : H →L[ℝ] H}
  (hP :
    OperatorRidgelet.IsTraceClassCovariance
      P)
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN :
    OperatorRidgelet.IsCenteredGaussianLayers
      P N)
  {α : ℝ} (hα : 0 < α)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (ρ₁ ρ₂ : SchwartzMap ℝ ℝ)
  (hρ₁ :
    OperatorRidgelet.IsAdmissible α ρ₁)
  (hρ₂ :
    OperatorRidgelet.IsAdmissible α ρ₂)
  (f g : ↥(MeasureTheory.Lp ℂ 2 μ))
  (hf :
    f ∈
      OperatorRidgelet.spectralCore μ
        (OperatorRidgelet.gaussianMixture
          N α))
  (hg :
    g ∈
      OperatorRidgelet.spectralCore μ
        (OperatorRidgelet.gaussianMixture
          N α)) :
  ∫ (p : H × ℝ),
      OperatorRidgelet.ridgelet μ (⇑ρ₁)
          (↑↑f) p *
        (starRingEnd ℂ)
          (OperatorRidgelet.ridgelet μ
            (⇑ρ₂) (↑↑g)
            p) ∂OperatorRidgelet.parameterMeasure
        (OperatorRidgelet.gaussianMixture
          N α) =
    OperatorRidgelet.crossAdmissibilityConst
        α ⇑ρ₁ ⇑ρ₂ *
      OperatorRidgelet.spectralInner μ
        (OperatorRidgelet.gaussianMixture
          N α)
        ↑↑f ↑↑g

**Theorem [thm:B]** Plancherel identity and injectivity.  The Plancherel identity
`⟨R_{ρ₁} f, R_{ρ₂} g⟩_{L²(λ_α)} = C^{(α)}_{ρ₁,ρ₂} ⟨f,g⟩_{𝓔_α}` for `f, g ∈ 𝒟_α`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.thm_B_ii_a.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H) {P Q : H →L[ℝ] H}
  (hP : OperatorRidgelet.IsTraceClassCovariance P)
  (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN : OperatorRidgelet.IsCenteredGaussianLayers P N) {α : ℝ}
  (hα : 0 < α) (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ) :
  ∃! R,
    ∀
      (f :
        ↥(OperatorRidgelet.spectralCore μ
            (OperatorRidgelet.gaussianMixture N α))),
      ↑↑(R
              (OperatorRidgelet.spectralEmbed μ
                (OperatorRidgelet.gaussianMixture N α)
                f)) =ᵐ[OperatorRidgelet.parameterMeasure
          (OperatorRidgelet.gaussianMixture N α)]
        OperatorRidgelet.ridgelet μ ⇑ρ ↑↑↑f

theorem OperatorRidgelet.Paper.thm_B_ii_a.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {P Q : H →L[ℝ] H}
  (hP :
    OperatorRidgelet.IsTraceClassCovariance
      P)
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN :
    OperatorRidgelet.IsCenteredGaussianLayers
      P N)
  {α : ℝ} (hα : 0 < α)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ :
    OperatorRidgelet.IsAdmissible α ρ) :
  ∃! R,
    ∀
      (f :
        ↥(OperatorRidgelet.spectralCore μ
            (OperatorRidgelet.gaussianMixture
              N α))),
      ↑↑(R
              (OperatorRidgelet.spectralEmbed
                μ
                (OperatorRidgelet.gaussianMixture
                  N α)
                f)) =ᵐ[OperatorRidgelet.parameterMeasure
          (OperatorRidgelet.gaussianMixture
            N α)]
        OperatorRidgelet.ridgelet μ ⇑ρ
          ↑↑↑f

**Theorem [thm:B]** Plancherel identity and injectivity.  An `α`-admissible `ρ` determines a
unique bounded extension `R_ρ : 𝓔_α → L²(λ_α)` of `f ↦ R_ρ f` from `𝒟_α`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.thm_B_ii_b.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H) {P Q : H →L[ℝ] H}
  (hP : OperatorRidgelet.IsTraceClassCovariance P)
  (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN : OperatorRidgelet.IsCenteredGaussianLayers P N) {α : ℝ}
  (hα : 0 < α) (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (R :
    ↥(OperatorRidgelet.spectralRange μ
          (OperatorRidgelet.gaussianMixture N α)) →L[ℂ]
      ↥(MeasureTheory.Lp ℂ 2
          (OperatorRidgelet.parameterMeasure
            (OperatorRidgelet.gaussianMixture N α))))
  (hR :
    ∀
      (f :
        ↥(OperatorRidgelet.spectralCore μ
            (OperatorRidgelet.gaussianMixture N α))),
      ↑↑(R
              (OperatorRidgelet.spectralEmbed μ
                (OperatorRidgelet.gaussianMixture N α)
                f)) =ᵐ[OperatorRidgelet.parameterMeasure
          (OperatorRidgelet.gaussianMixture N α)]
        OperatorRidgelet.ridgelet μ ⇑ρ ↑↑↑f)
  (G :
    ↥(OperatorRidgelet.spectralRange μ
        (OperatorRidgelet.gaussianMixture N α))) :
  ‖R G‖ ^ 2 = OperatorRidgelet.admissibilityConst α ⇑ρ * ‖G‖ ^ 2

theorem OperatorRidgelet.Paper.thm_B_ii_b.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {P Q : H →L[ℝ] H}
  (hP :
    OperatorRidgelet.IsTraceClassCovariance
      P)
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN :
    OperatorRidgelet.IsCenteredGaussianLayers
      P N)
  {α : ℝ} (hα : 0 < α)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (R :
    ↥(OperatorRidgelet.spectralRange μ
          (OperatorRidgelet.gaussianMixture
            N α)) →L[ℂ]
      ↥(MeasureTheory.Lp ℂ 2
          (OperatorRidgelet.parameterMeasure
            (OperatorRidgelet.gaussianMixture
              N α))))
  (hR :
    ∀
      (f :
        ↥(OperatorRidgelet.spectralCore μ
            (OperatorRidgelet.gaussianMixture
              N α))),
      ↑↑(R
              (OperatorRidgelet.spectralEmbed
                μ
                (OperatorRidgelet.gaussianMixture
                  N α)
                f)) =ᵐ[OperatorRidgelet.parameterMeasure
          (OperatorRidgelet.gaussianMixture
            N α)]
        OperatorRidgelet.ridgelet μ ⇑ρ
          ↑↑↑f)
  (G :
    ↥(OperatorRidgelet.spectralRange μ
        (OperatorRidgelet.gaussianMixture
          N α))) :
  ‖R G‖ ^ 2 =
    OperatorRidgelet.admissibilityConst α
        ⇑ρ *
      ‖G‖ ^ 2

**Theorem [thm:B]** Plancherel identity and injectivity.  The extension satisfies
`‖R_ρ f‖² = C^{(α)}_ρ ‖f‖²_{𝓔_α}`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.thm_B_ii_c.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H) {P Q : H →L[ℝ] H}
  (hP : OperatorRidgelet.IsTraceClassCovariance P)
  (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN : OperatorRidgelet.IsCenteredGaussianLayers P N) {α : ℝ}
  (hα : 0 < α) (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (R :
    ↥(OperatorRidgelet.spectralRange μ
          (OperatorRidgelet.gaussianMixture N α)) →L[ℂ]
      ↥(MeasureTheory.Lp ℂ 2
          (OperatorRidgelet.parameterMeasure
            (OperatorRidgelet.gaussianMixture N α))))
  (hR :
    ∀
      (f :
        ↥(OperatorRidgelet.spectralCore μ
            (OperatorRidgelet.gaussianMixture N α))),
      ↑↑(R
              (OperatorRidgelet.spectralEmbed μ
                (OperatorRidgelet.gaussianMixture N α)
                f)) =ᵐ[OperatorRidgelet.parameterMeasure
          (OperatorRidgelet.gaussianMixture N α)]
        OperatorRidgelet.ridgelet μ ⇑ρ ↑↑↑f) :
  IsClosed (Set.range ⇑R)

theorem OperatorRidgelet.Paper.thm_B_ii_c.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {P Q : H →L[ℝ] H}
  (hP :
    OperatorRidgelet.IsTraceClassCovariance
      P)
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN :
    OperatorRidgelet.IsCenteredGaussianLayers
      P N)
  {α : ℝ} (hα : 0 < α)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (R :
    ↥(OperatorRidgelet.spectralRange μ
          (OperatorRidgelet.gaussianMixture
            N α)) →L[ℂ]
      ↥(MeasureTheory.Lp ℂ 2
          (OperatorRidgelet.parameterMeasure
            (OperatorRidgelet.gaussianMixture
              N α))))
  (hR :
    ∀
      (f :
        ↥(OperatorRidgelet.spectralCore μ
            (OperatorRidgelet.gaussianMixture
              N α))),
      ↑↑(R
              (OperatorRidgelet.spectralEmbed
                μ
                (OperatorRidgelet.gaussianMixture
                  N α)
                f)) =ᵐ[OperatorRidgelet.parameterMeasure
          (OperatorRidgelet.gaussianMixture
            N α)]
        OperatorRidgelet.ridgelet μ ⇑ρ
          ↑↑↑f) :
  IsClosed (Set.range ⇑R)

**Theorem [thm:B]** Plancherel identity and injectivity.  The extension has closed range.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.thm_B_ii_d.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H) {P Q : H →L[ℝ] H}
  (hP : OperatorRidgelet.IsTraceClassCovariance P)
  (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN : OperatorRidgelet.IsCenteredGaussianLayers P N) {α : ℝ}
  (hα : 0 < α) (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (R :
    ↥(OperatorRidgelet.spectralRange μ
          (OperatorRidgelet.gaussianMixture N α)) →L[ℂ]
      ↥(MeasureTheory.Lp ℂ 2
          (OperatorRidgelet.parameterMeasure
            (OperatorRidgelet.gaussianMixture N α))))
  (hR :
    ∀
      (f :
        ↥(OperatorRidgelet.spectralCore μ
            (OperatorRidgelet.gaussianMixture N α))),
      ↑↑(R
              (OperatorRidgelet.spectralEmbed μ
                (OperatorRidgelet.gaussianMixture N α)
                f)) =ᵐ[OperatorRidgelet.parameterMeasure
          (OperatorRidgelet.gaussianMixture N α)]
        OperatorRidgelet.ridgelet μ ⇑ρ ↑↑↑f)
  (G :
    ↥(OperatorRidgelet.spectralRange μ
        (OperatorRidgelet.gaussianMixture N α))) :
  R G =
    OperatorRidgelet.spectralCoefficient
      (OperatorRidgelet.gaussianMixture N α) ⇑ρ ↑↑↑G

theorem OperatorRidgelet.Paper.thm_B_ii_d.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {P Q : H →L[ℝ] H}
  (hP :
    OperatorRidgelet.IsTraceClassCovariance
      P)
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN :
    OperatorRidgelet.IsCenteredGaussianLayers
      P N)
  {α : ℝ} (hα : 0 < α)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (R :
    ↥(OperatorRidgelet.spectralRange μ
          (OperatorRidgelet.gaussianMixture
            N α)) →L[ℂ]
      ↥(MeasureTheory.Lp ℂ 2
          (OperatorRidgelet.parameterMeasure
            (OperatorRidgelet.gaussianMixture
              N α))))
  (hR :
    ∀
      (f :
        ↥(OperatorRidgelet.spectralCore μ
            (OperatorRidgelet.gaussianMixture
              N α))),
      ↑↑(R
              (OperatorRidgelet.spectralEmbed
                μ
                (OperatorRidgelet.gaussianMixture
                  N α)
                f)) =ᵐ[OperatorRidgelet.parameterMeasure
          (OperatorRidgelet.gaussianMixture
            N α)]
        OperatorRidgelet.ridgelet μ ⇑ρ
          ↑↑↑f)
  (G :
    ↥(OperatorRidgelet.spectralRange μ
        (OperatorRidgelet.gaussianMixture
          N α))) :
  R G =
    OperatorRidgelet.spectralCoefficient
      (OperatorRidgelet.gaussianMixture N
        α)
      ⇑ρ ↑↑↑G

**Theorem [thm:B]** Plancherel identity and injectivity.  The extension factors as
`R_ρ = W_ρ U_α`: on `𝒦_α` it is the coefficient operator.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.thm_B_iii.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H) {P Q : H →L[ℝ] H}
  (hP : OperatorRidgelet.IsTraceClassCovariance P)
  (hQ : OperatorRidgelet.IsTraceClassCovariance Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN : OperatorRidgelet.IsCenteredGaussianLayers P N) {α : ℝ}
  (hα : 0 < α) (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ : OperatorRidgelet.IsCenteredGaussian Q μ) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ) (f : H → ℂ)
  (hf : MeasureTheory.Integrable f μ)
  (h :
    OperatorRidgelet.ridgelet μ (⇑ρ)
        f =ᵐ[OperatorRidgelet.parameterMeasure
        (OperatorRidgelet.gaussianMixture N α)]
      0) :
  f =ᵐ[μ] 0

theorem OperatorRidgelet.Paper.thm_B_iii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {P Q : H →L[ℝ] H}
  (hP :
    OperatorRidgelet.IsTraceClassCovariance
      P)
  (hQ :
    OperatorRidgelet.IsTraceClassCovariance
      Q)
  {N : ℝ → MeasureTheory.Measure H}
  (hN :
    OperatorRidgelet.IsCenteredGaussianLayers
      P N)
  {α : ℝ} (hα : 0 < α)
  (μ : MeasureTheory.Measure H)
  [MeasureTheory.IsProbabilityMeasure μ]
  (hμ :
    OperatorRidgelet.IsCenteredGaussian Q
      μ)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsAdmissible α ρ)
  (f : H → ℂ)
  (hf : MeasureTheory.Integrable f μ)
  (h :
    OperatorRidgelet.ridgelet μ (⇑ρ)
        f =ᵐ[OperatorRidgelet.parameterMeasure
        (OperatorRidgelet.gaussianMixture
          N α)]
      0) :
  f =ᵐ[μ] 0

**Theorem [thm:B]** Plancherel identity and injectivity.  Injectivity: if `ρ` is
`α`-admissible and `f ∈ L¹(μ_Q)`, then `R_ρ f = 0` `λ_α`-almost everywhere implies `f = 0`
`μ_Q`-almost everywhere.

Proof for Theorem 2.4.2

uses 0

Apply the one-dimensional Plancherel identity in the bias to the Fourier-slice identity and substitute \xi=-\omega a by homogeneity; admissibility gives square integrability and Cauchy–Schwarz justifies the cross identity. The norm identity extends R_\rho to the completion, an isometry up to a nonzero scalar has closed range, and R_\rho=W_\rho U_\alpha holds on the core and extends by continuity. For (iii), a fixed frequency with \widehat\rho\ne0 and homogeneity give \mathcal G_Qf=0 almost everywhere, and the argument of Lemma 2.3.2 finishes.