OAI/Probability/ThorpRouting/Adaptive/InsertionPerm.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.exists_near_cutoff line 14
  2. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.amplification_numerical line 40
  3. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.amplification_absorb line 58
  4. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.amplification_decay line 63
  5. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.full_tuple_fixed line 77
  6. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.full_tuple_finrank line 89
  7. theorem OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.palindrome_irrep_amplification line 93
  8. theorem OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.modified_irrep_amplification line 113
  9. theorem OAI.ThorpNine.Adaptive.Thorp.Specht.choose_tail_le_of_factorial line 134
  10. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.card_rowGroup_transpose line 167
  11. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.card_colGroup_transpose line 175
  12. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.card_transpose line 183
  13. theorem OAI.ThorpNine.Adaptive.Thorp.Specht.choose_column_tail_le_dimension line 187
  14. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.dimension_log_incidence line 197
  15. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.medium_dimension_raw line 218
  16. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.finset_power_sum line 274
  17. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.small_sets_count line 279
  18. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.small_sets_ceil_bound line 305
  19. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.exists_small_set_rate line 312
  20. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.log_error_eventually line 333
  21. theorem OAI.ThorpNine.Adaptive.Thorp.Specht.medium_dimension line 350
  22. lemma OAI.ThorpNine.Adaptive.Thorp.insertNth_castSucc_snoc line 373
  23. lemma OAI.ThorpNine.Adaptive.Thorp.rotate_cons line 388
  24. lemma OAI.ThorpNine.Adaptive.Thorp.rotate_insert line 391
  25. def OAI.ThorpNine.Adaptive.Thorp.insertionPerm line 395
  26. lemma OAI.ThorpNine.Adaptive.Thorp.insertionPerm_apply line 399
  27. lemma OAI.ThorpNine.Adaptive.Thorp.insertionPerm_zero line 402
  28. lemma OAI.ThorpNine.Adaptive.Thorp.insertionPerm_last line 406
  29. lemma OAI.ThorpNine.Adaptive.Thorp.physical_carry_step line 411
  30. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.sampleOperator_mul_const line 438
  31. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.sampleOperator_const_mul line 442
  32. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.sampleOperator_run line 446
  33. def OAI.ThorpNine.Adaptive.Thorp.carryCoins line 465
  34. lemma OAI.ThorpNine.Adaptive.Thorp.physical_carry_average line 473
  35. theorem OAI.ThorpNine.Adaptive.Thorp.physical_sweep_recursion line 492
  36. lemma OAI.ThorpNine.Adaptive.Thorp.childInjection_product line 525
  37. lemma OAI.ThorpNine.Adaptive.Thorp.childInjection_commute line 533
  38. lemma OAI.ThorpNine.Adaptive.Thorp.sampleOperator_child line 544
  39. lemma OAI.ThorpNine.Adaptive.Thorp.sampleOperator_child_commute line 560
  40. lemma OAI.ThorpNine.Adaptive.Thorp.inverse_butterfly_average_step line 567
  41. theorem OAI.ThorpNine.Adaptive.Thorp.physical_sweep_inverse_butterfly line 590
  42. lemma OAI.ThorpNine.Adaptive.Thorp.physical_sweep_adjoint line 604
  43. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.dimension_pos line 616
  44. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.near_numerical_cutoff line 623
  45. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.near_row_amplification line 646
  46. theorem OAI.ThorpNine.Adaptive.Thorp.Specht.near_row_spectral line 665
  47. theorem OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.full_palindrome_decay line 713
  48. theorem OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.full_modified_decay line 726
  49. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.palindrome_exception_cards line 737
  50. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.medium_parameters line 756
  51. lemma OAI.ThorpNine.Adaptive.Thorp.DimensionEstimates.geometric_ceil_bound line 770
  52. theorem OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.medium_exception_decay line 784
  53. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.partition_count line 834
  54. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.shapes_count line 839
  55. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.rowLens_headD line 843
  56. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.rowLens_tail_sum line 855
  57. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.positive_list_eq_of_tail_sum line 866