Commit 2023-06-20 10:20 9a53f9f9

View on Github →

port Analysis.Fourier.AddCircle (#5273)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Fourier/AddCircle.lean

added theorem AddCircle.continuous_toCircle

added def AddCircle.haarAddCircle

added theorem AddCircle.injective_toCircle

added theorem AddCircle.scaled_exp_map_periodic

added def AddCircle.toCircle

added theorem AddCircle.toCircle_add

added theorem AddCircle.volume_eq_smul_haarAddCircle

added theorem coeFn_fourierLp

added theorem coe_fourierBasis

added def fourier

added def fourierBasis

added theorem fourierBasis_repr

added theorem fourierCoeff.const_mul

added theorem fourierCoeff.const_smul

added def fourierCoeff

added theorem fourierCoeffOn.const_mul

added theorem fourierCoeffOn.const_smul

added def fourierCoeffOn

added theorem fourierCoeffOn_eq_integral

added theorem fourierCoeffOn_of_hasDerivAt

added theorem fourierCoeff_eq_intervalIntegral

added theorem fourierCoeff_liftIco_eq

added theorem fourierCoeff_liftIoc_eq

added theorem fourierCoeff_toLp

added def fourierSubalgebra

added theorem fourierSubalgebra_closure_eq_top

added theorem fourierSubalgebra_coe

added theorem fourierSubalgebra_conj_invariant

added theorem fourierSubalgebra_separatesPoints

added theorem fourier_add'

added theorem fourier_add

added theorem fourier_add_half_inv_index

added theorem fourier_apply

added theorem fourier_coe_apply'

added theorem fourier_coe_apply

added theorem fourier_eval_zero

added theorem fourier_neg'

added theorem fourier_neg

added theorem fourier_norm

added theorem fourier_one

added theorem fourier_zero'

added theorem fourier_zero

added theorem hasDerivAt_fourier

added theorem hasDerivAt_fourier_neg

added theorem hasSum_fourier_series_L2

added theorem hasSum_fourier_series_of_summable

added theorem has_antideriv_at_fourier_neg

added theorem has_pointwise_sum_fourier_series_of_summable

added theorem orthonormal_fourier

added theorem span_fourierLp_closure_eq_top

added theorem span_fourier_closure_eq_top

added theorem tsum_sq_fourierCoeff