Commit 2021-06-03 07:38 6d90d35f

View on Github →

feat(analysis/fourier): monomials on the circle are orthonormal (#6952) Make the circle into a measure space, using Haar measure, and prove that the monomials z ^ n are orthonormal when considered as elements of L^2 on the circle.

Estimated changes

Created src/analysis/fourier.lean

added def fourier

added theorem fourier_add

added theorem fourier_add_half_inv_index

added theorem fourier_neg

added theorem fourier_zero

added def haar_circle

added theorem orthonormal_fourier

Modified src/data/complex/exponential.lean

added theorem complex.exp_int_mul

Modified src/geometry/manifold/instances/circle.lean

modified theorem coe_div_circle

modified theorem coe_inv_circle

added theorem coe_inv_circle_eq_conj

added theorem exp_map_circle_apply

added theorem nonzero_of_mem_circle

added theorem norm_sq_eq_of_mem_circle

Modified src/measure_theory/l2_space.lean

added theorem measure_theory.bounded_continuous_function.inner_to_Lp

added theorem measure_theory.continuous_map.inner_to_Lp

Modified src/measure_theory/lp_space.lean

added theorem bounded_continuous_function.coe_fn_to_Lp

added theorem continuous_map.coe_fn_to_Lp

modified theorem continuous_map.to_Lp_norm_le

Modified src/topology/compacts.lean

added def topological_space.positive_compacts_univ

Modified src/topology/metric_space/basic.lean

added theorem is_compact_sphere