3.5. Plancherel identity, closed range, and injectivity🔗

Theorem3.14

Statement uses 3

Statement dependency previews

Preview

Definition 3.3

Loading preview

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

Used by 7

Reverse dependency previews

Preview

Definition Aux.6

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 F_Q. (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 Theorem3.14●7 theorems

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.thm_3_14_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_3_14_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:3.14]** 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_3_14_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_3_14_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:3.14]** 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_3_14_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_3_14_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:3.14]** 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_3_14_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_3_14_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:3.14]** Plancherel identity and injectivity.  The extension satisfies
`‖R_ρ f‖² = C^{(α)}_ρ ‖f‖²_{𝓔_α}`.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.thm_3_14_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_3_14_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:3.14]** Plancherel identity and injectivity.  The extension has closed range.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.thm_3_14_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_3_14_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:3.14]** Plancherel identity and injectivity.  The extension factors as
`R_ρ = W_ρ F_Q`: on `𝒦_α` it is the coefficient operator.

theoremdefined in OperatorRidgelet/Paper/Transform.lean

complete

theorem OperatorRidgelet.Paper.thm_3_14_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_3_14_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:3.14]** 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 3.14

Proof uses 4

Proof dependency previews

Preview

Lemma 3.2

Loading preview

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

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 F_Q holds on the core and extends by continuity. For (iii), a fixed frequency with \rho^\sharp\ne0 and homogeneity give F_Qf=0 almost everywhere, and the argument of Lemma 3.11 finishes.