OAI/Geometry/UnitDistances/Regularization.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarUnitDistances.IncidenceRegularization.mass line 8
  2. def OAI.PlanarUnitDistances.IncidenceRegularization.rect line 9
  3. lemma OAI.PlanarUnitDistances.IncidenceRegularization.mass_nonneg line 12
  4. lemma OAI.PlanarUnitDistances.IncidenceRegularization.mass_mono line 14
  5. lemma OAI.PlanarUnitDistances.IncidenceRegularization.rect_nonneg line 17
  6. def OAI.PlanarUnitDistances.IncidenceRegularization.objective line 25
  7. def OAI.PlanarUnitDistances.IncidenceRegularization.IsMaximizing line 28
  8. theorem OAI.PlanarUnitDistances.IncidenceRegularization.exists_maximizing line 35
  9. lemma OAI.PlanarUnitDistances.IncidenceRegularization.winner_positive line 55
  10. theorem OAI.PlanarUnitDistances.IncidenceRegularization.feasible_expansion line 69
  11. theorem OAI.PlanarUnitDistances.IncidenceRegularization.left_atom_bound line 91
  12. lemma OAI.PlanarUnitDistances.IncidenceRegularization.mass_le_one line 122
  13. lemma OAI.PlanarUnitDistances.IncidenceRegularization.transpose_maximizing line 127
  14. theorem OAI.PlanarUnitDistances.IncidenceRegularization.right_atom_bound line 138
  15. lemma OAI.PlanarUnitDistances.IncidenceRegularization.min_le_geometric line 151
  16. theorem OAI.PlanarUnitDistances.IncidenceRegularization.preliminary_square_root line 163
  17. lemma OAI.PlanarUnitDistances.IncidenceRegularization.renormalized_preliminary line 202
  18. theorem OAI.PlanarUnitDistances.IncidenceRegularization.maximizing_expansion line 226
  19. def OAI.PlanarUnitDistances.GeometricExpansion.factor line 309
  20. lemma OAI.PlanarUnitDistances.GeometricExpansion.factor_bounds line 313
  21. lemma OAI.PlanarUnitDistances.GeometricExpansion.incidence_degree_le line 337
  22. theorem OAI.PlanarUnitDistances.GeometricExpansion.preliminary line 343
  23. def OAI.PlanarUnitDistances.GeometricOptimizer.lift line 447
  24. lemma OAI.PlanarUnitDistances.GeometricOptimizer.lift_card line 448
  25. lemma OAI.PlanarUnitDistances.GeometricOptimizer.lift_subset line 449
  26. lemma OAI.PlanarUnitDistances.GeometricOptimizer.lift_univ line 453
  27. lemma OAI.PlanarUnitDistances.GeometricOptimizer.lift_subtype line 456
  28. lemma OAI.PlanarUnitDistances.GeometricOptimizer.subtype_subset line 459
  29. def OAI.PlanarUnitDistances.GeometricOptimizer.counting line 467
  30. def OAI.PlanarUnitDistances.GeometricOptimizer.weight line 468
  31. lemma OAI.PlanarUnitDistances.GeometricOptimizer.counting_mass line 470
  32. lemma OAI.PlanarUnitDistances.GeometricOptimizer.weight_rect line 473
  33. lemma OAI.PlanarUnitDistances.GeometricOptimizer.weight_row line 480
  34. theorem OAI.PlanarUnitDistances.GeometricOptimizer.exists_rectangle line 484
  35. lemma OAI.PlanarUnitDistances.IncidenceRegularization.winning_product line 611
  36. lemma OAI.PlanarUnitDistances.IncidenceRegularization.winning_product_lower line 643
  37. lemma OAI.PlanarUnitDistances.OptimizerPowers.factor_upper line 667
  38. theorem OAI.PlanarUnitDistances.OptimizerPowers.winning_powers line 705
  39. lemma OAI.PlanarUnitDistances.RegularizedPiece.eventually_choose line 805
  40. theorem OAI.PlanarUnitDistances.RegularizedPiece.regularize line 813