Documentation

PrimeNumberTheoremAnd.Fourier

@[instance_reducible]

def instCoeForallRealForallComplex_primeNumberTheoremAnd {E : Type u_1} :

Coe (E → ℝ) (E → ℂ)

Equations

instCoeForallRealForallComplex_primeNumberTheoremAnd = { coe := fun (f : E → ℝ) (n : E) => ↑(f n) }

Instances For

Inspect dependencies

instCoeForallRealForallComplex_primeNumberTheoremAnd · compiled type and proof/definition references.

@[simp]

theorem nnnorm_eq_of_mem_circle (z : Circle) :

‖↑z‖₊ = 1

Inspect dependencies

nnnorm_eq_of_mem_circle · compiled type and proof/definition references.

@[simp]

theorem nnnorm_circle_smul (z : Circle) (s : ℂ) :

‖z • s‖₊ = ‖s‖₊

Inspect dependencies

nnnorm_circle_smul · compiled type and proof/definition references.

noncomputable def e (u : ℝ) :

BoundedContinuousFunction ℝ ℂ

Equations

e u = { toFun := fun (v : ℝ) => ↑(Real.fourierChar (-v * u)), continuous_toFun := ⋯, map_bounded' := ⋯ }

Instances For

Inspect dependencies

e · compiled type and proof/definition references.

@[simp]

theorem e_apply (u v : ℝ) :

(e u) v = ↑(Real.fourierChar (-v * u))

Inspect dependencies

e_apply · compiled type and proof/definition references.

theorem hasDerivAt_e {u x : ℝ} :

HasDerivAt (⇑(e u)) (-2 * ↑Real.pi * ↑u * Complex.I * (e u) x) x

Inspect dependencies

hasDerivAt_e · compiled type and proof/definition references.

theorem fourierIntegral_deriv_aux2 (e : BoundedContinuousFunction ℝ ℂ) {f : ℝ → ℂ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) :

MeasureTheory.Integrable (⇑e * f) MeasureTheory.volume

Inspect dependencies

fourierIntegral_deriv_aux2 · compiled type and proof/definition references.

@[simp]

theorem F_neg {f : ℝ → ℂ} {u : ℝ} :

FourierTransform.fourier (fun (x : ℝ) => -f x) u = -FourierTransform.fourier f u

Inspect dependencies

F_neg · compiled type and proof/definition references.

@[simp]

theorem F_add {f g : ℝ → ℂ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (x : ℝ) :

FourierTransform.fourier (fun (x : ℝ) => f x + g x) x = FourierTransform.fourier f x + FourierTransform.fourier g x

Inspect dependencies

F_add · compiled type and proof/definition references.

@[simp]

theorem F_sub {f g : ℝ → ℂ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (x : ℝ) :

FourierTransform.fourier (fun (x : ℝ) => f x - g x) x = FourierTransform.fourier f x - FourierTransform.fourier g x

Inspect dependencies

F_sub · compiled type and proof/definition references.

@[simp]

theorem F_mul {f : ℝ → ℂ} {c : ℂ} {u : ℝ} :

FourierTransform.fourier (fun (x : ℝ) => c * f x) u = c * FourierTransform.fourier f u

Inspect dependencies

F_mul · compiled type and proof/definition references.

theorem fourierIntegral_self_add_deriv_deriv (f : W21) (u : ℝ) :

(1 + ↑u ^ 2) * FourierTransform.fourier f.toFun u = FourierTransform.fourier (fun (u : ℝ) => f.toFun u - 1 / (4 * ↑Real.pi ^ 2) * deriv ^[2] f.toFun u) u

Inspect dependencies

fourierIntegral_self_add_deriv_deriv · compiled type and proof/definition references.

@[simp]

theorem deriv_ofReal :

deriv Complex.ofReal = fun (x : ℝ) => 1

Inspect dependencies

deriv_ofReal · compiled type and proof/definition references.

theorem tendsto_intervalIntegral_zero_of_uniform_norm_bound {f : ℝ → ℝ → ℂ} {lo hi : ℝ} {B : ℝ → ℝ} (hB : Filter.Tendsto (fun (T : ℝ) => B T * |hi - lo|) Filter.atTop (nhds 0)) (hf : ∀ᶠ (T : ℝ) in Filter.atTop , ∀ x ∈ Set.uIoc lo hi, ‖f T x‖ ≤ B T) :

Filter.Tendsto (fun (T : ℝ) => ∫ (x : ℝ) in lo..hi, f T x) Filter.atTop (nhds 0)

If, eventually in T, the integrand f T is bounded on uIoc lo hi by B T and B T * |hi - lo| → 0, then the interval integral ∫ x in lo..hi, f T x → 0.

Inspect dependencies

tendsto_intervalIntegral_zero_of_uniform_norm_bound · compiled type and proof/definition references.

theorem tendsto_const_mul_log_add_two_div_add_two_atTop (K : ℝ) :

Filter.Tendsto (fun (T : ℝ) => K * (Real.log (T + 2) / (T + 2))) Filter.atTop (nhds 0)

The decay K * (log (T + 2) / (T + 2)) → 0 as T → ∞, for any constant K.

Inspect dependencies

tendsto_const_mul_log_add_two_div_add_two_atTop · compiled type and proof/definition references.

theorem norm_fourier_le_integral_deriv_div (g : ℝ → ℂ) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hdiff : Differentiable ℝ g) (hg' : MeasureTheory.Integrable (deriv g) MeasureTheory.volume) {w : ℝ} (hw : w ≠ 0) :

‖FourierTransform.fourier g w‖ ≤ (∫ (x : ℝ), ‖deriv g x‖) / (2 * Real.pi * |w|)

Fourier-transform decay from an integrable derivative: for integrable, differentiable g with integrable derivative, ‖𝓕 g w‖ ≤ (∫ ‖deriv g x‖) / (2π·|w|).

Inspect dependencies

norm_fourier_le_integral_deriv_div · compiled type and proof/definition references.

theorem norm_oscillatory_integral_le_integral_deriv_div_abs (g : ℝ → ℂ) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hdiff : Differentiable ℝ g) (hg' : MeasureTheory.Integrable (deriv g) MeasureTheory.volume) {T : ℝ} (hT : T ≠ 0) :

‖∫ (y : ℝ), g y * Complex.exp (↑T * Complex.I * ↑y)‖ ≤ (∫ (x : ℝ), ‖deriv g x‖) / |T|

The |T| variant of the oscillatory-integral decay bound: for T ≠ 0, ‖∫ g y · exp(T·i·y)‖ ≤ (∫ ‖deriv g x‖) / |T|.

Inspect dependencies

norm_oscillatory_integral_le_integral_deriv_div_abs · compiled type and proof/definition references.

theorem norm_oscillatory_integral_le_integral_deriv_div (g : ℝ → ℂ) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hdiff : Differentiable ℝ g) (hg' : MeasureTheory.Integrable (deriv g) MeasureTheory.volume) {T : ℝ} (hT : 0 < T) :

‖∫ (y : ℝ), g y * Complex.exp (↑T * Complex.I * ↑y)‖ ≤ (∫ (x : ℝ), ‖deriv g x‖) / T

The oscillatory-integral form of the decay bound: for 0 < T, ‖∫ g y · exp(T·i·y)‖ ≤ (∫ ‖deriv g x‖) / T.

Inspect dependencies

norm_oscillatory_integral_le_integral_deriv_div · compiled type and proof/definition references.