Airy equation and Kato smoothing

DefinitionFourier solution of the Airy equation#✓fully proved

For \(u_0 : \mathbb{R} \to \mathbb{C}\), let \(\widehat{u_0}(\xi) = (2\pi)^{-1/2} \int_{\mathbb{R}} u_0(y) e^{-iy\xi}\,dy\) be its unitary Fourier transform. The Airy solution with initial datum \(u_0\) is the function \(u : \mathbb{R}^2 \to \mathbb{C}\) given by

\[u(t, x) = (2\pi)^{-1/2} \int_{\mathbb{R}} e^{i(t\xi^3 + x\xi)}\, \widehat{u_0}(\xi)\,d\xi,\]

where an integral whose integrand is not integrable is taken to be \(0\).

For \(u_0 \in C_c^\infty(\mathbb{R})\) this function solves the Airy equation \(\partial_t u + \partial_x^3 u = 0\) with \(u(0, \cdot) = u_0\).

noncomputable def AirySolution (u0 : ℝ → ℂ) (t x : ℝ) : ℂ :=
  (Real.sqrt (2 * Real.pi))⁻¹ *
    ∫ ξ : ℝ,
      Complex.exp (Complex.I * (t * ξ ^ (3 : ℕ) + x * ξ)) *
        ((Real.sqrt (2 * Real.pi))⁻¹ * (𝓕 u0) (ξ / (2 * Real.pi)))

Used by 1

Used byKato smoothing identity for the Airy equation

TheoremKato smoothing identity for the Airy equation#●ready to prove

For \(u_0 : \mathbb{R} \to \mathbb{C}\) let \(\widehat{u_0}(\xi) = (2\pi)^{-1/2} \int_{\mathbb{R}} u_0(y) e^{-iy\xi}\,dy\) be its unitary Fourier transform, and let \(u(t, x) = (2\pi)^{-1/2} \int_{\mathbb{R}} e^{i(t\xi^3 + x\xi)}\, \widehat{u_0}(\xi)\,d\xi\) be the Airy solution with initial datum \(u_0\). There is a constant \(c_0 > 0\) such that for every smooth compactly supported \(u_0 : \mathbb{R} \to \mathbb{C}\) and every \(x_0 \in \mathbb{R}\), the function \(t \mapsto \partial_x u(t, x_0)\) belongs to \(L^2(\mathbb{R})\) and

\[\int_{\mathbb{R}} |\partial_x u(t, x_0)|^2\,dt = c_0 \int_{\mathbb{R}} |u_0(x)|^2\,dx.\]

The source's formalization used the transform \(\int u_0(y) e^{-2\pi i y\xi}\,dy\) together with the unitary phase and prefactor, so its initial datum was not \(u_0\) but the \(L^2\)-isometric rescaling \(x \mapsto (2\pi)^{-1/2} u_0(x / 2\pi)\); the identity holds for both with the same \(c_0\).

public theorem_wanted exists_pos_const_integral_norm_deriv_airySolution_sq_eq :
  ∃ c0 : ℝ, 0 < c0 ∧
    ∀ (u0 : ℝ → ℂ),
      ContDiff ℝ (⊤ : ℕ∞) u0 →
      HasCompactSupport u0 →
      (∀ x0 : ℝ,
          MemLp (fun t : ℝ => deriv (fun x : ℝ => AirySolution u0 t x) x0)
            (2 : ENNReal) volume) ∧
        ∀ x0 : ℝ,
          ∫ t : ℝ, ‖deriv (fun x : ℝ => AirySolution u0 t x) x0‖ ^ (2 : ℕ) =
            c0 * ∫ x : ℝ, ‖u0 x‖ ^ (2 : ℕ)

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Functional analysis; Distributions, generalized functions, distribution spaces), problem ma_proofbench_l2_27, with the change above.

Uses 1

Statement usesFourier solution of the Airy equation

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.