OAI/Analysis/SymmetricDomains/PolynomialIntegralCoordinates.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Release061.unit_disc_sum_eq_card line 9
  2. theorem OAI.Release061.locally_uniform_subsequence_of_equicontinuous line 26
  3. theorem OAI.Release061.equicontinuous_of_bounded_differentiableOn line 65
  4. theorem OAI.Release061.maximum_propagation_on_ball line 92
  5. theorem OAI.Release061.eq_one_of_local_maximum_propagation line 128
  6. theorem OAI.Release061.maximum_propagation_on_open_connected line 139
  7. theorem OAI.Release061.peak_distance_lt line 161
  8. theorem OAI.Release061.peak_localization line 171
  9. theorem OAI.Release061.exists_polynomial_integral_coordinates line 186