theorem Frourio.integral_mul_star_eq_inner {g : ℝ → ℂ} (hg_mem : MeasureTheory.MemLp g 2 MeasureTheory.volume) (φ : SchwartzMap ℝ ℂ) : ∫ (x : ℝ), g x * (starRingEnd ℂ) (φ.toFun x) = inner ℂ (MeasureTheory.MemLp.toLp (fun (x : ℝ) => φ x) ⋯) (MeasureTheory.MemLp.toLp g hg_mem)

Relate pairing with a Schwartz test function to the L² inner product.

theorem Frourio.ae_eq_of_memLp_schwartz_pairings {g₁ g₂ : ℝ → ℂ} (hg₁ : MeasureTheory.MemLp g₁ 2 MeasureTheory.volume) (hg₂ : MeasureTheory.MemLp g₂ 2 MeasureTheory.volume) (h_pairings : ∀ (φ : SchwartzMap ℝ ℂ), ∫ (x : ℝ), g₁ x * (starRingEnd ℂ) (φ.toFun x) = ∫ (x : ℝ), g₂ x * (starRingEnd ℂ) (φ.toFun x)) : g₁ =ᵐ[MeasureTheory.volume] g₂

Two L² functions that have identical pairings with all Schwartz tests coincide almost everywhere.

theorem Frourio.integrable_tail_small {f : ℝ → ℂ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (δ : ℝ) : δ > 0 → ∃ R > 0, ∫ (t : ℝ) in {t : ℝ | R ≤ |t|}, ‖f t‖ < δ

Helper lemma: For integrable functions, the tail integral can be made arbitrarily small.

theorem Frourio.eLpNorm_one_le_measure_mul_eLpNorm_two_of_ball {f : ℝ → ℂ} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (R : ℝ) : ∫ (t : ℝ) in {t : ℝ | |t| ≤ R}, ‖f t‖ ≤ (MeasureTheory.volume {t : ℝ | |t| ≤ R}).toReal ^ (1 / 2) * (MeasureTheory.eLpNorm f 2 MeasureTheory.volume).toReal

Hölder's inequality on a ball: L¹ norm bounded by L² norm times measure to the 1/2.

theorem Frourio.volume_ball_eq (R : ℝ) : MeasureTheory.volume {t : ℝ | |t| ≤ R} = ENNReal.ofReal (2 * R)

The Lebesgue measure of a ball in ℝ.

theorem Frourio.finite_uniform_tail_bound {ι : Type u_1} [Fintype ι] (g : ι → ℝ → ℂ) (hg : ∀ (i : ι), MeasureTheory.Integrable (g i) MeasureTheory.volume) (δ : ℝ) (hδ : 0 < δ) : ∃ R > 0, ∀ (i : ι), ∫ (t : ℝ) in {t : ℝ | R ≤ |t|}, ‖g i t‖ < δ

For a finite collection of integrable functions and their tails, we can find a uniform radius R such that all tails are small.

theorem Frourio.tail_integral_diff_le (f g : ℝ → ℂ) (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (R : ℝ) : ∫ (t : ℝ) in {t : ℝ | R ≤ |t|}, ‖f t - g t‖ ≤ (∫ (t : ℝ) in {t : ℝ | R ≤ |t|}, ‖f t‖) + ∫ (t : ℝ) in {t : ℝ | R ≤ |t|}, ‖g t‖

Helper: bound tail of difference by triangle inequality.

theorem Frourio.fourierIntegral_tendsto_of_schwartz_approx {φ : ℕ → SchwartzMap ℝ ℂ} {f : ℝ → ℂ} (hf_L1 : MeasureTheory.Integrable f MeasureTheory.volume) (hφ_L1 : ∀ (n : ℕ), MeasureTheory.Integrable (fun (t : ℝ) => (φ n) t) MeasureTheory.volume) (hφ_tendsto_L1 : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (t : ℝ) => f t - (φ n) t) 1 MeasureTheory.volume) Filter.atTop (nhds 0)) (ξ : ℝ) : Filter.Tendsto (fun (n : ℕ) => fourierIntegral (fun (t : ℝ) => (φ n) t) ξ) Filter.atTop (nhds (fourierIntegral f ξ))

If Schwartz functions φₙ approximate f in both L¹ and L², then their Fourier transforms converge pointwise to the Fourier transform of f. We require L¹ convergence explicitly, since L² convergence alone is insufficient.

theorem Frourio.fourierIntegral_L2_convergence_of_schwartz_approx {φ : ℕ → SchwartzMap ℝ ℂ} {f : ℝ → ℂ} (_hf_L1 : MeasureTheory.Integrable f MeasureTheory.volume) (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)) : ∃ (ψLp : ℕ → ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (ψ_lim : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)), (∀ (n : ℕ), ψLp n = MeasureTheory.MemLp.toLp (fun (ξ : ℝ) => fourierIntegral (fun (t : ℝ) => (φ n) t) ξ) ⋯) ∧ Filter.Tendsto ψLp Filter.atTop (nhds ψ_lim)

If Schwartz functions φₙ approximate f in L², then their Fourier transforms form a Cauchy sequence in L², which converges strongly to some limit in L².

theorem Frourio.fourierIntegral_memLp_limit {φ : ℕ → SchwartzMap ℝ ℂ} {f : ℝ → ℂ} (hf_L1 : MeasureTheory.Integrable f MeasureTheory.volume) (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)) : ∃ (ψLp : ℕ → ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (ψ_lim : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)), (∀ (n : ℕ), ψLp n = MeasureTheory.MemLp.toLp (fun (ξ : ℝ) => fourierIntegral (fun (t : ℝ) => (φ n) t) ξ) ⋯) ∧ Filter.Tendsto ψLp Filter.atTop (nhds ψ_lim)

When a function f is approximated in L² by Schwartz functions, the corresponding Fourier transforms form a Cauchy sequence in L² and hence converge to some limit in L². We package this convergence datum.

theorem Frourio.fourierIntegral_memLp_of_memLp (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) (ψLp : ℕ → ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) (ψ_lim : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)), (∀ (n : ℕ), ψLp n = MeasureTheory.MemLp.toLp (fun (ξ : ℝ) => fourierIntegral (fun (t : ℝ) => (φ n) t) ξ) ⋯) ∧ Filter.Tendsto ψLp Filter.atTop (nhds ψ_lim)

theorem Frourio.integrable_norm_sq_of_memLp_two {f : ℝ → ℂ} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : MeasureTheory.Integrable (fun (t : ℝ) => ‖f t‖ ^ 2) MeasureTheory.volume

For an L² function, the square of its norm is integrable.

theorem Frourio.memLp_two_tail_norm_sq_small {f : ℝ → ℂ} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (δ : ℝ) : δ > 0 → ∃ R > 0, ∫ (t : ℝ) in {t : ℝ | R ≤ |t|}, ‖f t‖ ^ 2 < δ

The tail of an L² function has small squared norm.

theorem Frourio.integrable_indicator_ball_of_integrable {f : ℝ → ℂ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (R : ℝ) : MeasureTheory.Integrable (fun (t : ℝ) => {t : ℝ | |t| ≤ R}.indicator f t) MeasureTheory.volume

Truncating an integrable function to a ball preserves integrability.

theorem Frourio.tsupport_indicator_subset_ball {f : ℝ → ℂ} {R : ℝ} : (tsupport fun (t : ℝ) => {t : ℝ | |t| ≤ R}.indicator f t) ⊆ Metric.closedBall 0 R

The support of a ball-truncated function is contained in that ball.

theorem Frourio.sub_indicator_ball_eq_indicator_compl (f : ℝ → ℂ) (R : ℝ) : (fun (t : ℝ) => f t - {t : ℝ | |t| ≤ R}.indicator f t) = fun (t : ℝ) => {t : ℝ | |t| ≤ R}ᶜ.indicator f t

Removing the ball of radius R from f corresponds to restricting f to the complement.

theorem Frourio.integrable_memLp_tail_small {f : ℝ → ℂ} (hf_L1 : MeasureTheory.Integrable f MeasureTheory.volume) (hf_L2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) (δ : ℝ) : δ > 0 → ∃ R > 0, ∫ (t : ℝ) in {t : ℝ | R ≤ |t|}, ‖f t‖ < δ ∧ ∫ (t : ℝ) in {t : ℝ | R ≤ |t|}, ‖f t‖ ^ 2 < δ

Small L¹ and L² tails for integrable and L² functions.

theorem Frourio.eLpNorm_one_tail_indicator_sub {f : ℝ → ℂ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) {R δ : ℝ} (h_tail : ∫ (t : ℝ) in {t : ℝ | R ≤ |t|}, ‖f t‖ < δ) : MeasureTheory.eLpNorm (fun (t : ℝ) => f t - {t : ℝ | |t| ≤ R}.indicator f t) 1 MeasureTheory.volume < ENNReal.ofReal δ

Control the L¹ error after truncating a function outside a ball using the tail integral.

theorem Frourio.eLpNorm_two_tail_indicator_sub {f : ℝ → ℂ} (hf_L2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) {R δ : ℝ} (hδ : 0 < δ) (h_tail : ∫ (t : ℝ) in {t : ℝ | R ≤ |t|}, ‖f t‖ ^ 2 < δ ^ 2) : MeasureTheory.eLpNorm (fun (t : ℝ) => f t - {t : ℝ | |t| ≤ R}.indicator f t) 2 MeasureTheory.volume < ENNReal.ofReal δ

Control the L² error after truncating a function outside a ball using the squared tail integral.

theorem Frourio.memLp_one_indicator_ball_of_memLp_two {f : ℝ → ℂ} (hf_L2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) (R : ℝ) : MeasureTheory.MemLp (fun (t : ℝ) => {t : ℝ | |t| ≤ R}.indicator f t) 1 MeasureTheory.volume

L¹/L² control on the difference between f and its ball truncation.

theorem Frourio.integrable_indicator_tail_of_tail_bound {f : ℝ → ℂ} (hf_L2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) {R : ℝ} (h_tail_finite : MeasureTheory.HasFiniteIntegral (fun (t : ℝ) => {t : ℝ | R ≤ |t|}.indicator (fun (t : ℝ) => ‖f t‖) t) MeasureTheory.volume) : MeasureTheory.Integrable (fun (t : ℝ) => {t : ℝ | R ≤ |t|}.indicator f t) MeasureTheory.volume

theorem Frourio.integrable_indicator_ball_of_memLp_two {f : ℝ → ℂ} (hf_L2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) (R : ℝ) : MeasureTheory.Integrable (fun (t : ℝ) => {t : ℝ | |t| ≤ R}.indicator f t) MeasureTheory.volume

theorem Frourio.integrable_of_memLp_two_with_tail_bound {f : ℝ → ℂ} (hf_L2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) {R : ℝ} (h_tail_finite : MeasureTheory.HasFiniteIntegral (fun (t : ℝ) => {t : ℝ | R ≤ |t|}.indicator (fun (t : ℝ) => ‖f t‖) t) MeasureTheory.volume) : MeasureTheory.Integrable f MeasureTheory.volume

theorem Frourio.hasFiniteIntegral_indicator_norm_of_integral_lt {f : ℝ → ℂ} (R δ : ℝ) (hf_meas : MeasureTheory.AEStronglyMeasurable (fun (t : ℝ) => {t : ℝ | R ≤ |t|}.indicator (fun (t : ℝ) => ‖f t‖) t) MeasureTheory.volume) (h_tail : ∫⁻ (t : ℝ) in {t : ℝ | R ≤ |t|}, ENNReal.ofReal ‖f t‖ < ENNReal.ofReal δ) : MeasureTheory.HasFiniteIntegral (fun (t : ℝ) => {t : ℝ | R ≤ |t|}.indicator (fun (t : ℝ) => ‖f t‖) t) MeasureTheory.volume

theorem Frourio.smooth_compact_support_to_schwartz_L1_L2 {g : ℝ → ℂ} (hg_compact : HasCompactSupport g) (hg_smooth : ContDiff ℝ (↑⊤) g) (ε : ℝ) (hε : 0 < ε) : ∃ (φ : SchwartzMap ℝ ℂ), MeasureTheory.eLpNorm (fun (t : ℝ) => g t - φ t) 1 MeasureTheory.volume < ENNReal.ofReal ε ∧ MeasureTheory.eLpNorm (fun (t : ℝ) => g t - φ t) 2 MeasureTheory.volume < ENNReal.ofReal ε

Upgrade a smooth compactly supported approximation to a Schwartz approximation in L¹ and L².