Documentation

CsdLean4.Mathlib.Analysis.Fourier.PartialFourierDeriv

The derivatives of the partial Fourier transform are partial Fourier transforms #

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #171 (out of #121(ii), brick 2 of 5: the partial Fourier transform on 𝓒(ℝ Γ— ℝ, β„‚)).

For a Schwartz kernel K on the plane and a direction h = (h₁, hβ‚‚),

βˆ‚_h 𝓕₂K = 𝓕₂(Dop h K), Dop h K = h₁ Β· βˆ‚_u K + hβ‚‚ Β· (βˆ’2Ο€i w) Β· K,

and Dop h is a continuous linear map of 𝓒(ℝ Γ— ℝ, β„‚) to itself (Mathlib's lineDerivOpCLM along (1, 0) and smulLeftCLM of the temperate-growth function w ↦ βˆ’2Ο€i w). So the identity iterates: the n-th derivative of 𝓕₂K evaluated on directions v₁, …, vβ‚™ is 𝓕₂ of K with the n operators Dop vα΅’ applied β€” a partial Fourier transform of a Schwartz function, never a derivative of one. This is what lets #173 bound a derivative of 𝓕₂K by an integral.

First order is #124's β˜…β˜… fderiv_integral_apply_of_bound on #170's integrand, with #170's bound family at orders 0 and 1; the pointwise derivative of the integrand is the product rule, the phase contributing βˆ’2Ο€i w hβ‚‚ and the kernel its u-derivative. The iteration is iteratedFDeriv_apply_succ_last (#124), which peels the last direction as the innermost derivative.

Honest scope #

References: PartialFourierSmooth.lean (#170), ContDiffParametricIntegralFDeriv.lean (#124, fderiv_integral_apply_of_bound, iteratedFDeriv_apply_succ_last), SchwartzPartialIntegral.lean (#126(ii), the measurability lemmas); Mathlib Analysis/Distribution/SchwartzSpace/Basic.lean (smulLeftCLM) and Deriv.lean (lineDerivOpCLM); specs/BACKLOG.md #171, #121.

The first-order operator #

source
noncomputable def SchwartzMap.wMul (q : ℝ Γ— ℝ) :
β„‚

The multiplier (u, w) ↦ βˆ’2Ο€i w.

Equations
Instances For
    source
    theorem SchwartzMap.wMul_eq_clm :
    wMul = ⇑(-(2 * ↑Real.pi * Complex.I) β€’ Complex.ofRealCLM ∘SL ContinuousLinearMap.snd ℝ ℝ ℝ)
    source
    theorem SchwartzMap.hasTemperateGrowth_wMul :
    Function.HasTemperateGrowth wMul
    source
    theorem SchwartzMap.lineDerivOpCLM_apply_eq_fderiv (m : ℝ Γ— ℝ) (K : SchwartzMap (ℝ Γ— ℝ) β„‚) (q : ℝ Γ— ℝ) :
    ((LineDeriv.lineDerivOpCLM β„‚ (SchwartzMap (ℝ Γ— ℝ) β„‚) m) K) q = (fderiv ℝ (⇑K) q) m

    The directional derivative CLM of Schwartz space, evaluated.

    source
    noncomputable def SchwartzMap.Dop (h : ℝ Γ— ℝ) :
    SchwartzMap (ℝ Γ— ℝ) β„‚ β†’L[β„‚] SchwartzMap (ℝ Γ— ℝ) β„‚

    The first-order operator Dop h K = h₁ Β· βˆ‚_u K + hβ‚‚ Β· (βˆ’2Ο€i w) Β· K, a continuous linear map of Schwartz space to itself.

    Equations
    Instances For
      source
      theorem SchwartzMap.Dop_apply (h : ℝ Γ— ℝ) (K : SchwartzMap (ℝ Γ— ℝ) β„‚) (q : ℝ Γ— ℝ) :
      ((Dop h) K) q = ↑h.1 * (fderiv ℝ (⇑K) q) (1, 0) + ↑h.2 * (wMul q * K q)
      source
      theorem SchwartzMap.Dop_add (h₁ hβ‚‚ : ℝ Γ— ℝ) :
      Dop (h₁ + hβ‚‚) = Dop h₁ + Dop hβ‚‚
      source
      theorem SchwartzMap.Dop_smul (c : ℝ) (h : ℝ Γ— ℝ) :
      Dop (c β€’ h) = ↑c β€’ Dop h
      source
      theorem SchwartzMap.Dop_fst :
      Dop (1, 0) = LineDeriv.lineDerivOpCLM β„‚ (SchwartzMap (ℝ Γ— ℝ) β„‚) (1, 0)
      source
      theorem SchwartzMap.Dop_snd :
      Dop (0, 1) = smulLeftCLM β„‚ wMul

      The pointwise derivative of the integrand #

      source
      theorem SchwartzMap.fderiv_partialFourierIntegrand_apply (K : SchwartzMap (ℝ Γ— ℝ) β„‚) (w : ℝ) (p h : ℝ Γ— ℝ) :
      (fderiv ℝ (fun (y : ℝ Γ— ℝ) => K.partialFourierIntegrand (y, w)) p) h = ((Dop h) K).partialFourierIntegrand (p, w)

      β˜… The derivative of the integrand in the parameter is the integrand of Dop h K.

      Integrability and linearity in the kernel #

      source
      theorem SchwartzMap.integrable_partialFourierIntegrand (K : SchwartzMap (ℝ Γ— ℝ) β„‚) (p : ℝ Γ— ℝ) :
      MeasureTheory.Integrable (fun (w : ℝ) => K.partialFourierIntegrand (p, w)) MeasureTheory.volume
      source
      theorem SchwartzMap.partialFourier_add (K₁ Kβ‚‚ : SchwartzMap (ℝ Γ— ℝ) β„‚) :
      (K₁ + Kβ‚‚).partialFourier = K₁.partialFourier + Kβ‚‚.partialFourier
      source
      theorem SchwartzMap.partialFourier_smul (c : β„‚) (K : SchwartzMap (ℝ Γ— ℝ) β„‚) :
      (c β€’ K).partialFourier = c β€’ K.partialFourier

      The first derivative #

      source
      theorem SchwartzMap.norm_partialFourierIntegrand_le (K : SchwartzMap (ℝ Γ— ℝ) β„‚) (p : ℝ Γ— ℝ) (w : ℝ) :
      β€–K.partialFourierIntegrand (p, w)β€– ≀ leibnizConst 0 * K.kSup 0 * (1 + w ^ 2)⁻¹

      The bound family of #170 at order 0, in the form #124's first-order identity takes.

      source
      theorem SchwartzMap.norm_fderiv_partialFourierIntegrand_le (K : SchwartzMap (ℝ Γ— ℝ) β„‚) (p : ℝ Γ— ℝ) (w : ℝ) :
      β€–fderiv ℝ (fun (y : ℝ Γ— ℝ) => K.partialFourierIntegrand (y, w)) pβ€– ≀ leibnizConst 1 * K.kSup 1 * (1 + w ^ 2)⁻¹

      And at order 1.

      source
      theorem SchwartzMap.fderiv_partialFourier_apply (K : SchwartzMap (ℝ Γ— ℝ) β„‚) (p h : ℝ Γ— ℝ) :
      (fderiv ℝ K.partialFourier p) h = ((Dop h) K).partialFourier p

      β˜…β˜… The derivative of the partial Fourier transform in a direction is the partial Fourier transform of Dop h K: βˆ‚_h 𝓕₂K(p) = 𝓕₂(Dop h K)(p).

      source
      theorem SchwartzMap.fderiv_partialFourier_fst (K : SchwartzMap (ℝ Γ— ℝ) β„‚) (p : ℝ Γ— ℝ) :
      (fderiv ℝ K.partialFourier p) (1, 0) = ((LineDeriv.lineDerivOpCLM β„‚ (SchwartzMap (ℝ Γ— ℝ) β„‚) (1, 0)) K).partialFourier p

      βˆ‚_u 𝓕₂K = 𝓕₂(βˆ‚_u K).

      source
      theorem SchwartzMap.fderiv_partialFourier_snd (K : SchwartzMap (ℝ Γ— ℝ) β„‚) (p : ℝ Γ— ℝ) :
      (fderiv ℝ K.partialFourier p) (0, 1) = ((smulLeftCLM β„‚ wMul) K).partialFourier p

      βˆ‚_ΞΎ 𝓕₂K = 𝓕₂((βˆ’2Ο€i w) K).

      source
      theorem SchwartzMap.hasFDerivAt_partialFourier (K : SchwartzMap (ℝ Γ— ℝ) β„‚) (p : ℝ Γ— ℝ) :
      HasFDerivAt K.partialFourier ((ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight (((LineDeriv.lineDerivOpCLM β„‚ (SchwartzMap (ℝ Γ— ℝ) β„‚) (1, 0)) K).partialFourier p) + (ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight (((smulLeftCLM β„‚ wMul) K).partialFourier p)) p

      β˜… The derivative as a continuous linear map in the direction.

      All orders #

      source
      noncomputable def SchwartzMap.dopFin (n : β„•) :
      (Fin n β†’ ℝ Γ— ℝ) β†’ SchwartzMap (ℝ Γ— ℝ) β„‚ β†’L[β„‚] SchwartzMap (ℝ Γ— ℝ) β„‚

      The composite of Dop along a tuple of directions, the last direction applied first β€” the order iteratedFDeriv_apply_succ_last peels them in.

      Equations
      Instances For
        source
        @[simp]
        theorem SchwartzMap.dopFin_zero (v : Fin 0 β†’ ℝ Γ— ℝ) :
        dopFin 0 v = ContinuousLinearMap.id β„‚ (SchwartzMap (ℝ Γ— ℝ) β„‚)
        source
        theorem SchwartzMap.dopFin_succ (n : β„•) (v : Fin (n + 1) β†’ ℝ Γ— ℝ) :
        dopFin (n + 1) v = dopFin n (Fin.init v) ∘SL Dop (v (Fin.last n))
        source
        theorem SchwartzMap.iteratedFDeriv_partialFourier_apply (n : β„•) (K : SchwartzMap (ℝ Γ— ℝ) β„‚) (p : ℝ Γ— ℝ) (v : Fin n β†’ ℝ Γ— ℝ) :
        (iteratedFDeriv ℝ n K.partialFourier p) v = ((dopFin n v) K).partialFourier p

        β˜…β˜… Every iterated derivative of the partial Fourier transform is a partial Fourier transform: βˆ‚βΏ 𝓕₂K(p)(v₁, …, vβ‚™) = 𝓕₂(dopFin v K)(p).