OAI/Analysis/IntegralMeans/LevelIndex.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Brennan.sum_loopIndex_sublevel line 21
2. lemma OAI.Brennan.windingNumber_normal_field line 92
3. lemma OAI.Brennan.periodic_simple_eq_of_near line 140
4. lemma OAI.Brennan.periodic_simple_shift line 156
5. lemma OAI.Brennan.periodic_simple_reverse line 166
6. lemma OAI.Brennan.orient_unit_curve line 176
7. lemma OAI.Brennan.orient_periodic_curve line 235
8. lemma OAI.Brennan.regular_level_index_sum line 263
9. def OAI.Brennan.tangentGradient line 325
10. lemma OAI.Brennan.tangentGradient_orthogonal line 328
11. lemma OAI.Brennan.tangentGradient_ne_zero line 336
12. lemma OAI.Brennan.tangentGradient_contDiff line 350
13. lemma OAI.Brennan.tangentGradient_hasCompactSupport line 356
14. lemma OAI.Brennan.compact_regular_level_oriented_curves line 368
15. lemma OAI.Brennan.loopIndex_zero_of_im_lt line 391
16. lemma OAI.Brennan.closure_windingInterior_subset_halfPlane line 404
17. lemma OAI.Brennan.reciprocalPotential_lt_on_windingInterior line 419
18. lemma OAI.Brennan.extend_compact_sublevel line 431