OAI/Combinatorics/BalancedRyser/Profiles/ProfileDetection.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.ProfileDetection.tendsto_scaled_exponential_series line 18
  2. theorem OAI.Balanced.ProfileDetection.summable_exponential_series line 64
  3. theorem OAI.Balanced.ProfileDetection.analyticOnNhd_complex_exponential_series line 75
  4. theorem OAI.Balanced.ProfileDetection.analyticOnNhd_exponential_series line 97
  5. theorem OAI.Balanced.ProfileDetection.exists_least_supported_exponent line 122
  6. theorem OAI.Balanced.ProfileDetection.coefficients_zero_of_exponential_series_eventually_zero line 137
  7. theorem OAI.Balanced.ProfileDetection.exists_positive_exponential_series_ne_zero line 155
  8. theorem OAI.Balanced.ProfileDetection.exponential_series_ae_ne_zero line 170
  9. theorem OAI.Balanced.ProfileDetection.analyticOnNhd_log_exponential_series line 181
  10. theorem OAI.Balanced.ProfileDetection.log_exponential_series_ae_ne_zero line 198
  11. def OAI.Balanced.ProfileDetection.profileExponent line 213
  12. theorem OAI.Balanced.ProfileDetection.profileExponent_injective line 216
  13. theorem OAI.Balanced.ProfileDetection.profileExponent_finite_sublevel line 235
  14. theorem OAI.Balanced.ProfileDetection.profileExponent_nonneg line 252
  15. theorem OAI.Balanced.ProfileDetection.profile_power_series_ae_ne_zero line 256
  16. theorem OAI.Balanced.ProfileDetection.summable_profile_power_series line 269
  17. theorem OAI.Balanced.ProfileDetection.profile_power_series_ae_ne_of_ne line 281
  18. theorem OAI.Balanced.ProfileDetection.profile_coefficients_zero_of_eventually_zero line 305