OAI/MeasureTheory/SelfSimilar/FairPairs.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.EntropyRateDimension.FairPairs.Law line 14
  2. def OAI.EntropyRateDimension.FairPairs.Law.edges line 20
  3. def OAI.EntropyRateDimension.FairPairs.incident line 25
  4. def OAI.EntropyRateDimension.FairPairs.Feasible line 30
  5. def OAI.EntropyRateDimension.FairPairs.capacity line 33
  6. theorem OAI.EntropyRateDimension.FairPairs.edge_mem_left line 36
  7. theorem OAI.EntropyRateDimension.FairPairs.edge_mem_right line 40
  8. theorem OAI.EntropyRateDimension.FairPairs.incident_sum line 44
  9. theorem OAI.EntropyRateDimension.FairPairs.feasible_zero line 55
  10. theorem OAI.EntropyRateDimension.FairPairs.total_nonneg line 61
  11. theorem OAI.EntropyRateDimension.FairPairs.total_le_one line 65
  12. theorem OAI.EntropyRateDimension.FairPairs.weight_le_one line 70
  13. theorem OAI.EntropyRateDimension.FairPairs.totals_nonempty line 74
  14. theorem OAI.EntropyRateDimension.FairPairs.totals_bddAbove line 78
  15. theorem OAI.EntropyRateDimension.FairPairs.capacity_nonneg line 84
  16. theorem OAI.EntropyRateDimension.FairPairs.capacity_le_one line 88
  17. theorem OAI.EntropyRateDimension.FairPairs.total_le_capacity line 93
  18. theorem OAI.EntropyRateDimension.FairPairs.capacity_eq_zero_of_edges_eq_empty line 97
  19. theorem OAI.EntropyRateDimension.FairPairs.feasible_isClosed line 105
  20. theorem OAI.EntropyRateDimension.FairPairs.feasible_isCompact line 124
  21. theorem OAI.EntropyRateDimension.FairPairs.capacity_attained line 131
  22. theorem OAI.EntropyRateDimension.FairPairs.sum_first_endpoint line 141
  23. theorem OAI.EntropyRateDimension.FairPairs.sum_second_endpoint line 152
  24. theorem OAI.EntropyRateDimension.FairPairs.coupling_incident line 163
  25. theorem OAI.EntropyRateDimension.FairPairs.coupling_band_le_capacity line 189
  26. def OAI.EntropyRateDimension.FairPairs.bandIndex line 218
  27. theorem OAI.EntropyRateDimension.FairPairs.bandIndex_eq line 220
  28. theorem OAI.EntropyRateDimension.FairPairs.capacity_eq_zero_outside_pair_bands line 235
  29. theorem OAI.EntropyRateDimension.FairPairs.exists_capacity_cutoff line 246
  30. def OAI.EntropyRateDimension.FairPairs.conditionalCoupling line 257
  31. theorem OAI.EntropyRateDimension.FairPairs.cell_mass_pos line 261
  32. theorem OAI.EntropyRateDimension.FairPairs.conditionalCoupling_nonneg line 270
  33. theorem OAI.EntropyRateDimension.FairPairs.conditionalCoupling_symm line 279
  34. theorem OAI.EntropyRateDimension.FairPairs.conditionalCoupling_row line 286
  35. theorem OAI.EntropyRateDimension.FairPairs.conditionalCoupling_eq_zero_of_ne line 298
  36. theorem OAI.EntropyRateDimension.FairPairs.deviation_le_pair_distance line 303
  37. theorem OAI.EntropyRateDimension.FairPairs.mem_bandIndex line 321
  38. theorem OAI.EntropyRateDimension.FairPairs.coupling_distance_le line 333
  39. theorem OAI.EntropyRateDimension.FairPairs.geometric_fine_scale_bound line 390