Infinite-dimensional operator ridgelet transform

4.1. Spectral targets and coefficient estimates🔗

Lemma4.1
uses 1
Used by 2
Reverse dependency previews
Preview
Theorem 4.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Let \nu be a Borel measure on H, let Y be a separable complex Hilbert space, and let G\in L^1(\nu;Y). Then g_G(x)=\int_H e^{i\langle x,\xi\rangle}G(\xi)\,\nu(\mathrm d\xi) belongs to C_b(H;Y), satisfies \|g_G\|_\infty\le\|G\|_{L^1(\nu;Y)}, and determines G up to \nu-almost-everywhere equality. No input weight, filter, homogeneity, or full-support assumption is needed.

Lean code for Lemma4.1●3 theorems
  • theoremdefined in OperatorRidgelet/Paper/Revision.lean
    complete
    theorem OperatorRidgelet.Paper.lem_4_1_i.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  (ν : MeasureTheory.Measure H) (G : H → Y)
  (_hG : MeasureTheory.Integrable G ν) (x : H) :
  ‖OperatorRidgelet.spectralTarget ν G x‖ ≤ ∫ (ξ : H), ‖G ξ‖ ∂ν
    theorem OperatorRidgelet.Paper.lem_4_1_i.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  (ν : MeasureTheory.Measure H)
  (G : H → Y)
  (_hG : MeasureTheory.Integrable G ν)
  (x : H) :
  ‖OperatorRidgelet.spectralTarget ν G
        x‖ ≤
    ∫ (ξ : H), ‖G ξ‖ ∂ν
    **Lemma [lem:4.1]** The spectral target has the uniform L¹ norm bound.
  • theoremdefined in OperatorRidgelet/Paper/Revision.lean
    complete
    theorem OperatorRidgelet.Paper.lem_4_1_ii.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] (ν : MeasureTheory.Measure H) (G : H → Y)
  (hG : MeasureTheory.Integrable G ν) :
  Continuous (OperatorRidgelet.spectralTarget ν G)
    theorem OperatorRidgelet.Paper.lem_4_1_ii.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  (ν : MeasureTheory.Measure H)
  (G : H → Y)
  (hG : MeasureTheory.Integrable G ν) :
  Continuous
    (OperatorRidgelet.spectralTarget ν G)
    **Lemma [lem:4.1]** An integrable spectral density has a continuous target.
  • theoremdefined in OperatorRidgelet/Paper/Revision.lean
    complete
    theorem OperatorRidgelet.Paper.lem_4_1_iii.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℂ Y]
  [CompleteSpace Y] [SecondCountableTopology Y]
  (ν : MeasureTheory.Measure H) (G : H → Y)
  (hG : MeasureTheory.Integrable G ν)
  (hzero : OperatorRidgelet.spectralTarget ν G = 0) : G =ᵐ[ν] 0
    theorem OperatorRidgelet.Paper.lem_4_1_iii.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (ν : MeasureTheory.Measure H)
  (G : H → Y)
  (hG : MeasureTheory.Integrable G ν)
  (hzero :
    OperatorRidgelet.spectralTarget ν G =
      0) :
  G =ᵐ[ν] 0
    **Lemma [lem:4.1]** A spectral density is determined by its target.
Proof for Lemma 4.1
uses 0

The integral triangle inequality gives the norm bound, and dominated convergence with majorant \|G(\xi)\|_Y gives continuity. If g_G=0, pair the finite vector measure G\nu with vectors in a countable dense subset of Y. Fourier uniqueness makes each resulting scalar measure zero: finite-dimensional Fourier uniqueness determines all cylinder sets, which generate the Borel sigma-algebra of H. Intersect the countably many full-measure sets and use continuity of the pairing to obtain G=0 almost everywhere. Apply the argument to a difference for uniqueness.

Definition4.2
Statement uses 3
Statement dependency previews
Preview
Definition Aux.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 7
Reverse dependency previews
Preview
Lemma 4.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Fix a symmetric compact set I\subset\mathbb R\setminus\{0\} containing \operatorname{supp}\rho^\sharp (a frequency window). Write G_a(\omega):=G(\omega a), the restriction to the line through the origin spanned by a\ne0, with G_0 constant. A bounded Borel G:H\to\mathbb C is regular along rays if every G_a is C^\infty on a neighbourhood of I and M_m(G)=\int_H(1+\|a\|)^{m+2}\max_{k\le m}\sup_{\omega\in I}|\partial_\omega^kG(\omega a)|\,\nu_\alpha(\mathrm da)<\infty for every integer m\ge0. Such a G belongs to L^1(\nu_\alpha)\cap L^2(\nu_\alpha) (the theorem part of the definition).

Lean code for Definition4.2●6 declarations
  • structure(4 fields)defined in OperatorRidgelet/Reconstruction/Defs.lean
    complete
    structure OperatorRidgelet.IsFrequencyWindow (ρ : ℝ → ℝ) (I : Set ℝ) : Prop
    structure OperatorRidgelet.IsFrequencyWindow
  (ρ : ℝ → ℝ) (I : Set ℝ) : Prop
    The frequency window fixed before Definition `def:4.2`: a symmetric compact set
`I ⊆ ℝ ∖ {0}` containing the support of `ρ♯`.

    Fields

    isCompact : IsCompact I
    `I` is compact. 
    zero_notMem : 0 ∉ I
    `I` stays away from the origin. 
    neg_mem : ∀ ω ∈ I, -ω ∈ I
    `I` is symmetric. 
    tsupport_subset : tsupport (OperatorRidgelet.filterFourier ρ) ⊆ I
    `I` contains the support of `ρ♯`.
  • defdefined in OperatorRidgelet/Reconstruction/Defs.lean
    complete
    def OperatorRidgelet.rayDerivBound.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y] (I : Set ℝ) (G : H → Y)
  (m : ℕ) (a : H) : ENNReal
    def OperatorRidgelet.rayDerivBound.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  (I : Set ℝ) (G : H → Y) (m : ℕ)
  (a : H) : ENNReal
    The derivative bound `max_{k ≤ m} sup_{ω ∈ I} ‖∂_ω^k G_a(ω)‖`, with
`G_a(ω) := G (ω • a)`, in `ℝ≥0∞`.
  • defdefined in OperatorRidgelet/Reconstruction/Defs.lean
    complete
    def OperatorRidgelet.rayMoment.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  (ν : MeasureTheory.Measure H) (I : Set ℝ) (G : H → Y) (m : ℕ) :
  ENNReal
    def OperatorRidgelet.rayMoment.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  (ν : MeasureTheory.Measure H)
  (I : Set ℝ) (G : H → Y) (m : ℕ) :
  ENNReal
    The weighted derivative integral
`M_m(G) = ∫ (1+‖a‖)^{m+2} max_{k ≤ m} sup_{ω ∈ I} ‖∂_ω^k G(ωa)‖ ν(da)`
(`eq:ray-regularity`), in `ℝ≥0∞`.
  • structure(4 fields)defined in OperatorRidgelet/Reconstruction/Defs.lean
    complete
    structure OperatorRidgelet.IsRegularAlongRays.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  (ν : MeasureTheory.Measure H) (I : Set ℝ) (G : H → Y) : Prop
    structure OperatorRidgelet.IsRegularAlongRays.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  (ν : MeasureTheory.Measure H)
  (I : Set ℝ) (G : H → Y) : Prop
    **Definition [def:4.2]** A bounded Borel density `G` is regular along rays (with
respect to the direction measure `ν` and the frequency window `I`) if for every direction `a`
the restriction `G_a(ω) := G (ω • a)` to the line through the origin is `C^∞` on a
neighbourhood of `I` and every weighted derivative integral `M_m(G)` is finite.
The case `a = 0` gives the constant function `G 0`.

    Fields

    stronglyMeasurable : MeasureTheory.StronglyMeasurable G
    `G` is Borel. 
    bounded : ∃ M, ∀ (ξ : H), ‖G ξ‖ ≤ M
    `G` is bounded. 
    contDiffOn : ∀ (a : H), ∃ U, IsOpen U ∧ I ⊆ U ∧ ContDiffOn ℝ (↑⊤) (fun ω => G (ω • a)) U
    `ω ↦ G(ωa)` is `C^∞` on an open neighbourhood of `I`, for every direction `a`. 
    rayMoment_lt_top : ∀ (m : ℕ), OperatorRidgelet.rayMoment ν I G m < ⊤
    `M_m(G) < ∞` for every `m`.
  • defdefined in OperatorRidgelet/Reconstruction/Defs.lean
    complete
    def OperatorRidgelet.spectralTarget.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  (ν : MeasureTheory.Measure H) (G : H → Y) (x : H) : Y
    def OperatorRidgelet.spectralTarget.{u_1, u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] {Y : Type u_2}
  [NormedAddCommGroup Y] [NormedSpace ℂ Y]
  (ν : MeasureTheory.Measure H)
  (G : H → Y) (x : H) : Y
    The target with spectral density `G` with respect to `ν`,
`g_G(x) = ∫ e^{i⟪x,ξ⟫} G(ξ) ν(dξ)` (`eq:spectral-target`), the Fourier transform of the finite
measure `G ν`; for a scalar density `•` is the product.
  • theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean
    complete
    theorem OperatorRidgelet.Paper.def_4_2.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H) [MeasureTheory.SigmaFinite ν] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsBandPass ρ) (I : Set ℝ)
  (hI : OperatorRidgelet.IsFrequencyWindow (⇑ρ) I) (G : H → ℂ)
  (hG : OperatorRidgelet.IsRegularAlongRays ν I G) :
  MeasureTheory.Integrable G ν ∧ MeasureTheory.MemLp G 2 ν
    theorem OperatorRidgelet.Paper.def_4_2.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (I : Set ℝ)
  (hI :
    OperatorRidgelet.IsFrequencyWindow
      (⇑ρ) I)
  (G : H → ℂ)
  (hG :
    OperatorRidgelet.IsRegularAlongRays ν
      I G) :
  MeasureTheory.Integrable G ν ∧
    MeasureTheory.MemLp G 2 ν
    **Definition [def:4.2]** Regularity along rays.  A density that is regular along
rays belongs to `L¹(ν_α) ∩ L²(ν_α)` (homogeneity with a fixed `ω ∈ I`).
Lemma4.3
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 3
Reverse dependency previews
Preview
Theorem 4.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Fix a band-pass \rho, a symmetric compact frequency window I away from zero, and an integer r\ge0. Let Y be a separable complex Hilbert space and let G:H\to Y be bounded and Borel, with \omega\mapsto G(\omega a) of class C^{r+2} near I for every a. Write D_m(a)=\max_{k\le m}\sup_{\omega\in I}\|\partial_\omega^kG(\omega a)\|_Y and A_{m,r}(G)=\int_H(1+\|a\|)^rD_m(a)\,\nu_\alpha(\mathrm da). If A_{r+2,r}(G)<\infty, then G\in L^1(\nu_\alpha;Y)\cap L^2(\nu_\alpha;Y), and the inverse Fourier integral is a jointly measurable representative \gamma_G of W_\rho G. Moreover, (1+|c|)^{r+2}\|\gamma_G(a,c)\|_Y\le C_{\rho,I,r}D_{r+2}(a) and \int_{H\times\mathbb R}(1+\|a\|+|c|)^r\|\gamma_G(a,c)\|_Y\,\mathrm d\lambda_\alpha\le c_{\rho,I,r}A_{r+2,r}(G). The constants do not depend on G or the dimension of Y.

Lean code for Lemma4.3●5 theorems
  • theoremdefined in OperatorRidgelet/Paper/Revision.lean
    complete
    theorem OperatorRidgelet.Paper.lem_4_3_i.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] (ν : MeasureTheory.Measure H) {α : ℝ}
  (hν : OperatorRidgelet.IsHomogeneous α ν) (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (I : Set ℝ)
  (hI : OperatorRidgelet.IsFrequencyWindow (⇑ρ) I) (G : H → Y)
  (hG : MeasureTheory.StronglyMeasurable G)
  (hbound : ∃ M, ∀ (ξ : H), ‖G ξ‖ ≤ M) (r : ℕ)
  (hM : OperatorRidgelet.finiteRayMoment ν I G (r + 2) r < ⊤) :
  MeasureTheory.Integrable G ν ∧ MeasureTheory.MemLp G 2 ν
    theorem OperatorRidgelet.Paper.lem_4_3_i.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  (ν : MeasureTheory.Measure H) {α : ℝ}
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (I : Set ℝ)
  (hI :
    OperatorRidgelet.IsFrequencyWindow
      (⇑ρ) I)
  (G : H → Y)
  (hG :
    MeasureTheory.StronglyMeasurable G)
  (hbound : ∃ M, ∀ (ξ : H), ‖G ξ‖ ≤ M)
  (r : ℕ)
  (hM :
    OperatorRidgelet.finiteRayMoment ν I G
        (r + 2) r <
      ⊤) :
  MeasureTheory.Integrable G ν ∧
    MeasureTheory.MemLp G 2 ν
    **Lemma [lem:4.3]** A bounded density with a finite ray moment is L¹∩L².
  • theoremdefined in OperatorRidgelet/Paper/Revision.lean
    complete
    theorem OperatorRidgelet.Paper.lem_4_3_ii.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] [CompleteSpace Y] [SecondCountableTopology Y]
  (ν : MeasureTheory.Measure H) [MeasureTheory.SigmaFinite ν] {α : ℝ}
  (hα : 0 < α) (hν : OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ) (hρ : OperatorRidgelet.IsBandPass ρ) (I : Set ℝ)
  (hI : OperatorRidgelet.IsFrequencyWindow (⇑ρ) I) (G : H → Y)
  (hG : MeasureTheory.StronglyMeasurable G)
  (hbound : ∃ M, ∀ (ξ : H), ‖G ξ‖ ≤ M) (r : ℕ)
  (hM : OperatorRidgelet.finiteRayMoment ν I G (r + 2) r < ⊤) :
  MeasureTheory.StronglyMeasurable
      (OperatorRidgelet.coefficientFormulaVec (⇑ρ) G) ∧
    ↑↑(OperatorRidgelet.spectralCoefficientVec ν (⇑ρ)
            G) =ᵐ[OperatorRidgelet.parameterMeasure ν]
      OperatorRidgelet.coefficientFormulaVec (⇑ρ) G
    theorem OperatorRidgelet.Paper.lem_4_3_ii.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  [CompleteSpace Y]
  [SecondCountableTopology Y]
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν] {α : ℝ}
  (hα : 0 < α)
  (hν :
    OperatorRidgelet.IsHomogeneous α ν)
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (I : Set ℝ)
  (hI :
    OperatorRidgelet.IsFrequencyWindow
      (⇑ρ) I)
  (G : H → Y)
  (hG :
    MeasureTheory.StronglyMeasurable G)
  (hbound : ∃ M, ∀ (ξ : H), ‖G ξ‖ ≤ M)
  (r : ℕ)
  (hM :
    OperatorRidgelet.finiteRayMoment ν I G
        (r + 2) r <
      ⊤) :
  MeasureTheory.StronglyMeasurable
      (OperatorRidgelet.coefficientFormulaVec
        (⇑ρ) G) ∧
    ↑↑(OperatorRidgelet.spectralCoefficientVec
            ν (⇑ρ)
            G) =ᵐ[OperatorRidgelet.parameterMeasure
        ν]
      OperatorRidgelet.coefficientFormulaVec
        (⇑ρ) G
    **Lemma [lem:4.3]** The inverse integral represents the coefficient.
  • theoremdefined in OperatorRidgelet/Paper/Revision.lean
    complete
    theorem OperatorRidgelet.Paper.lem_4_3_iii.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y] [InnerProductSpace ℂ Y] (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (I : Set ℝ)
  (hI : OperatorRidgelet.IsFrequencyWindow (⇑ρ) I) (r : ℕ) :
  0 < OperatorRidgelet.finiteCoefficientDecayConstant ρ (r + 2) ∧
    OperatorRidgelet.finiteCoefficientDecayConstant ρ (r + 2) < ⊤ ∧
      ∀ (G : H → Y),
        (∀ (a : H),
            ∃ U,
              IsOpen U ∧
                I ⊆ U ∧
                  ContDiffOn ℝ (↑(r + 2)) (fun ω => G (ω • a)) U) →
          ∀ (a : H) (c : ℝ),
            ENNReal.ofReal ((1 + |c|) ^ (r + 2)) *
                ‖OperatorRidgelet.coefficientFormulaVec (⇑ρ) G
                    (a, c)‖ₑ ≤
              OperatorRidgelet.finiteCoefficientDecayConstant ρ
                  (r + 2) *
                OperatorRidgelet.rayDerivBound I G (r + 2) a
    theorem OperatorRidgelet.Paper.lem_4_3_iii.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H] {Y : Type u_2}
  [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (I : Set ℝ)
  (hI :
    OperatorRidgelet.IsFrequencyWindow
      (⇑ρ) I)
  (r : ℕ) :
  0 <
      OperatorRidgelet.finiteCoefficientDecayConstant
        ρ (r + 2) ∧
    OperatorRidgelet.finiteCoefficientDecayConstant
          ρ (r + 2) <
        ⊤ ∧
      ∀ (G : H → Y),
        (∀ (a : H),
            ∃ U,
              IsOpen U ∧
                I ⊆ U ∧
                  ContDiffOn ℝ (↑(r + 2))
                    (fun ω => G (ω • a))
                    U) →
          ∀ (a : H) (c : ℝ),
            ENNReal.ofReal
                  ((1 + |c|) ^ (r + 2)) *
                ‖OperatorRidgelet.coefficientFormulaVec
                    (⇑ρ) G (a, c)‖ₑ ≤
              OperatorRidgelet.finiteCoefficientDecayConstant
                  ρ (r + 2) *
                OperatorRidgelet.rayDerivBound
                  I G (r + 2) a
    **Lemma [lem:4.3]** Finitely many ray derivatives give pointwise decay.
  • theoremdefined in OperatorRidgelet/Paper/Revision.lean
    complete
    theorem OperatorRidgelet.Paper.lem_4_3_iv.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν] (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (I : Set ℝ)
  (hI : OperatorRidgelet.IsFrequencyWindow (⇑ρ) I) (r : ℕ) :
  OperatorRidgelet.finiteCoefficientMomentConstant ρ r ≠ ⊤ ∧
    ∀ (G : H → Y),
      MeasureTheory.StronglyMeasurable G →
        (∀ (a : H),
            ∃ U,
              IsOpen U ∧
                I ⊆ U ∧
                  ContDiffOn ℝ (↑(r + 2)) (fun ω => G (ω • a)) U) →
          ∫⁻ (θ : H × ℝ),
              ENNReal.ofReal ((1 + ‖θ.1‖ + |θ.2|) ^ r) *
                ‖OperatorRidgelet.coefficientFormulaVec (⇑ρ) G
                    θ‖ₑ ∂OperatorRidgelet.parameterMeasure ν ≤
            OperatorRidgelet.finiteCoefficientMomentConstant ρ r *
              OperatorRidgelet.finiteRayMoment ν I G (r + 2) r
    theorem OperatorRidgelet.Paper.lem_4_3_iv.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (I : Set ℝ)
  (hI :
    OperatorRidgelet.IsFrequencyWindow
      (⇑ρ) I)
  (r : ℕ) :
  OperatorRidgelet.finiteCoefficientMomentConstant
        ρ r ≠
      ⊤ ∧
    ∀ (G : H → Y),
      MeasureTheory.StronglyMeasurable G →
        (∀ (a : H),
            ∃ U,
              IsOpen U ∧
                I ⊆ U ∧
                  ContDiffOn ℝ (↑(r + 2))
                    (fun ω => G (ω • a))
                    U) →
          ∫⁻ (θ : H × ℝ),
              ENNReal.ofReal
                  ((1 + ‖θ.1‖ + |θ.2|) ^
                    r) *
                ‖OperatorRidgelet.coefficientFormulaVec
                    (⇑ρ) G
                    θ‖ₑ ∂OperatorRidgelet.parameterMeasure
                ν ≤
            OperatorRidgelet.finiteCoefficientMomentConstant
                ρ r *
              OperatorRidgelet.finiteRayMoment
                ν I G (r + 2) r
    **Lemma [lem:4.3]** The parameter moment is bounded by A_{r+2,r}.
  • theoremdefined in OperatorRidgelet/Paper/Revision.lean
    complete
    theorem OperatorRidgelet.Paper.lem_4_3_v.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [MeasurableSpace H]
  [BorelSpace H] {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y] (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν] (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ) (I : Set ℝ)
  (hI : OperatorRidgelet.IsFrequencyWindow (⇑ρ) I) (G : H → Y)
  (hG : MeasureTheory.StronglyMeasurable G) (r : ℕ)
  (hGs :
    ∀ (a : H),
      ∃ U,
        IsOpen U ∧
          I ⊆ U ∧ ContDiffOn ℝ (↑(r + 2)) (fun ω => G (ω • a)) U)
  (hM : OperatorRidgelet.finiteRayMoment ν I G (r + 2) r < ⊤) :
  MeasureTheory.Integrable
    (fun θ =>
      (1 + ‖θ.1‖ + |θ.2|) ^ r *
        ‖OperatorRidgelet.coefficientFormulaVec (⇑ρ) G θ‖)
    (OperatorRidgelet.parameterMeasure ν)
    theorem OperatorRidgelet.Paper.lem_4_3_v.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [MeasurableSpace H] [BorelSpace H]
  {Y : Type u_2} [NormedAddCommGroup Y]
  [InnerProductSpace ℂ Y]
  (ν : MeasureTheory.Measure H)
  [MeasureTheory.SigmaFinite ν]
  (ρ : SchwartzMap ℝ ℝ)
  (hρ : OperatorRidgelet.IsBandPass ρ)
  (I : Set ℝ)
  (hI :
    OperatorRidgelet.IsFrequencyWindow
      (⇑ρ) I)
  (G : H → Y)
  (hG :
    MeasureTheory.StronglyMeasurable G)
  (r : ℕ)
  (hGs :
    ∀ (a : H),
      ∃ U,
        IsOpen U ∧
          I ⊆ U ∧
            ContDiffOn ℝ (↑(r + 2))
              (fun ω => G (ω • a)) U)
  (hM :
    OperatorRidgelet.finiteRayMoment ν I G
        (r + 2) r <
      ⊤) :
  MeasureTheory.Integrable
    (fun θ =>
      (1 + ‖θ.1‖ + |θ.2|) ^ r *
        ‖OperatorRidgelet.coefficientFormulaVec
            (⇑ρ) G θ‖)
    (OperatorRidgelet.parameterMeasure ν)
    **Lemma [lem:4.3]** Finite ray data imply a finite parameter moment.
Proof for Lemma 4.3
Proof uses 2
Proof dependency previews
Preview
Lemma 3.2
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

Difference quotients and countable dense subsets of I give measurability of D_m. Homogeneity at one fixed nonzero frequency gives G\in L^1; boundedness gives G\in L^2. Set m=r+2 and h_a(\omega)=\rho^\sharp(\omega)G(-\omega a). Leibniz' rule bounds \|h_a\|_1+\|h_a^{(m)}\|_1 by a filter-dependent constant times D_m(a). The function h_a is compactly supported and C^m; the derivatives of the filter vanish at its support boundary. Bound the inverse Fourier integral directly for |c|\le1, and integrate by parts m times for |c|>1. This proves the decay estimate. Finally use 1+\|a\|+|c|\le(1+\|a\|)(1+|c|) and \int_{\mathbb R}(1+|c|)^{-2}\,\mathrm dc=2 to obtain the moment bound by Tonelli. No synthesis identity enters this argument.

Lemma4.4
uses 1
Used by 3
Reverse dependency previews
Preview
Theorem 6.8
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

The following functions satisfy Definition 4.2 for every band-pass \rho. (a) G(\xi)=q(\xi)e^{-\kappa(\xi)/2}, where \kappa(\xi)=\langle S\xi,\xi\rangle, S is bounded and positive, S\ge\theta Q for some \theta>0, and q is a polynomial in \kappa and finitely many bounded linear functionals \ell_i satisfying |\ell_i(\xi)|^2\le C_i\kappa(\xi) for every \xi. Equivalently, \ell_i=\langle S^{1/2}v_i,\cdot\rangle for some v_i\in H. A polynomial in \kappa alone requires no further condition. (b) G(\xi)=\varphi(\|\xi-\xi_0\|^2) for \varphi\in C_c^\infty(\mathbb R); more generally, bounded densities with bounded support, smooth restrictions G_a(\omega)=G(\omega a) near I, and \sup_{\omega\in I}|\partial_\omega^kG(\omega a)|\le C_k(1+\|a\|)^{p_k} for every k. (c) Finite linear combinations, and Bochner integrals G=\int_\Omega G_y\,m(\mathrm dy) of uniformly bounded measurable families over a finite measure, subject to these neighbourhood bounds: there is an open U\supset I where every function \omega\mapsto G_y(\omega a) is smooth, and finite-valued Borel h_k:H\to[0,\infty) such that \sup_{\omega\in U}|\partial_\omega^kG_y(\omega a)|\le h_k(a) for every y,a,k, and \int_H(1+\|a\|)^{m+2}\max_{k\le m}h_k(a)\,\nu_\alpha(\mathrm da)<\infty for every m. The bounds hold on the open neighbourhood and for every direction.

Lean code for Lemma4.4●5 theorems
  • theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean
    complete
    theorem OperatorRidgelet.Paper.lem_4_4_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 < α) (S : H →L[ℝ] H) (hS : IsSelfAdjoint S) {θ : ℝ}
  (hθ : 0 < θ) (hSQ : ∀ (ξ : H), θ * inner ℝ (Q ξ) ξ ≤ inner ℝ (S ξ) ξ)
  {k : ℕ} (ℓ : Fin k → H →L[ℝ] ℝ)
  (hℓ :
    ∀ (i : Fin k), ∃ C, ∀ (ξ : H), (ℓ i) ξ ^ 2 ≤ C * inner ℝ (S ξ) ξ)
  (q : MvPolynomial (Option (Fin k)) ℂ) (ρ : SchwartzMap ℝ ℝ) :
  OperatorRidgelet.IsBandPass ρ →
    ∀ (I : Set ℝ),
      OperatorRidgelet.IsFrequencyWindow (⇑ρ) I →
        OperatorRidgelet.IsRegularAlongRays
          (OperatorRidgelet.gaussianMixture N α) I fun ξ =>
          (MvPolynomial.eval fun o =>
                o.elim ↑(inner ℝ (S ξ) ξ) fun i => ↑((ℓ i) ξ))
              q *
            Complex.exp (-↑(inner ℝ (S ξ) ξ / 2))
    theorem OperatorRidgelet.Paper.lem_4_4_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 < α) (S : H →L[ℝ] H)
  (hS : IsSelfAdjoint S) {θ : ℝ}
  (hθ : 0 < θ)
  (hSQ :
    ∀ (ξ : H),
      θ * inner ℝ (Q ξ) ξ ≤
        inner ℝ (S ξ) ξ)
  {k : ℕ} (ℓ : Fin k → H →L[ℝ] ℝ)
  (hℓ :
    ∀ (i : Fin k),
      ∃ C,
        ∀ (ξ : H),
          (ℓ i) ξ ^ 2 ≤
            C * inner ℝ (S ξ) ξ)
  (q : MvPolynomial (Option (Fin k)) ℂ)
  (ρ : SchwartzMap ℝ ℝ) :
  OperatorRidgelet.IsBandPass ρ →
    ∀ (I : Set ℝ),
      OperatorRidgelet.IsFrequencyWindow
          (⇑ρ) I →
        OperatorRidgelet.IsRegularAlongRays
          (OperatorRidgelet.gaussianMixture
            N α)
          I fun ξ =>
          (MvPolynomial.eval fun o =>
                o.elim ↑(inner ℝ (S ξ) ξ)
                  fun i => ↑((ℓ i) ξ))
              q *
            Complex.exp
              (-↑(inner ℝ (S ξ) ξ / 2))
    **Lemma [lem:4.4]** Densities that are regular along rays.  Gaussian-type
densities `G(ξ) = q(ξ) e^{-κ(ξ)/2}`, `κ(ξ) = ⟨Sξ,ξ⟩` with `S` a bounded positive operator with
`S ≥ θQ`, `θ > 0`, and `q` a polynomial in `κ(ξ)` and in finitely many bounded linear
functionals `ℓ_i` of `ξ` dominated by the quadratic form, `|ℓ_i(ξ)|² ≤ C_i κ(ξ)`, are regular
along rays for every band-pass `ρ` (and every frequency window of `ρ`).
  • theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean
    complete
    theorem OperatorRidgelet.Paper.lem_4_4_b_i.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H) {P : H →L[ℝ] H}
  (hP : OperatorRidgelet.IsTraceClassCovariance P)
  {N : ℝ → MeasureTheory.Measure H}
  (hN : OperatorRidgelet.IsCenteredGaussianLayers P N) {α : ℝ}
  (hα : 0 < α) (ξ₀ : H) (φ : ℝ → ℂ) (hφ : ContDiff ℝ (↑⊤) φ)
  (hφc : HasCompactSupport φ) (ρ : SchwartzMap ℝ ℝ) :
  OperatorRidgelet.IsBandPass ρ →
    ∀ (I : Set ℝ),
      OperatorRidgelet.IsFrequencyWindow (⇑ρ) I →
        OperatorRidgelet.IsRegularAlongRays
          (OperatorRidgelet.gaussianMixture N α) I fun ξ =>
          φ (‖ξ - ξ₀‖ ^ 2)
    theorem OperatorRidgelet.Paper.lem_4_4_b_i.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {P : H →L[ℝ] H}
  (hP :
    OperatorRidgelet.IsTraceClassCovariance
      P)
  {N : ℝ → MeasureTheory.Measure H}
  (hN :
    OperatorRidgelet.IsCenteredGaussianLayers
      P N)
  {α : ℝ} (hα : 0 < α) (ξ₀ : H)
  (φ : ℝ → ℂ) (hφ : ContDiff ℝ (↑⊤) φ)
  (hφc : HasCompactSupport φ)
  (ρ : SchwartzMap ℝ ℝ) :
  OperatorRidgelet.IsBandPass ρ →
    ∀ (I : Set ℝ),
      OperatorRidgelet.IsFrequencyWindow
          (⇑ρ) I →
        OperatorRidgelet.IsRegularAlongRays
          (OperatorRidgelet.gaussianMixture
            N α)
          I fun ξ => φ (‖ξ - ξ₀‖ ^ 2)
    **Lemma [lem:4.4]** Densities that are regular along rays.  Radial bumps
`G(ξ) = φ(‖ξ - ξ₀‖²)` with `φ ∈ C_c^∞(ℝ)` are regular along rays for every band-pass `ρ`.
  • theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean
    complete
    theorem OperatorRidgelet.Paper.lem_4_4_b_ii.{u_1} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H) {P : H →L[ℝ] H}
  (hP : OperatorRidgelet.IsTraceClassCovariance P)
  {N : ℝ → MeasureTheory.Measure H}
  (hN : OperatorRidgelet.IsCenteredGaussianLayers P N) {α : ℝ}
  (hα : 0 < α) (G : H → ℂ) (hG : Measurable G)
  (hGb : ∃ M, ∀ (ξ : H), ‖G ξ‖ ≤ M)
  (hG0 : ∃ R₀, ∀ (ξ : H), R₀ < ‖ξ‖ → G ξ = 0) (ρ : SchwartzMap ℝ ℝ) :
  OperatorRidgelet.IsBandPass ρ →
    ∀ (I : Set ℝ),
      OperatorRidgelet.IsFrequencyWindow (⇑ρ) I →
        (∀ (a : H),
            ∃ U,
              IsOpen U ∧
                I ⊆ U ∧ ContDiffOn ℝ (↑⊤) (fun ω => G (ω • a)) U) →
          (∀ (k : ℕ),
              ∃ C p,
                ∀ (a : H),
                  ∀ ω ∈ I,
                    ‖iteratedDeriv k (fun ω => G (ω • a)) ω‖ ≤
                      C * (1 + ‖a‖) ^ p) →
            OperatorRidgelet.IsRegularAlongRays
              (OperatorRidgelet.gaussianMixture N α) I G
    theorem OperatorRidgelet.Paper.lem_4_4_b_ii.{u_1}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (hH : ¬FiniteDimensional ℝ H)
  {P : H →L[ℝ] H}
  (hP :
    OperatorRidgelet.IsTraceClassCovariance
      P)
  {N : ℝ → MeasureTheory.Measure H}
  (hN :
    OperatorRidgelet.IsCenteredGaussianLayers
      P N)
  {α : ℝ} (hα : 0 < α) (G : H → ℂ)
  (hG : Measurable G)
  (hGb : ∃ M, ∀ (ξ : H), ‖G ξ‖ ≤ M)
  (hG0 :
    ∃ R₀, ∀ (ξ : H), R₀ < ‖ξ‖ → G ξ = 0)
  (ρ : SchwartzMap ℝ ℝ) :
  OperatorRidgelet.IsBandPass ρ →
    ∀ (I : Set ℝ),
      OperatorRidgelet.IsFrequencyWindow
          (⇑ρ) I →
        (∀ (a : H),
            ∃ U,
              IsOpen U ∧
                I ⊆ U ∧
                  ContDiffOn ℝ (↑⊤)
                    (fun ω => G (ω • a))
                    U) →
          (∀ (k : ℕ),
              ∃ C p,
                ∀ (a : H),
                  ∀ ω ∈ I,
                    ‖iteratedDeriv k
                          (fun ω =>
                            G (ω • a))
                          ω‖ ≤
                      C * (1 + ‖a‖) ^ p) →
            OperatorRidgelet.IsRegularAlongRays
              (OperatorRidgelet.gaussianMixture
                N α)
              I G
    **Lemma [lem:4.4]** Densities that are regular along rays.  More generally,
a bounded Borel `G` that is `C^∞` along rays (on a neighbourhood of the frequency window),
vanishes outside a bounded set, and satisfies `sup_{ω ∈ I} |∂_ω^k G(ωa)| ≤ C_k (1+‖a‖)^{p_k}`
for all `k`, is regular along rays for every band-pass `ρ`.
  • theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean
    complete
    theorem OperatorRidgelet.Paper.lem_4_4_c_i.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H) (I : Set ℝ) {ι : Type u_2}
  (s : Finset ι) (c : ι → ℂ) (G : ι → H → ℂ)
  (hG : ∀ i ∈ s, OperatorRidgelet.IsRegularAlongRays ν I (G i)) :
  OperatorRidgelet.IsRegularAlongRays ν I fun ξ => ∑ i ∈ s, c i * G i ξ
    theorem OperatorRidgelet.Paper.lem_4_4_c_i.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H)
  (I : Set ℝ) {ι : Type u_2}
  (s : Finset ι) (c : ι → ℂ)
  (G : ι → H → ℂ)
  (hG :
    ∀ i ∈ s,
      OperatorRidgelet.IsRegularAlongRays
        ν I (G i)) :
  OperatorRidgelet.IsRegularAlongRays ν I
    fun ξ => ∑ i ∈ s, c i * G i ξ
    **Lemma [lem:4.4]** Densities that are regular along rays.  Finite linear
combinations of densities that are regular along rays are regular along rays.
  • theoremdefined in OperatorRidgelet/Paper/Reconstruction.lean
    complete
    theorem OperatorRidgelet.Paper.lem_4_4_c_ii.{u_1, u_2} {H : Type u_1}
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
  [SecondCountableTopology H] [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H) (I : Set ℝ) {Ω : Type u_2}
  [MeasurableSpace Ω] (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m] (G : Ω → H → ℂ)
  (hGm : Measurable (Function.uncurry G))
  (hG : ∀ (y : Ω), OperatorRidgelet.IsRegularAlongRays ν I (G y))
  (hGb : ∃ M, ∀ (y : Ω) (ξ : H), ‖G y ξ‖ ≤ M) (U : Set ℝ)
  (hU : IsOpen U) (hIU : I ⊆ U)
  (hsmooth :
    ∀ (y : Ω) (a : H), ContDiffOn ℝ (↑⊤) (fun ω => G y (ω • a)) U)
  (hunif :
    ∀ (k : ℕ),
      ∃ h,
        ∫⁻ (a : H), ENNReal.ofReal ((1 + ‖a‖) ^ (k + 2)) * ↑(h a) ∂ν <
            ⊤ ∧
          ∀ (y : Ω) (a : H),
            OperatorRidgelet.rayDerivBound U (G y) k a ≤ ↑(h a)) :
  OperatorRidgelet.IsRegularAlongRays ν I fun ξ => ∫ (y : Ω), G y ξ ∂m
    theorem OperatorRidgelet.Paper.lem_4_4_c_ii.{u_1,
    u_2}
  {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℝ H]
  [CompleteSpace H]
  [SecondCountableTopology H]
  [MeasurableSpace H] [BorelSpace H]
  (ν : MeasureTheory.Measure H)
  (I : Set ℝ) {Ω : Type u_2}
  [MeasurableSpace Ω]
  (m : MeasureTheory.Measure Ω)
  [MeasureTheory.IsFiniteMeasure m]
  (G : Ω → H → ℂ)
  (hGm : Measurable (Function.uncurry G))
  (hG :
    ∀ (y : Ω),
      OperatorRidgelet.IsRegularAlongRays
        ν I (G y))
  (hGb :
    ∃ M, ∀ (y : Ω) (ξ : H), ‖G y ξ‖ ≤ M)
  (U : Set ℝ) (hU : IsOpen U)
  (hIU : I ⊆ U)
  (hsmooth :
    ∀ (y : Ω) (a : H),
      ContDiffOn ℝ (↑⊤)
        (fun ω => G y (ω • a)) U)
  (hunif :
    ∀ (k : ℕ),
      ∃ h,
        ∫⁻ (a : H),
              ENNReal.ofReal
                  ((1 + ‖a‖) ^ (k + 2)) *
                ↑(h a) ∂ν <
            ⊤ ∧
          ∀ (y : Ω) (a : H),
            OperatorRidgelet.rayDerivBound
                U (G y) k a ≤
              ↑(h a)) :
  OperatorRidgelet.IsRegularAlongRays ν I
    fun ξ => ∫ (y : Ω), G y ξ ∂m
    **Lemma [lem:4.4]** Densities that are regular along rays.  Bochner
integrals `∫ G_y m(dy)` of a measurable family of densities that are regular along rays, over
a finite measure `m`, are regular along rays when the densities are uniformly bounded and the
weights of `eq:ray-regularity` have a `ν_α`-integrable majorant that is uniform in `y`.
Proof for Lemma 4.4
Proof uses 2
Proof dependency previews
Preview
Lemma 3.2
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

For (a), domination of the linear functionals gives |q(\xi)|\le C(1+\kappa(\xi))^p, so G is bounded. Derivatives of G_a(\omega)=G(\omega a) with respect to \omega are polynomials times e^{-\omega^2\kappa(a)/2}; on I\subset\{r\le|\omega|\le R\} their bound is C_k(1+\|a\|)^{p_k}e^{-r^2\theta\langle Qa,a\rangle/2}. Apply Lemma 3.12. For (b), derivatives vanish outside a bounded set of directions, on which \nu_\alpha is finite. For (c), the finite neighbourhood bounds justify differentiation under the Bochner integral for each direction. The triangle inequality and Tonelli give M_m(G)\le m(\Omega)\int_H(1+\|a\|)^{m+2}\max_{k\le m}h_k(a)\,\nu_\alpha(\mathrm da)<\infty.