OAI/Probability/ThorpRouting/Casimir/ZeroExtend.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.sum_injections line 13
  2. def OAI.ThorpNine.Casimir.Thorp.SparseContact.zeroExtend line 25
  3. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.zeroExtend_inj line 30
  4. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.zeroExtend_noninj line 36
  5. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.sum_zeroExtend_mul line 41
  6. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.norm_zeroExtend line 47
  7. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.partial_proper_zero line 55
  8. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.partial_full_action line 92
  9. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.alternating_retained_eq line 111
  10. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.alternating_harmonic_action line 121
  11. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.harmonic_action_bound line 150
  12. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.harmonic_action_zero_one line 188
  13. def OAI.ThorpNine.Casimir.Thorp.SparseContact.sweepOperator line 210
  14. def OAI.ThorpNine.Casimir.Thorp.SparseContact.MainStatement line 217
  15. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.exists_exact_fixed_unit line 233
  16. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.sweep_forward_norm line 254
  17. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.sweep_norm_le_one line 262
  18. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.sample_sweep_bound line 270
  19. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.sample_sweep_zero_one line 295
  20. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.sweep_norm_bound line 316
  21. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.sweep_zero_one line 336
  22. def OAI.ThorpNine.Casimir.Thorp.SparseContact.contactConstant line 359
  23. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.contactConstant_gt_one line 361
  24. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.contactConstant_gt_two line 366
  25. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.inflated_contact_bound line 371
  26. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.contact_crude_arithmetic line 392
  27. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.sweep_sharp_bound line 406
  28. theorem OAI.ThorpNine.Casimir.Thorp.SparseContact.uniform_sparse_contact line 438
  29. lemma OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.log_factorial_upper_binary line 457
  30. lemma OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.log_factorial_lower line 477
  31. lemma OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.log_factorial_upper line 491
  32. def OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.fiberWeight line 508
  33. lemma OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.fiberWeight_nonneg line 511
  34. lemma OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.fiberWeight_pos line 514
  35. lemma OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.fiber_sum line 518
  36. lemma OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.sum_fiberWeight line 529
  37. theorem OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.incidence_entropy line 533
  38. lemma OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.log_factorial_upper_binary_all line 578
  39. lemma OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.log_fiber_factorials line 585
  40. theorem OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.dimension_log_from_incidence line 597
  41. lemma OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.scaled_binEntropy line 623
  42. lemma OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.log_choose_lower_entropy line 633
  43. lemma OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.binEntropy_three_quarters line 655
  44. def OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.entropyGap line 664
  45. lemma OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.entropyGap_pos line 666
  46. lemma OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.entropyGap_eq line 670
  47. lemma OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.binEntropy_tail_lower line 676
  48. lemma OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.log_dimension_from_binomial line 689
  49. lemma OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.balanced_dimension_coefficient_pos line 707
  50. lemma OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.log_choose_upper line 711
  51. lemma OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.log_choose_lower line 718
  52. lemma OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.footprint_log_bound line 726
  53. lemma OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.log_factorial_le_mul_log line 744
  54. lemma OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.near_row_log_dimension line 750
  55. def OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.nearPower line 780
  56. def OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.nearFraction line 781
  57. def OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.tailPower line 782
  58. def OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.chosenTuple line 784
  59. lemma OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.chosenTuple_bounds line 787
  60. lemma OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.chosenTuple_tail_lower line 811
  61. lemma OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.chosenTuple_log_footprint line 820
  62. lemma OAI.ThorpNine.Casimir.Thorp.DimensionEstimates.near_row_log_uniform line 858