OAI/Probability/ThorpRouting/Harmonic/ZeroExtend.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.sum_injections line 13
  2. def OAI.ThorpNine.Harmonic.Thorp.SparseContact.zeroExtend line 25
  3. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.zeroExtend_inj line 30
  4. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.zeroExtend_noninj line 36
  5. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.sum_zeroExtend_mul line 41
  6. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.norm_zeroExtend line 47
  7. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.partial_proper_zero line 55
  8. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.partial_full_action line 92
  9. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.alternating_retained_eq line 111
  10. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.alternating_harmonic_action line 121
  11. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.harmonic_action_bound line 150
  12. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.harmonic_action_zero_one line 188
  13. def OAI.ThorpNine.Harmonic.Thorp.SparseContact.MainStatement line 210
  14. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.exists_exact_fixed_unit line 226
  15. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.sweep_forward_norm line 247
  16. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.sweep_norm_le_one line 255
  17. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.sample_sweep_bound line 263
  18. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.sample_sweep_zero_one line 288
  19. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.sweep_norm_bound line 309
  20. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.sweep_zero_one line 329
  21. def OAI.ThorpNine.Harmonic.Thorp.SparseContact.contactConstant line 352
  22. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.contactConstant_gt_one line 354
  23. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.contactConstant_gt_two line 359
  24. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.inflated_contact_bound line 364
  25. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.contact_crude_arithmetic line 385
  26. lemma OAI.ThorpNine.Harmonic.Thorp.SparseContact.sweep_sharp_bound line 399
  27. theorem OAI.ThorpNine.Harmonic.Thorp.SparseContact.uniform_sparse_contact line 431
  28. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.log_factorial_upper_binary line 450
  29. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.log_factorial_lower line 470
  30. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.log_factorial_upper line 484
  31. def OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.fiberWeight line 501
  32. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.fiberWeight_nonneg line 504
  33. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.fiberWeight_pos line 507
  34. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.fiber_sum line 511
  35. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.sum_fiberWeight line 522
  36. theorem OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.incidence_entropy line 526
  37. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.log_factorial_upper_binary_all line 571
  38. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.log_fiber_factorials line 578
  39. theorem OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.dimension_log_from_incidence line 590
  40. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.scaled_binEntropy line 616
  41. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.log_choose_lower_entropy line 626
  42. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.binEntropy_three_quarters line 648
  43. def OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.entropyGap line 657
  44. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.entropyGap_pos line 659
  45. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.entropyGap_eq line 663
  46. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.binEntropy_tail_lower line 669
  47. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.log_dimension_from_binomial line 682
  48. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.balanced_dimension_coefficient_pos line 700
  49. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.log_choose_upper line 704
  50. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.log_choose_lower line 711
  51. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.footprint_log_bound line 719
  52. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.log_factorial_le_mul_log line 737
  53. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.near_row_log_dimension line 743
  54. def OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.nearPower line 773
  55. def OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.nearFraction line 774
  56. def OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.tailPower line 775
  57. def OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.chosenTuple line 777
  58. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.chosenTuple_bounds line 780
  59. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.chosenTuple_tail_lower line 804
  60. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.chosenTuple_log_footprint line 813
  61. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.near_row_log_uniform line 851