OAI/Analysis/IntegralMeans/CompactClass.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.Brennan.(instance at line 21) line 21
2. lemma OAI.Brennan.compact_closure_of_disk_bounds line 23
3. def OAI.Brennan.diskExtend line 53
4. lemma OAI.Brennan.diskExtend_apply line 56
5. lemma OAI.Brennan.diskExtend_convergence line 59
6. def OAI.Brennan.diskSchlichtSet line 66
7. lemma OAI.Brennan.isClosed_diskSchlichtSet line 68
8. lemma OAI.Brennan.isCompact_diskSchlichtSet line 94
9. def OAI.Brennan.DiskClass line 107
10. instance OAI.Brennan.(instance at line 109) line 109
11. instance OAI.Brennan.(instance at line 111) line 111
12. lemma OAI.Brennan.differentiableOn_iteratedDeriv_disk line 113
13. lemma OAI.Brennan.tendstoLocallyUniformlyOn_iteratedDeriv_disk line 119
14. def OAI.Brennan.diskClassJet line 130
15. lemma OAI.Brennan.continuous_diskClassJet line 135
16. lemma OAI.Brennan.continuous_diskClassJet_eval line 144