OAI/Geometry/UnitDistances/Entropy.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarUnitDistances.IncidenceEntropy.entropy line 9
  2. lemma OAI.PlanarUnitDistances.IncidenceEntropy.atom_le_one line 12
  3. lemma OAI.PlanarUnitDistances.IncidenceEntropy.entropy_nonneg line 17
  4. lemma OAI.PlanarUnitDistances.IncidenceEntropy.entropy_le_log_card line 25
  5. lemma OAI.PlanarUnitDistances.IncidenceEntropy.entropy_off_diagonal_bound line 49
  6. lemma OAI.PlanarUnitDistances.IncidenceEntropy.joint_KL_entropy line 77
  7. theorem OAI.PlanarUnitDistances.IncidenceEntropy.mutual_information_bound line 112
  8. def OAI.PlanarUnitDistances.IncidenceEntropy.indicator line 127
  9. def OAI.PlanarUnitDistances.IncidenceEntropy.degree line 130
  10. def OAI.PlanarUnitDistances.IncidenceEntropy.edgeCount line 131
  11. def OAI.PlanarUnitDistances.IncidenceEntropy.wedge line 132
  12. def OAI.PlanarUnitDistances.IncidenceEntropy.pointLaw line 134
  13. lemma OAI.PlanarUnitDistances.IncidenceEntropy.indicator_nonneg line 138
  14. lemma OAI.PlanarUnitDistances.IncidenceEntropy.degree_nonneg line 144
  15. lemma OAI.PlanarUnitDistances.IncidenceEntropy.edgeCount_nonneg line 147
  16. lemma OAI.PlanarUnitDistances.IncidenceEntropy.wedge_nonneg line 150
  17. lemma OAI.PlanarUnitDistances.IncidenceEntropy.wedge_symm line 156
  18. lemma OAI.PlanarUnitDistances.IncidenceEntropy.pointLaw_sum line 162
  19. lemma OAI.PlanarUnitDistances.IncidenceEntropy.wedge_fst line 167
  20. lemma OAI.PlanarUnitDistances.IncidenceEntropy.wedge_snd line 178
  21. lemma OAI.PlanarUnitDistances.IncidenceEntropy.wedge_sum line 183
  22. theorem OAI.PlanarUnitDistances.IncidenceEntropy.wedge_diagonal line 189
  23. theorem OAI.PlanarUnitDistances.IncidenceEntropy.wedge_atom line 206
  24. theorem OAI.PlanarUnitDistances.IncidenceEntropy.wedge_information line 221
  25. lemma OAI.PlanarUnitDistances.UnitCodegree.center_linear line 244
  26. def OAI.PlanarUnitDistances.UnitCodegree.centerPolynomial line 250
  27. lemma OAI.PlanarUnitDistances.UnitCodegree.centerPolynomial_eval line 253
  28. lemma OAI.PlanarUnitDistances.UnitCodegree.centerPolynomial_expansion line 261
  29. lemma OAI.PlanarUnitDistances.UnitCodegree.centerPolynomial_ne_zero line 268
  30. lemma OAI.PlanarUnitDistances.UnitCodegree.centerPolynomial_degree line 276
  31. theorem OAI.PlanarUnitDistances.UnitCodegree.common_centers_card line 286
  32. lemma OAI.PlanarUnitDistances.UnitCodegree.unit_distance_equation line 296
  33. theorem OAI.PlanarUnitDistances.UnitCodegree.unit_centers_card line 301
  34. def OAI.PlanarUnitDistances.UnitCodegree.zCoordinate line 306
  35. lemma OAI.PlanarUnitDistances.UnitCodegree.zCoordinate_apply line 309
  36. theorem OAI.PlanarUnitDistances.IncidenceEntropy.unit_incidence_codegree line 320
  37. theorem OAI.PlanarUnitDistances.IncidenceEntropy.planar_wedge_information line 343
  38. def OAI.PlanarUnitDistances.UniformGraphLaw.law line 368
  39. lemma OAI.PlanarUnitDistances.UniformGraphLaw.right_eq line 377
  40. lemma OAI.PlanarUnitDistances.UniformGraphLaw.left_eq line 381
  41. lemma OAI.PlanarUnitDistances.UniformGraphLaw.col_eq line 385
  42. lemma OAI.PlanarUnitDistances.UniformGraphLaw.row_eq line 391
  43. lemma OAI.PlanarUnitDistances.UniformGraphLaw.wedge_val line 398
  44. theorem OAI.PlanarUnitDistances.UniformGraphLaw.edge_count line 406
  45. abbrev OAI.PlanarUnitDistances.GeometricLaw.Plane line 455
  46. def OAI.PlanarUnitDistances.GeometricLaw.E line 456
  47. lemma OAI.PlanarUnitDistances.GeometricLaw.degree_eq line 457
  48. lemma OAI.PlanarUnitDistances.GeometricLaw.edgeCount_eq line 461
  49. lemma OAI.PlanarUnitDistances.GeometricLaw.row_count line 464
  50. lemma OAI.PlanarUnitDistances.GeometricLaw.card_pos line 470
  51. def OAI.PlanarUnitDistances.GeometricLaw.graph line 476
  52. lemma OAI.PlanarUnitDistances.GeometricLaw.left_eq line 478
  53. lemma OAI.PlanarUnitDistances.GeometricLaw.right_eq line 481
  54. lemma OAI.PlanarUnitDistances.GeometricLaw.row_le line 484
  55. def OAI.PlanarUnitDistances.GeometricLaw.counting line 492
  56. lemma OAI.PlanarUnitDistances.GeometricLaw.counting_event line 496
  57. def OAI.PlanarUnitDistances.GeometricLaw.image line 501
  58. lemma OAI.PlanarUnitDistances.GeometricLaw.image_sub line 502
  59. lemma OAI.PlanarUnitDistances.GeometricLaw.image_card line 506
  60. lemma OAI.PlanarUnitDistances.GeometricLaw.event_eq line 508
  61. theorem OAI.PlanarUnitDistances.GeometricLaw.expansion line 534
  62. lemma OAI.PlanarUnitDistances.GeometricLaw.wedge_eq line 548
  63. theorem OAI.PlanarUnitDistances.GeometricLaw.information line 562
  64. lemma OAI.PlanarUnitDistances.PowerGrowth.Upper.log_ratio line 582
  65. lemma OAI.PlanarUnitDistances.PowerGrowth.Lower.log_ratio line 589
  66. theorem OAI.PlanarUnitDistances.InformationPowers.information_rate line 600
  67. lemma OAI.PlanarUnitDistances.PowerGrowth.Upper.power_bound line 643
  68. lemma OAI.PlanarUnitDistances.PowerGrowth.Lower.power_bound line 646
  69. lemma OAI.PlanarUnitDistances.PowerGrowth.Lower.tends_to_infinity line 649