Fourier

📁 Source: PrimeNumberTheoremAnd/Fourier.lean

Statistics

Metric	Count
Definitions e, instCoeForallRealForallComplex_primeNumberTheoremAnd	2
Theorems F_add, F_mul, F_neg, F_sub, deriv_ofReal, e_apply, fourierIntegral_deriv_aux2, fourierIntegral_self_add_deriv_deriv, hasDerivAt_e, nnnorm_circle_smul, nnnorm_eq_of_mem_circle	11
Total	13

(root)

Definitions

Name	Category	Theorems
e 📖	CompOp	2 math math: e_apply, hasDerivAt_e
instCoeForallRealForallComplex_primeNumberTheoremAnd 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
F_add 📖	—	—	—	—	—
F_mul 📖	—	—	—	—	—
F_neg 📖	—	—	—	—	—
F_sub 📖	—	—	—	—	F_neg F_add
deriv_ofReal 📖	—	—	—	—	—
e_apply 📖	mathematical	—	e	—	—
fourierIntegral_deriv_aux2 📖	—	—	—	—	—
fourierIntegral_self_add_deriv_deriv 📖	mathematical	—	W1.toFun	—	W1.integrable W1.differentiable F_sub W21.hf F_mul W21.hf' W21.hf''
hasDerivAt_e 📖	mathematical	—	e	—	—
nnnorm_circle_smul 📖	—	—	—	—	nnnorm_eq_of_mem_circle
nnnorm_eq_of_mem_circle 📖	—	—	—	—	—

---

← Back to Index