Lean Ridgelet Blueprint

3. Unitary coordinates and their Fourier construction🔗

This chapter corresponds to the unitary coordinate transform in the arXiv source src/02theory.tex and its construction and proof in src/supp-proofs.tex. “Fourier--dilation” describes the construction; the operator's formal manuscript name is the unitary coordinate transform T.

Definition3.1
uses 0used by 1✓L∃∀N

For a Schwartz parameter distribution \gamma, construct the unitary coordinate transform by T[\gamma](x,\omega)=(2\pi)^{-m}\int_{\mathbb R^m\times\mathbb R}\gamma(a,b)e^{i\omega(a\cdot x-b)}\,da\,db. For every fixed x, this formula is bundled as a Schwartz element of the fiber core. The scalar kernel is jointly continuous in (x,\omega); continuity in the completed fiber norm is the remaining step needed for unconditional strong measurability. Once the resulting fiber-valued function is in Bochner L^2, it is bundled as the corresponding Hilbert-space coordinate.

Lean code for Definition3.1●5 declarations
  • defdefined in LeanRidgelet/Transform/FourierDilation.lean
    complete
    def LeanRidgelet.fourierDilationTransformCore {m : ℕ}
  (γ : SchwartzMap (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (x : LeanRidgelet.InputSpace m) (ω : ℝ) : ℂ
    def LeanRidgelet.fourierDilationTransformCore
  {m : ℕ}
  (γ :
    SchwartzMap
      (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (x : LeanRidgelet.InputSpace m)
  (ω : ℝ) : ℂ
    Implementation after :=
    :=
  ((2 * Real.pi : ℂ) ^ m)⁻¹ *
    ∫ p : InputSpace m × ℝ, γ p * fourierDilationKernel x ω p
    The Fourier construction of `T` on Schwartz parameter distributions, before Hilbert-space
extension.
  • theoremdefined in LeanRidgelet/Transform/FourierDilation.lean
    complete
    theorem LeanRidgelet.continuous_fourierDilationTransformCore {m : ℕ}
  (γ : SchwartzMap (LeanRidgelet.InputSpace m × ℝ) ℂ) :
  Continuous fun z ↦ LeanRidgelet.fourierDilationTransformCore γ z.1 z.2
    theorem LeanRidgelet.continuous_fourierDilationTransformCore
  {m : ℕ}
  (γ :
    SchwartzMap
      (LeanRidgelet.InputSpace m × ℝ) ℂ) :
  Continuous fun z ↦
    LeanRidgelet.fourierDilationTransformCore
      γ z.1 z.2
    The scalar Fourier--dilation core is jointly continuous in the input and dilation
frequency.  This supplies the scalar measurability part of the later fiber-valued strong
measurability argument.
  • theoremdefined in LeanRidgelet/Transform/FourierDilation.lean
    complete
    theorem LeanRidgelet.continuous_fourierDilationTransformCore_left {m : ℕ}
  (γ : SchwartzMap (LeanRidgelet.InputSpace m × ℝ) ℂ) (ω : ℝ) :
  Continuous fun x ↦ LeanRidgelet.fourierDilationTransformCore γ x ω
    theorem LeanRidgelet.continuous_fourierDilationTransformCore_left
  {m : ℕ}
  (γ :
    SchwartzMap
      (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (ω : ℝ) :
  Continuous fun x ↦
    LeanRidgelet.fourierDilationTransformCore
      γ x ω
    For each fixed frequency, the scalar Fourier--dilation core is continuous in the input.
  • defdefined in LeanRidgelet/Transform/FourierDilation.lean
    complete
    def LeanRidgelet.fourierDilationTransformFiberCore {m : ℕ} [NeZero m]
  (s t : ℝ) (γ : SchwartzMap (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (x : LeanRidgelet.InputSpace m) : LeanRidgelet.FiberCore m s t
    def LeanRidgelet.fourierDilationTransformFiberCore
  {m : ℕ} [NeZero m] (s t : ℝ)
  (γ :
    SchwartzMap
      (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (x : LeanRidgelet.InputSpace m) :
  LeanRidgelet.FiberCore m s t
    Implementation after :=
    :=
  ((2 * Real.pi : ℂ) ^ m)⁻¹ •
    SchwartzMap.compCLMOfAntilipschitz ℂ (by fun_prop)
      antilipschitzWith_paperFrequencyScale (parameterFourierRestriction γ x)
    The integral Fourier--dilation formula, bundled as an element of the Schwartz fiber core.
  • defdefined in LeanRidgelet/Transform/FourierDilation.lean
    complete
    def LeanRidgelet.fourierDilationTransformCoreL2 {m : ℕ} [NeZero m] (s t : ℝ)
  (γ : SchwartzMap (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (hγ :
    MeasureTheory.MemLp
      (LeanRidgelet.fourierDilationTransformFiber s t γ) 2
      MeasureTheory.volume) :
  ↥(LeanRidgelet.BochnerL2 (LeanRidgelet.InputSpace m)
      (LeanRidgelet.FiberSpace m s t) MeasureTheory.volume)
    def LeanRidgelet.fourierDilationTransformCoreL2
  {m : ℕ} [NeZero m] (s t : ℝ)
  (γ :
    SchwartzMap
      (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (hγ :
    MeasureTheory.MemLp
      (LeanRidgelet.fourierDilationTransformFiber
        s t γ)
      2 MeasureTheory.volume) :
  ↥(LeanRidgelet.BochnerL2
      (LeanRidgelet.InputSpace m)
      (LeanRidgelet.FiberSpace m s t)
      MeasureTheory.volume)
    Implementation after :=
    :=
  hγ.toLp (fourierDilationTransformFiber s t γ)
    Bundle the fiber-valued core formula as a Bochner `L²` coordinate once its analytic
membership has been established.
Definition3.2
uses 0used by 0✓L∃∀N

Define frequency dilation by D_\omega[x]=\omega x and the pullback coordinate by \kappa(x,\omega)=(-D_\omega[x],\omega).

Lean code for Definition3.2●2 definitions
  • defdefined in LeanRidgelet/Transform/FourierDilation.lean
    complete
    def LeanRidgelet.frequencyDilation {m : ℕ} (ω : ℝ)
  (x : LeanRidgelet.InputSpace m) : LeanRidgelet.InputSpace m
    def LeanRidgelet.frequencyDilation {m : ℕ}
  (ω : ℝ)
  (x : LeanRidgelet.InputSpace m) :
  LeanRidgelet.InputSpace m
    Implementation after :=
    :=
  ω • x
    The dilation `Dω[x] = ωx` on the input space.
  • defdefined in LeanRidgelet/Transform/FourierDilation.lean
    complete
    def LeanRidgelet.fourierDilationCoordinate {m : ℕ}
  (x : LeanRidgelet.InputSpace m) (ω : ℝ) :
  LeanRidgelet.InputSpace m × ℝ
    def LeanRidgelet.fourierDilationCoordinate
  {m : ℕ} (x : LeanRidgelet.InputSpace m)
  (ω : ℝ) : LeanRidgelet.InputSpace m × ℝ
    Implementation after :=
    :=
  (-frequencyDilation ω x, ω)
    The pullback coordinate map `κ(x,ω) = (-Dω[x],ω)`.
Lemma3.3
uses 0used by 0✓L∃∀N

Away from the null set \omega=0, the substitution y=\omega x gives a weighted integral identity with Jacobian |\omega|^m.

Lean code for Lemma3.3●2 theorems
  • theoremdefined in LeanRidgelet/Transform/FourierDilation.lean
    complete
    theorem LeanRidgelet.integral_fourierDilationCoordinate_mul {m : ℕ} [NeZero m]
  (f : LeanRidgelet.InputSpace m × ℝ → ℝ)
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hf_cont : Continuous f) :
  ∫ (z : LeanRidgelet.InputSpace m × ℝ), f z =
    ∫ (z : LeanRidgelet.InputSpace m × ℝ),
      f (LeanRidgelet.fourierDilationCoordinate z.1 z.2) * |z.2| ^ m
    theorem LeanRidgelet.integral_fourierDilationCoordinate_mul
  {m : ℕ} [NeZero m]
  (f : LeanRidgelet.InputSpace m × ℝ → ℝ)
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hf_cont : Continuous f) :
  ∫ (z : LeanRidgelet.InputSpace m × ℝ),
      f z =
    ∫ (z : LeanRidgelet.InputSpace m × ℝ),
      f
          (LeanRidgelet.fourierDilationCoordinate
            z.1 z.2) *
        |z.2| ^ m
    Weighted dilation change of variables in integral form. This is the identity obtained by
pushing `|ω|^m dx dω` forward along `(x, ω) ↦ (-ωx, ω)`. It does not require global
injectivity: the exceptional fiber `ω = 0` is null, and the remaining fibers use Haar-measure
scaling.
  • theoremdefined in LeanRidgelet/Transform/FourierDilation.lean
    complete
    theorem LeanRidgelet.integrable_fourierDilationCoordinate_mul {m : ℕ} [NeZero m]
  (f : LeanRidgelet.InputSpace m × ℝ → ℝ)
  (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (hf_cont : Continuous f) :
  MeasureTheory.Integrable
    (fun z ↦
      f (LeanRidgelet.fourierDilationCoordinate z.1 z.2) * |z.2| ^ m)
    MeasureTheory.volume
    theorem LeanRidgelet.integrable_fourierDilationCoordinate_mul
  {m : ℕ} [NeZero m]
  (f : LeanRidgelet.InputSpace m × ℝ → ℝ)
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (hf_cont : Continuous f) :
  MeasureTheory.Integrable
    (fun z ↦
      f
          (LeanRidgelet.fourierDilationCoordinate
            z.1 z.2) *
        |z.2| ^ m)
    MeasureTheory.volume
    Integrability of the weighted pullback appearing in the Fourier--dilation change of
variables. This is the integrability component used internally by
`integral_fourierDilationCoordinate_mul`, exposed for later Bochner `L²` arguments.
Theorem3.4
uses 0used by 0✓L∃∀N

Combining the paper-normalized Plancherel identity with the dilation change of variables yields, on the Schwartz core, \int |T[\gamma](x,\omega)|^2|\omega|^m\,dx\,d\omega=(2\pi)^{1-m}\|\gamma\|_{L^2}^2.

Lean code for Theorem3.4●2 theorems
  • theoremdefined in LeanRidgelet/Transform/FourierDilation.lean
    complete
    theorem LeanRidgelet.fourierDilationTransformCore_norm_sq {m : ℕ} [NeZero m]
  (γ : SchwartzMap (LeanRidgelet.InputSpace m × ℝ) ℂ) :
  ∫ (p : LeanRidgelet.InputSpace m × ℝ), ‖γ p‖ ^ 2 =
    (2 * Real.pi) ^ (m - 1) *
      ∫ (z : LeanRidgelet.InputSpace m × ℝ),
        ‖LeanRidgelet.fourierDilationTransformCore γ z.1 z.2‖ ^ 2 *
          |z.2| ^ m
    theorem LeanRidgelet.fourierDilationTransformCore_norm_sq
  {m : ℕ} [NeZero m]
  (γ :
    SchwartzMap
      (LeanRidgelet.InputSpace m × ℝ) ℂ) :
  ∫ (p : LeanRidgelet.InputSpace m × ℝ),
      ‖γ p‖ ^ 2 =
    (2 * Real.pi) ^ (m - 1) *
      ∫ (z :
        LeanRidgelet.InputSpace m × ℝ),
        ‖LeanRidgelet.fourierDilationTransformCore
                γ z.1 z.2‖ ^
            2 *
          |z.2| ^ m
    Plancherel plus the dilation Jacobian for the unitary-coordinate formula on the Schwartz
core.
  • theoremdefined in LeanRidgelet/Transform/FourierDilation.lean
    complete
    theorem LeanRidgelet.integral_fiberBaseNormSq_fourierDilationTransformFiberCore
  {m : ℕ} [NeZero m] (s t : ℝ)
  (γ : SchwartzMap (LeanRidgelet.InputSpace m × ℝ) ℂ) :
  ∫ (x : LeanRidgelet.InputSpace m),
      LeanRidgelet.fiberBaseNormSq m
        (LeanRidgelet.fourierDilationTransformFiberCore s t γ x) =
    ∫ (p : LeanRidgelet.InputSpace m × ℝ), ‖γ p‖ ^ 2
    theorem LeanRidgelet.integral_fiberBaseNormSq_fourierDilationTransformFiberCore
  {m : ℕ} [NeZero m] (s t : ℝ)
  (γ :
    SchwartzMap
      (LeanRidgelet.InputSpace m × ℝ) ℂ) :
  ∫ (x : LeanRidgelet.InputSpace m),
      LeanRidgelet.fiberBaseNormSq m
        (LeanRidgelet.fourierDilationTransformFiberCore
          s t γ x) =
    ∫ (p : LeanRidgelet.InputSpace m × ℝ),
      ‖γ p‖ ^ 2
Definition3.5
uses 0used by 1✓L∃∀N

On the transported coordinate model, the unitary coordinate transform T is a linear isometric equivalence from \mathcal G_{s,t} to L^2(\mathbb R^m;\mathcal H_{s,t}). For the concrete core formula, the base part of the fiber norm is already integrable; after strong measurability, Bochner L^2 membership is equivalent to integrability of the remaining Sobolev term.

Lean code for Definition3.5●3 declarations
  • defdefined in LeanRidgelet/Transform/FourierDilation.lean
    complete
    def LeanRidgelet.fourierDilationTransform (m : ℕ) [NeZero m] (s t : ℝ) :
  ↥(LeanRidgelet.ParameterSpace m s t) ≃ₗᵢ[ℂ]
    ↥(LeanRidgelet.BochnerL2 (LeanRidgelet.InputSpace m)
        (LeanRidgelet.FiberSpace m s t) MeasureTheory.volume)
    def LeanRidgelet.fourierDilationTransform
  (m : ℕ) [NeZero m] (s t : ℝ) :
  ↥(LeanRidgelet.ParameterSpace m s
        t) ≃ₗᵢ[ℂ]
    ↥(LeanRidgelet.BochnerL2
        (LeanRidgelet.InputSpace m)
        (LeanRidgelet.FiberSpace m s t)
        MeasureTheory.volume)
    Implementation after :=
    :=
  parameterCoordinateEquiv m s t
    The unitary coordinate transform `T` in the transported coordinate model.
  • defdefined in LeanRidgelet/Transform/FourierDilation.lean
    complete
    def LeanRidgelet.fourierDilationCompatibilityDomain {m : ℕ} [NeZero m]
  (s t : ℝ) : Set (SchwartzMap (LeanRidgelet.InputSpace m × ℝ) ℂ)
    def LeanRidgelet.fourierDilationCompatibilityDomain
  {m : ℕ} [NeZero m] (s t : ℝ) :
  Set
    (SchwartzMap
      (LeanRidgelet.InputSpace m × ℝ) ℂ)
    Implementation after :=
    :=
  {γ | AEStronglyMeasurable (fourierDilationTransformFiber s t γ) volume ∧
    Integrable (fun x : InputSpace m =>
      fiberSobolevNormSq s t (fourierDilationTransformFiberCore s t γ x))}
    The manuscript compatibility domain `S^T_{s,t}(Θ)` for Schwartz parameter data.

The two clauses keep the analytic responsibilities visible: strong measurability of the
completion-valued core and integrability of its Sobolev graph term.  This is a set predicate,
not a structure carrying unproved analytic assumptions.
  • theoremdefined in LeanRidgelet/Transform/FourierDilation.lean
    complete
    theorem LeanRidgelet.mem_fourierDilationCompatibilityDomain_iff_memLp {m : ℕ}
  [NeZero m] (s t : ℝ)
  (γ : SchwartzMap (LeanRidgelet.InputSpace m × ℝ) ℂ) :
  γ ∈ LeanRidgelet.fourierDilationCompatibilityDomain s t ↔
    MeasureTheory.MemLp
      (LeanRidgelet.fourierDilationTransformFiber s t γ) 2
      MeasureTheory.volume
    theorem LeanRidgelet.mem_fourierDilationCompatibilityDomain_iff_memLp
  {m : ℕ} [NeZero m] (s t : ℝ)
  (γ :
    SchwartzMap
      (LeanRidgelet.InputSpace m × ℝ) ℂ) :
  γ ∈
      LeanRidgelet.fourierDilationCompatibilityDomain
        s t ↔
    MeasureTheory.MemLp
      (LeanRidgelet.fourierDilationTransformFiber
        s t γ)
      2 MeasureTheory.volume
    Membership in the concrete compatibility domain is exactly Bochner `L²` membership of the
Fourier--dilation core.  The base part is automatically integrable, so only measurability and the
Sobolev graph term remain in the set definition.
Definition3.6
uses 0used by 0✓L∃∀N

For a Schwartz coordinate test function u, define the inverse-transform Fourier expression by T^{-1}[u](a,b)=\frac1{2\pi}\int u(x,\omega)e^{-i\omega(a\cdot x-b)}|\omega|^m\,dx\,d\omega.

Lean code for Definition3.6●1 definition
  • defdefined in LeanRidgelet/Transform/FourierDilation.lean
    complete
    def LeanRidgelet.inverseFourierDilationTransformCore {m : ℕ}
  (u : SchwartzMap (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (p : LeanRidgelet.InputSpace m × ℝ) : ℂ
    def LeanRidgelet.inverseFourierDilationTransformCore
  {m : ℕ}
  (u :
    SchwartzMap
      (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (p : LeanRidgelet.InputSpace m × ℝ) : ℂ
    Implementation after :=
    :=
  (2 * Real.pi : ℂ)⁻¹ *
    ∫ z : InputSpace m × ℝ, u z * inverseFourierDilationKernel p z
    The Fourier expression for the inverse coordinate transform on a Schwartz test function.
Theorem3.7
uses 0used by 0✓L∃∀N

On Hilbert-space coordinates, T^*=T^{-1} and T^{-1}\circ T=I.

Lean code for Theorem3.7●1 theorem
  • theoremdefined in LeanRidgelet/Transform/FourierDilation.lean
    complete
    theorem LeanRidgelet.inverseFourierDilationTransform_apply_fourierDilationTransform
  (m : ℕ) [NeZero m] (s t : ℝ)
  (γ : ↥(LeanRidgelet.ParameterSpace m s t)) :
  (LeanRidgelet.inverseFourierDilationTransform m s t)
      ((LeanRidgelet.fourierDilationTransform m s t) γ) =
    γ
    theorem LeanRidgelet.inverseFourierDilationTransform_apply_fourierDilationTransform
  (m : ℕ) [NeZero m] (s t : ℝ)
  (γ :
    ↥(LeanRidgelet.ParameterSpace m s
        t)) :
  (LeanRidgelet.inverseFourierDilationTransform
        m s t)
      ((LeanRidgelet.fourierDilationTransform
          m s t)
        γ) =
    γ
Theorem3.8
Statement uses 2
Statement dependency previews
Preview
Definition 3.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

If the fiber-valued integral formula associated with a parameter Schwartz function belongs to Bochner L^2, its inverse-unitary realization is mapped back to that concrete core coordinate. Thus the integral representation agrees with the transported unitary on its natural domain.

Lean code for Theorem3.8●2 theorems
  • theoremdefined in LeanRidgelet/Transform/FourierDilation.lean
    complete
    theorem LeanRidgelet.fourierDilationTransform_parameterSchwartzRealization
  {m : ℕ} [NeZero m] (s t : ℝ)
  (γ : SchwartzMap (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (hγ :
    MeasureTheory.MemLp
      (LeanRidgelet.fourierDilationTransformFiber s t γ) 2
      MeasureTheory.volume) :
  (LeanRidgelet.fourierDilationTransform m s t)
      (LeanRidgelet.parameterSchwartzRealization s t γ hγ) =
    LeanRidgelet.fourierDilationTransformCoreL2 s t γ hγ
    theorem LeanRidgelet.fourierDilationTransform_parameterSchwartzRealization
  {m : ℕ} [NeZero m] (s t : ℝ)
  (γ :
    SchwartzMap
      (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (hγ :
    MeasureTheory.MemLp
      (LeanRidgelet.fourierDilationTransformFiber
        s t γ)
      2 MeasureTheory.volume) :
  (LeanRidgelet.fourierDilationTransform m
        s t)
      (LeanRidgelet.parameterSchwartzRealization
        s t γ hγ) =
    LeanRidgelet.fourierDilationTransformCoreL2
      s t γ hγ
    Compatibility of the concrete core formula with the transported unitary model.
  • theoremdefined in LeanRidgelet/Transform/FourierDilation.lean
    complete
    theorem LeanRidgelet.fourierDilationTransform_parameterSchwartzRealization_apply_ae
  {m : ℕ} [NeZero m] (s t : ℝ)
  (γ : SchwartzMap (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (hγ :
    MeasureTheory.MemLp
      (LeanRidgelet.fourierDilationTransformFiber s t γ) 2
      MeasureTheory.volume) :
  ↑↑((LeanRidgelet.fourierDilationTransform m s t)
          (LeanRidgelet.parameterSchwartzRealization s t γ
            hγ)) =ᵐ[MeasureTheory.volume]
    LeanRidgelet.fourierDilationTransformFiber s t γ
    theorem LeanRidgelet.fourierDilationTransform_parameterSchwartzRealization_apply_ae
  {m : ℕ} [NeZero m] (s t : ℝ)
  (γ :
    SchwartzMap
      (LeanRidgelet.InputSpace m × ℝ) ℂ)
  (hγ :
    MeasureTheory.MemLp
      (LeanRidgelet.fourierDilationTransformFiber
        s t γ)
      2 MeasureTheory.volume) :
  ↑↑((LeanRidgelet.fourierDilationTransform
            m s t)
          (LeanRidgelet.parameterSchwartzRealization
            s t γ
            hγ)) =ᵐ[MeasureTheory.volume]
    LeanRidgelet.fourierDilationTransformFiber
      s t γ