OAI/Analysis/SymmetricDomains/SmoothFlatWeightedFourier.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.Release061.weighted_summable_of_cubic_decayline 18 - lemma
OAI.Release061.fourierCoeffOn_norm_leline 45 - lemma
OAI.Release061.fourierCoeffOn_deriv_norm_leline 57 - theorem
OAI.Release061.smooth_flat_weighted_fourierline 73