OAI/Probability/ThorpRouting/Harmonic/InsertionPerm.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.chosenTuple_density_bound line 14
  2. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.near_conditions_eventually line 51
  3. theorem OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.exists_near_cutoff line 71
  4. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.amplification_numerical line 97
  5. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.amplification_absorb line 115
  6. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.amplification_decay line 120
  7. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.full_tuple_fixed line 134
  8. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.full_tuple_finrank line 146
  9. theorem OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.palindrome_irrep_amplification line 150
  10. theorem OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.modified_irrep_amplification line 170
  11. theorem OAI.ThorpNine.Harmonic.Thorp.Specht.choose_tail_le_of_factorial line 191
  12. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.card_rowGroup_transpose line 224
  13. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.card_colGroup_transpose line 232
  14. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.card_transpose line 240
  15. theorem OAI.ThorpNine.Harmonic.Thorp.Specht.choose_column_tail_le_dimension line 244
  16. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.dimension_log_incidence line 254
  17. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.medium_dimension_raw line 275
  18. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.finset_power_sum line 331
  19. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.small_sets_count line 336
  20. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.small_sets_ceil_bound line 362
  21. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.exists_small_set_rate line 369
  22. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.log_error_eventually line 390
  23. theorem OAI.ThorpNine.Harmonic.Thorp.Specht.medium_dimension line 407
  24. lemma OAI.ThorpNine.Harmonic.Thorp.insertNth_castSucc_snoc line 430
  25. lemma OAI.ThorpNine.Harmonic.Thorp.rotate_cons line 445
  26. lemma OAI.ThorpNine.Harmonic.Thorp.rotate_insert line 448
  27. def OAI.ThorpNine.Harmonic.Thorp.insertionPerm line 452
  28. lemma OAI.ThorpNine.Harmonic.Thorp.insertionPerm_apply line 456
  29. lemma OAI.ThorpNine.Harmonic.Thorp.insertionPerm_zero line 459
  30. lemma OAI.ThorpNine.Harmonic.Thorp.insertionPerm_last line 463
  31. lemma OAI.ThorpNine.Harmonic.Thorp.physical_carry_step line 468
  32. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.sampleOperator_mul_const line 495
  33. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.sampleOperator_const_mul line 499
  34. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.sampleOperator_run line 503
  35. def OAI.ThorpNine.Harmonic.Thorp.carryCoins line 522
  36. lemma OAI.ThorpNine.Harmonic.Thorp.physical_carry_average line 530
  37. theorem OAI.ThorpNine.Harmonic.Thorp.physical_sweep_recursion line 549
  38. lemma OAI.ThorpNine.Harmonic.Thorp.childInjection_product line 582
  39. lemma OAI.ThorpNine.Harmonic.Thorp.childInjection_commute line 590
  40. lemma OAI.ThorpNine.Harmonic.Thorp.sampleOperator_child line 601
  41. lemma OAI.ThorpNine.Harmonic.Thorp.sampleOperator_child_commute line 617
  42. lemma OAI.ThorpNine.Harmonic.Thorp.inverse_butterfly_average_step line 624
  43. theorem OAI.ThorpNine.Harmonic.Thorp.physical_sweep_inverse_butterfly line 647
  44. lemma OAI.ThorpNine.Harmonic.Thorp.physical_sweep_adjoint line 661
  45. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.dimension_pos line 673
  46. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.near_numerical_cutoff line 680
  47. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.near_row_amplification line 703
  48. theorem OAI.ThorpNine.Harmonic.Thorp.Specht.near_row_spectral line 722
  49. theorem OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.full_palindrome_decay line 770
  50. theorem OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.full_modified_decay line 783
  51. lemma OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.palindrome_exception_cards line 794
  52. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.medium_parameters line 813
  53. lemma OAI.ThorpNine.Harmonic.Thorp.DimensionEstimates.geometric_ceil_bound line 827
  54. theorem OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.medium_exception_decay line 841