OAI/Analysis/SymmetricDomains/CosineBumpWeightedSummable.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Release061.Wiener.exists_boundary_of_weighted_summable line 19
2. lemma OAI.Release061.Wiener.exists_real_boundary_of_weighted_summable line 38
3. def OAI.Release061.Wiener.circleCos line 55
4. lemma OAI.Release061.Wiener.circleCos_zero line 58
5. lemma OAI.Release061.Wiener.circleCos_coe line 60
6. lemma OAI.Release061.Wiener.circleCos_half line 65
7. def OAI.Release061.Wiener.cosineBump line 70
8. lemma OAI.Release061.Wiener.cosineBump_weighted_summable line 74