Fourier–Plancherel in L²

This file sets up the statements needed to extend the explicit Fourier integral to an isometry on L²(ℝ). The key intermediate results (still left as goals) are:

• the Fourier integral of an L¹ ∩ L² function belongs to L²;
• the Plancherel identity relating the L² norms on the time and frequency sides with the 1 / (2π) normalisation used in Frourio.Analysis.FourierPlancherel.

instance Frourio.fact_one_le_two_ennreal : Fact (1 ≤ 2)

instance Frourio.volume_hasTemperateGrowth : MeasureTheory.volume.HasTemperateGrowth

theorem Frourio.smooth_compactly_supported_dense_L2 (f_L2 : ℝ → ℂ) (hf : MeasureTheory.MemLp f_L2 2 MeasureTheory.volume) (ε : ℝ) (hε_pos : ε > 0) : ∃ (g : ℝ → ℂ), HasCompactSupport g ∧ ContDiff ℝ (↑⊤) g ∧ MeasureTheory.eLpNorm (f_L2 - g) 2 MeasureTheory.volume < ENNReal.ofReal ε

theorem Frourio.tendsto_one_div_add_one_nhds_0 : Filter.Tendsto (fun (n : ℕ) => 1 / (↑n + 1)) Filter.atTop (nhds 0)

The sequence n ↦ 1/(n+1) tends to zero.

theorem Frourio.smooth_compactly_supported_dense_L2_sequence (f : ℝ → ℂ) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : ∃ (ψ : ℕ → ℝ → ℂ), (∀ (n : ℕ), HasCompactSupport (ψ n)) ∧ (∀ (n : ℕ), ContDiff ℝ (↑⊤) (ψ n)) ∧ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (t : ℝ) => f t - ψ n t) 2 MeasureTheory.volume) Filter.atTop (nhds 0)

Produce a sequence of compactly supported smooth approximations for an L² function.

theorem Frourio.Schwartz.memLp_fourierIntegral (φ : SchwartzMap ℝ ℂ) {p : ENNReal} : MeasureTheory.MemLp (fun (ξ : ℝ) => fourierIntegral (fun (t : ℝ) => φ t) ξ) p MeasureTheory.volume

The Fourier integral of a Schwartz function is in every Lᵖ.

theorem Frourio.fourierIntegral_inner_schwartz {f : ℝ → ℂ} (hf_L1 : MeasureTheory.Integrable f MeasureTheory.volume) (ψ : SchwartzMap ℝ ℂ) : ∫ (ξ : ℝ), VectorFourier.fourierIntegral Real.fourierChar MeasureTheory.volume (innerₗ ℝ) f ξ * Schwartz.conjFourierTransform ψ ξ = ∫ (t : ℝ), f t * VectorFourier.fourierIntegral Real.fourierChar MeasureTheory.volume (innerₗ ℝ) (Schwartz.conjFourierTransform ψ) t

Pairing the Fourier transform of an integrable function with a Schwartz test function can be rewritten using the conjugated transform.

theorem Frourio.fourierIntegral_inner_schwartz_conj {f : ℝ → ℂ} (hf_L1 : MeasureTheory.Integrable f MeasureTheory.volume) (ψ : SchwartzMap ℝ ℂ) : ∫ (ξ : ℝ), fourierIntegral f ξ * (starRingEnd ℂ) (fourierIntegral (fun (t : ℝ) => ψ t) ξ) = ∫ (t : ℝ), f t * (starRingEnd ℂ) (ψ t)

Frequency-side pairing with a Schwartz function can be rewritten using the explicit kernel formulation.

theorem Frourio.fourierIntegral_memLp_of_schwartz (φ : SchwartzMap ℝ ℂ) : MeasureTheory.MemLp (fun (ξ : ℝ) => fourierIntegral (fun (t : ℝ) => φ t) ξ) 2 MeasureTheory.volume

For Schwartz functions the Fourier integral belongs to L².

theorem Frourio.fourierIntegral_eLpNorm_eq (φ : SchwartzMap ℝ ℂ) : MeasureTheory.eLpNorm (fun (ξ : ℝ) => fourierIntegral (fun (t : ℝ) => φ t) ξ) 2 MeasureTheory.volume = MeasureTheory.eLpNorm (fun (t : ℝ) => φ t) 2 MeasureTheory.volume

theorem Frourio.schwartz_integrable (φ : SchwartzMap ℝ ℂ) : MeasureTheory.Integrable (fun (t : ℝ) => φ t) MeasureTheory.volume

A Schwartz function is integrable.

theorem Frourio.exists_schwartz_L2_approx (f : ℝ → ℂ) (_hf_L1 : MeasureTheory.Integrable f MeasureTheory.volume) (hf_L2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) : ∃ (φ : ℕ → SchwartzMap ℝ ℂ), (∀ (n : ℕ), MeasureTheory.Integrable (fun (t : ℝ) => (φ n) t) MeasureTheory.volume) ∧ (∀ (n : ℕ), MeasureTheory.MemLp (fun (t : ℝ) => (φ n) t) 2 MeasureTheory.volume) ∧ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (t : ℝ) => f t - (φ n) t) 2 MeasureTheory.volume) Filter.atTop (nhds 0)

L¹ ∩ L² functions can be approximated in L² by Schwartz functions. This is a preparatory statement for the Plancherel extension.

theorem Frourio.tendsto_inner_const_right_of_L2_tendsto {φ : ℕ → ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)} {f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)} (hφ : Filter.Tendsto φ Filter.atTop (nhds f)) (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : Filter.Tendsto (fun (n : ℕ) => inner ℂ (φ n) g) Filter.atTop (nhds (inner ℂ f g))

theorem Frourio.tendsto_inner_const_left_of_L2_tendsto {φ : ℕ → ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)} {f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)} (hφ : Filter.Tendsto φ Filter.atTop (nhds f)) (g : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : Filter.Tendsto (fun (n : ℕ) => inner ℂ g (φ n)) Filter.atTop (nhds (inner ℂ g f))

theorem Frourio.exists_schwartz_L2_approx_general (f : ℝ → ℂ) (hf_L2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) (ε : ℝ) (hε_pos : 0 < ε) : ∃ (φ : SchwartzMap ℝ ℂ), MeasureTheory.eLpNorm (fun (t : ℝ) => f t - φ t) 2 MeasureTheory.volume < ENNReal.ofReal ε

Each L² function can be approximated arbitrarily well by a Schwartz function.

theorem Frourio.denseRange_schwartz_toLp_L2 : DenseRange fun (φ : SchwartzMap ℝ ℂ) => MeasureTheory.MemLp.toLp (fun (t : ℝ) => φ t) ⋯

Schwartz functions are dense in L²(ℝ) viewed as Lp.

theorem Frourio.tendsto_schwartz_toLp_L2 (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ∃ (φ : ℕ → SchwartzMap ℝ ℂ), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.MemLp.toLp (fun (t : ℝ) => (φ n) t) ⋯) Filter.atTop (nhds f)

Every L² function is the limit of a sequence of Schwartz functions in the L² topology. This upgrades the density statement to a sequential form that is convenient for limit arguments.

theorem Frourio.exists_schwartz_inner_ne_zero {h : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)} (hh : h ≠ 0) : ∃ (ψ : SchwartzMap ℝ ℂ), inner ℂ h (MeasureTheory.MemLp.toLp (fun (t : ℝ) => ψ t) ⋯) ≠ 0

If an L² function is nonzero, some Schwartz test function detects it via the inner product.

theorem Frourio.L2_eq_zero_of_inner_schwartz {h : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)} (hh : ∀ (ψ : SchwartzMap ℝ ℂ), inner ℂ h (MeasureTheory.MemLp.toLp (fun (t : ℝ) => ψ t) ⋯) = 0) : h = 0

If the inner product against every Schwartz test function vanishes, then the L² function is identically zero.

theorem Frourio.eLpNorm_tendsto_toReal_of_tendsto {φ : ℕ → SchwartzMap ℝ ℂ} {f : ℝ → ℂ} (hf_L2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hφ_L2 : ∀ (n : ℕ), MeasureTheory.MemLp (fun (t : ℝ) => (φ n) t) 2 MeasureTheory.volume) (hφ_tendsto : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (t : ℝ) => f t - (φ n) t) 2 MeasureTheory.volume) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => (MeasureTheory.eLpNorm (fun (t : ℝ) => f t - (φ n) t) 2 MeasureTheory.volume).toReal) Filter.atTop (nhds 0)

theorem Frourio.toLp_tendsto_of_eLpNorm_tendsto {φ : ℕ → SchwartzMap ℝ ℂ} {f : ℝ → ℂ} (hf_L2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hφ_L2 : ∀ (n : ℕ), MeasureTheory.MemLp (fun (t : ℝ) => (φ n) t) 2 MeasureTheory.volume) (hφ_tendsto : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (t : ℝ) => f t - (φ n) t) 2 MeasureTheory.volume) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.MemLp.toLp (fun (t : ℝ) => (φ n) t) ⋯) Filter.atTop (nhds (MeasureTheory.MemLp.toLp f hf_L2))

theorem Frourio.weak_limit_fourierIntegral_of_schwartz_tendsto {φ : ℕ → SchwartzMap ℝ ℂ} {f : ℝ → ℂ} (hf_L2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hφ_L1 : ∀ (n : ℕ), MeasureTheory.Integrable (fun (t : ℝ) => (φ n) t) MeasureTheory.volume) (hφ_L2 : ∀ (n : ℕ), MeasureTheory.MemLp (fun (t : ℝ) => (φ n) t) 2 MeasureTheory.volume) (hφ_tendsto : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (t : ℝ) => f t - (φ n) t) 2 MeasureTheory.volume) Filter.atTop (nhds 0)) (ψ : SchwartzMap ℝ ℂ) : Filter.Tendsto (fun (n : ℕ) => inner ℂ (MeasureTheory.MemLp.toLp (fun (ξ : ℝ) => fourierIntegral (fun (t : ℝ) => ψ t) ξ) ⋯) (MeasureTheory.MemLp.toLp (fun (ξ : ℝ) => fourierIntegral (fun (t : ℝ) => (φ n) t) ξ) ⋯)) Filter.atTop (nhds (∫ (t : ℝ), f t * (starRingEnd ℂ) (ψ t)))

theorem Frourio.fourierIntegral_cauchySeq_of_schwartz_tendsto {φ : ℕ → SchwartzMap ℝ ℂ} {f : ℝ → ℂ} (hf_L2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hφ_L1 : ∀ (n : ℕ), MeasureTheory.Integrable (fun (t : ℝ) => (φ n) t) MeasureTheory.volume) (hφ_L2 : ∀ (n : ℕ), MeasureTheory.MemLp (fun (t : ℝ) => (φ n) t) 2 MeasureTheory.volume) (hφ_tendsto : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (t : ℝ) => f t - (φ n) t) 2 MeasureTheory.volume) Filter.atTop (nhds 0)) : CauchySeq fun (n : ℕ) => MeasureTheory.MemLp.toLp (fun (ξ : ℝ) => fourierIntegral (fun (t : ℝ) => (φ n) t) ξ) ⋯

theorem Frourio.weak_convergence_fourierIntegral_of_schwartz_approx {φ : ℕ → SchwartzMap ℝ ℂ} {f : ℝ → ℂ} (hf_L1 : MeasureTheory.Integrable f MeasureTheory.volume) (ψLp : ℕ → ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : (∀ (n : ℕ), ψLp n = MeasureTheory.MemLp.toLp (fun (ξ : ℝ) => fourierIntegral (fun (t : ℝ) => (φ n) t) ξ) ⋯) → ∀ (h_weak_limit : ∀ (ψ : SchwartzMap ℝ ℂ), Filter.Tendsto (fun (n : ℕ) => inner ℂ (MeasureTheory.MemLp.toLp (fun (ξ : ℝ) => fourierIntegral (fun (t : ℝ) => ψ t) ξ) ⋯) (ψLp n)) Filter.atTop (nhds (∫ (t : ℝ), f t * (starRingEnd ℂ) (ψ t)))) (ψ : SchwartzMap ℝ ℂ), Filter.Tendsto (fun (n : ℕ) => ∫ (x : ℝ), ↑↑(ψLp n) x * (starRingEnd ℂ) (ψ.toFun x)) Filter.atTop (nhds (∫ (x : ℝ), fourierIntegral f x * (starRingEnd ℂ) (ψ.toFun x)))

Weak convergence of Fourier transforms of Schwartz approximations implies convergence to the Fourier transform of the limit function.

theorem Frourio.strong_L2_implies_weak_convergence_schwartz (ψLp : ℕ → ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (ψ_lim : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (hψ_lim : Filter.Tendsto ψLp Filter.atTop (nhds ψ_lim)) (φ : SchwartzMap ℝ ℂ) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : ℝ), ↑↑(ψLp n) x * (starRingEnd ℂ) (φ.toFun x)) Filter.atTop (nhds (∫ (x : ℝ), ↑↑ψ_lim x * (starRingEnd ℂ) (φ.toFun x)))

Strong L² convergence implies weak convergence against Schwartz test functions.