OAI/Combinatorics/Distances/PolynomialIsolation.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Polynomial separators, finite-point isolation and elementary bounds for distinct Euclidean distances.

  1. abbrev OAI.ErdosDistinctDistances.Point line 13
  2. def OAI.ErdosDistinctDistances.distances line 15
  3. theorem OAI.ErdosDistinctDistances.mem_distances line 21
  4. theorem OAI.ErdosDistinctDistances.coe_distances line 31
  5. theorem OAI.ErdosDistinctDistances.distance_pos line 37
  6. theorem OAI.ErdosDistinctDistances.zero_not_mem_distances line 41
  7. theorem OAI.ErdosDistinctDistances.distances_mono line 46
  8. theorem OAI.ErdosDistinctDistances.distances_nonempty line 51
  9. theorem OAI.ErdosDistinctDistances.one_le_card_distances line 56
  10. theorem OAI.ErdosDistinctDistances.failure_gives_regime line 59
  11. theorem OAI.ErdosDistinctDistances.regime_precludes_bound line 114
  12. def OAI.ErdosDistinctDistances.complexPoint line 130
  13. def OAI.ErdosDistinctDistances.squaredDistancePolynomial line 132
  14. theorem OAI.ErdosDistinctDistances.eval_squaredDistancePolynomial line 135
  15. theorem OAI.ErdosDistinctDistances.degree_squaredDistancePolynomial line 143
  16. def OAI.ErdosDistinctDistances.separatorFactor line 156
  17. def OAI.ErdosDistinctDistances.physicalSeparator line 160
  18. theorem OAI.ErdosDistinctDistances.degree_separatorFactor line 163
  19. theorem OAI.ErdosDistinctDistances.degree_physicalSeparator line 177
  20. theorem OAI.ErdosDistinctDistances.eval_physicalSeparator_self line 185
  21. theorem OAI.ErdosDistinctDistances.eval_physicalSeparator_ne line 194
  22. theorem OAI.ErdosDistinctDistances.eval_physicalSeparator line 201
  23. def OAI.ErdosDistinctDistances.isolationPolynomials line 209
  24. theorem OAI.ErdosDistinctDistances.degree_isolationPolynomials line 216
  25. theorem OAI.ErdosDistinctDistances.isolation_zero_iff line 237
  26. theorem OAI.ErdosDistinctDistances.linearIndependent_physicalSeparator line 278
  27. theorem OAI.ErdosDistinctDistances.finrank_restrictDegree line 295
  28. theorem OAI.ErdosDistinctDistances.elementary_card_bound line 317
  29. def OAI.ErdosDistinctDistances.lengthFiber line 330
  30. def OAI.ErdosDistinctDistances.equalLengthPairs line 334
  31. theorem OAI.ErdosDistinctDistances.sum_lengthFiber_card line 339
  32. theorem OAI.ErdosDistinctDistances.equalLengthPairs_card line 349
  33. theorem OAI.ErdosDistinctDistances.equalLengthPairs_lower_bound line 373
  34. theorem OAI.ErdosDistinctDistances.equalLengthPairs_lower_bound_real line 381