OAI/Analysis/IntegralMeans/CriticalCount.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Brennan.squaredReciprocalPotential line 21
  2. lemma OAI.Brennan.squaredReciprocalPotential_eq_sq line 24
  3. lemma OAI.Brennan.squaredReciprocalPotential_nonneg line 33
  4. lemma OAI.Brennan.contDiffAt_squaredReciprocalPotential line 38
  5. lemma OAI.Brennan.potential_ge_iff_reciprocalPotential_le line 46
  6. lemma OAI.Brennan.compact_squaredReciprocal_sublevel line 57
  7. lemma OAI.Brennan.regularizedGradient_formula line 80
  8. lemma OAI.Brennan.fderiv_squaredReciprocalPotential_apply line 98
  9. lemma OAI.Brennan.fderiv_squaredReciprocalPotential_eq_zero_iff line 119
  10. lemma OAI.Brennan.det_regularizedGradient_ne_zero line 140
  11. lemma OAI.Brennan.compact_convex_halfPlane_envelope line 157
  12. lemma OAI.Brennan.continuous_extension_near_compact line 168
  13. lemma OAI.Brennan.squaredReciprocalPotential_lt_windingInterior line 190
  14. lemma OAI.Brennan.regular_potential_level_index_sum line 211
  15. lemma OAI.Brennan.planeIndex_regularizedGradient_at_critical line 330
  16. lemma OAI.Brennan.critical_count_strict_sublevel line 353
  17. lemma OAI.Brennan.finite_critical_squared_sublevel line 435
  18. lemma OAI.Brennan.potential_ge_iff_squaredReciprocal_le line 448
  19. lemma OAI.Brennan.finset_gap_above line 456
  20. theorem OAI.Brennan.critical_count line 478
  21. theorem OAI.Brennan.criticalCountStatement_proved line 523