OAI/Analysis/IntegralMeans/KoebePolar.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Brennan.Sharp.sector_cos_lower line 10
2. lemma OAI.Brennan.Sharp.polar_cone_data line 19
3. lemma OAI.Brennan.Sharp.polar_left_mem_disk line 34
4. lemma OAI.Brennan.Sharp.polar_right_mem_disk line 41
5. lemma OAI.Brennan.Sharp.koebe_polar_left_lower line 48
6. lemma OAI.Brennan.Sharp.koebe_polar_right_lower line 56