def instCoeForallRealForallComplex_primeNumberTheoremAnd {E : Type u_1} : Coe (E → ℝ) (E → ℂ)

Equations

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

@[simp]

theorem nnnorm_eq_of_mem_circle (z : Circle) : ‖↑z‖₊ = 1

@[simp]

theorem nnnorm_circle_smul (z : Circle) (s : ℂ) : ‖z • s‖₊ = ‖s‖₊

noncomputable def e (u : ℝ) : BoundedContinuousFunction ℝ ℂ

Equations

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

@[simp]

theorem e_apply (u v : ℝ) : (e u) v = ↑(Real.fourierChar (-v * u))

theorem hasDerivAt_e {u x : ℝ} : HasDerivAt (⇑(e u)) (-2 * ↑Real.pi * ↑u * Complex.I * (e u) x) x

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

@[simp]

theorem F_neg {f : ℝ → ℂ} {u : ℝ} : Real.fourierIntegral (fun (x : ℝ) => -f x) u = -Real.fourierIntegral f u

@[simp]

theorem F_add {f g : ℝ → ℂ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (x : ℝ) : Real.fourierIntegral (fun (x : ℝ) => f x + g x) x = Real.fourierIntegral f x + Real.fourierIntegral g x

@[simp]

theorem F_sub {f g : ℝ → ℂ} (hf : MeasureTheory.Integrable f MeasureTheory.volume) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (x : ℝ) : Real.fourierIntegral (fun (x : ℝ) => f x - g x) x = Real.fourierIntegral f x - Real.fourierIntegral g x

@[simp]

theorem F_mul {f : ℝ → ℂ} {c : ℂ} {u : ℝ} : Real.fourierIntegral (fun (x : ℝ) => c * f x) u = c * Real.fourierIntegral f u

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

@[simp]

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