OAI/Probability/ThorpRouting/Adaptive/MainStatement.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.partial_full_action line 13
  2. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.alternating_retained_eq line 32
  3. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.alternating_harmonic_action line 42
  4. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.harmonic_action_bound line 71
  5. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.harmonic_action_zero_one line 109
  6. def OAI.ThorpNine.Adaptive.Thorp.SparseContact.MainStatement line 131
  7. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.exists_exact_fixed_unit line 147
  8. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.sweep_forward_norm line 168
  9. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.sweep_norm_le_one line 176
  10. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.sample_sweep_bound line 184
  11. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.sample_sweep_zero_one line 209
  12. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.sweep_norm_bound line 230
  13. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.sweep_zero_one line 250
  14. def OAI.ThorpNine.Adaptive.Thorp.SparseContact.contactConstant line 273
  15. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.contactConstant_gt_one line 275
  16. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.contactConstant_gt_two line 280
  17. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.inflated_contact_bound line 285
  18. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.contact_crude_arithmetic line 306
  19. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.sweep_sharp_bound line 320
  20. theorem OAI.ThorpNine.Adaptive.Thorp.SparseContact.uniform_sparse_contact line 352
  21. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.log_factorial_upper_binary line 371
  22. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.log_factorial_lower line 391
  23. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.log_factorial_upper line 405
  24. def OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.fiberWeight line 422
  25. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.fiberWeight_nonneg line 425
  26. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.fiberWeight_pos line 428
  27. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.fiber_sum line 432
  28. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.sum_fiberWeight line 443
  29. theorem OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.incidence_entropy line 447
  30. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.log_factorial_upper_binary_all line 492
  31. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.log_fiber_factorials line 499
  32. theorem OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.dimension_log_from_incidence line 511
  33. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.scaled_binEntropy line 537
  34. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.log_choose_lower_entropy line 547
  35. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.binEntropy_three_quarters line 569
  36. def OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.entropyGap line 578
  37. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.entropyGap_pos line 580
  38. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.entropyGap_eq line 584
  39. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.binEntropy_tail_lower line 590
  40. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.log_dimension_from_binomial line 603
  41. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.balanced_dimension_coefficient_pos line 621
  42. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.log_choose_upper line 625
  43. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.log_choose_lower line 632
  44. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.footprint_log_bound line 640
  45. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.log_factorial_le_mul_log line 658
  46. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.near_row_log_dimension line 664
  47. def OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.nearPower line 694
  48. def OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.nearFraction line 695
  49. def OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.tailPower line 696
  50. def OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.chosenTuple line 698
  51. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.chosenTuple_bounds line 701
  52. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.chosenTuple_tail_lower line 725
  53. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.chosenTuple_log_footprint line 734
  54. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.near_row_log_uniform line 772
  55. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.chosenTuple_density_bound line 789
  56. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.near_conditions_eventually line 826