OAI/Geometry/UnitDistances/Obstruction.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PlanarUnitDistances.PolynomialBlocks.natDegree_eval₂_le line 9
  2. lemma OAI.PlanarUnitDistances.PolynomialBlocks.unique_natDegree_le line 24
  3. lemma OAI.PlanarUnitDistances.PolynomialBlocks.unique_eval line 30
  4. abbrev OAI.PlanarUnitDistances.PolynomialBlocks.bivar line 43
  5. lemma OAI.PlanarUnitDistances.PolynomialBlocks.bivar_eval line 46
  6. lemma OAI.PlanarUnitDistances.PolynomialBlocks.bivar_natDegree_le line 57
  7. lemma OAI.PlanarUnitDistances.PolynomialBlocks.swap_bivar line 67
  8. lemma OAI.PlanarUnitDistances.PolynomialBlocks.swap_bivar_natDegree_le line 79
  9. lemma OAI.PlanarUnitDistances.PolynomialBlocks.unique_zeros_card_le line 88
  10. def OAI.PlanarUnitDistances.FiniteGraphPruning.mass line 111
  11. lemma OAI.PlanarUnitDistances.FiniteGraphPruning.mass_nonneg line 114
  12. lemma OAI.PlanarUnitDistances.FiniteGraphPruning.mass_mono line 118
  13. theorem OAI.PlanarUnitDistances.FiniteGraphPruning.prune line 127
  14. lemma OAI.PlanarUnitDistances.DenseLoci.mass_swap line 191
  15. lemma OAI.PlanarUnitDistances.DenseLoci.mass_le_card_mul line 195
  16. lemma OAI.PlanarUnitDistances.DenseLoci.cards_pos_of_mass_pos line 202
  17. lemma OAI.PlanarUnitDistances.DenseLoci.prune_nonneg line 212
  18. lemma OAI.PlanarUnitDistances.DenseLoci.mass_restrict_lower line 228
  19. theorem OAI.PlanarUnitDistances.DenseLoci.sequence_prune line 235
  20. lemma OAI.PlanarUnitDistances.DenseLoci.upper_card_subset line 263
  21. lemma OAI.PlanarUnitDistances.DenseLoci.lower_card_of_dense line 268
  22. def OAI.PlanarUnitDistances.DenseLoci.Uniform line 286
  23. def OAI.PlanarUnitDistances.DenseLoci.OnCurve line 290
  24. def OAI.PlanarUnitDistances.DenseLoci.Controlled line 295
  25. lemma OAI.PlanarUnitDistances.DenseLoci.Controlled.mono line 298
  26. theorem OAI.PlanarUnitDistances.DenseLoci.control_left line 313
  27. theorem OAI.PlanarUnitDistances.DenseLoci.controlled_subsets line 333
  28. lemma OAI.PlanarUnitDistances.LocusBlocks.plane_zeros_card line 379
  29. theorem OAI.PlanarUnitDistances.LocusBlocks.plane_uniformBlocks line 394
  30. theorem OAI.PlanarUnitDistances.LocusBlocks.curve_uniformBlocks line 414
  31. def OAI.PlanarUnitDistances.AlgebraicObstruction.indicator line 433
  32. lemma OAI.PlanarUnitDistances.AlgebraicObstruction.mass_indicator line 437
  33. abbrev OAI.PlanarUnitDistances.AlgebraicObstruction.z line 450
  34. abbrev OAI.PlanarUnitDistances.AlgebraicObstruction.w line 451
  35. lemma OAI.PlanarUnitDistances.AlgebraicObstruction.single_independent line 454
  36. lemma OAI.PlanarUnitDistances.AlgebraicObstruction.locus_root_descend line 460
  37. structure OAI.PlanarUnitDistances.AlgebraicObstruction.Hypotheses line 479
  38. lemma OAI.PlanarUnitDistances.AlgebraicObstruction.grid_labels line 493
  39. lemma OAI.PlanarUnitDistances.AlgebraicObstruction.plane line 542
  40. lemma OAI.PlanarUnitDistances.AlgebraicObstruction.curve_plane line 586
  41. lemma OAI.PlanarUnitDistances.AlgebraicObstruction.map_circle line 634
  42. lemma OAI.PlanarUnitDistances.AlgebraicObstruction.curve_curve line 654
  43. theorem OAI.PlanarUnitDistances.AlgebraicObstruction.no_rectangles line 746