OAI/Probability/ThorpRouting/Adaptive/TupleKernel.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ThorpNine.Adaptive.Thorp.Casimir.applyKernel_mul line 11
  2. lemma OAI.ThorpNine.Adaptive.Thorp.Casimir.applyKernel_one line 27
  3. lemma OAI.ThorpNine.Adaptive.Thorp.Casimir.symmetric_hs_power line 34
  4. lemma OAI.ThorpNine.Adaptive.Thorp.Casimir.trace_power_le_hs line 48
  5. lemma OAI.ThorpNine.Adaptive.Thorp.Casimir.palindrome_selfadjoint line 74
  6. lemma OAI.ThorpNine.Adaptive.Thorp.Casimir.coefficient_trace_amplification line 82
  7. def OAI.ThorpNine.Adaptive.Thorp.Casimir.tupleKernel line 133
  8. lemma OAI.ThorpNine.Adaptive.Thorp.Casimir.palindrome_trace_amplification line 136
  9. lemma OAI.ThorpNine.Adaptive.Thorp.Casimir.tupleKernel_symm line 167
  10. lemma OAI.ThorpNine.Adaptive.Thorp.Casimir.tupleKernel_power64 line 171
  11. lemma OAI.ThorpNine.Adaptive.Thorp.Casimir.K_selfadjoint line 195
  12. lemma OAI.ThorpNine.Adaptive.Thorp.Casimir.K_norm_le_one line 199
  13. lemma OAI.ThorpNine.Adaptive.Thorp.Casimir.fixed_trace_bound line 203
  14. lemma OAI.ThorpNine.Adaptive.Thorp.Casimir.levelScale_ge line 226
  15. lemma OAI.ThorpNine.Adaptive.Thorp.Casimir.choose_le_exp_levelScale line 234
  16. lemma OAI.ThorpNine.Adaptive.Thorp.Casimir.trace_bound line 250
  17. lemma OAI.ThorpNine.Adaptive.Thorp.Casimir.levelScale_le line 285
  18. lemma OAI.ThorpNine.Adaptive.Thorp.Casimir.nontrivial_uniform_zero line 296
  19. lemma OAI.ThorpNine.Adaptive.Thorp.Casimir.gap_of_uniform_zero line 307
  20. lemma OAI.ThorpNine.Adaptive.Thorp.Casimir.nontrivial_gap line 315
  21. lemma OAI.ThorpNine.Adaptive.Thorp.Casimir.eventual_level_dimension line 320
  22. lemma OAI.ThorpNine.Adaptive.Thorp.Casimir.eventual_level_contraction line 358
  23. lemma OAI.ThorpNine.Adaptive.Thorp.Casimir.finite_positive_lower line 379
  24. theorem OAI.ThorpNine.Adaptive.Thorp.Casimir.level_contraction line 391
  25. def OAI.ThorpNine.Adaptive.Thorp.Specht.cardLabels line 430
  26. def OAI.ThorpNine.Adaptive.Thorp.Specht.cardRepresentation line 433
  27. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.cardRepresentation_unitary line 437
  28. instance OAI.ThorpNine.Adaptive.Thorp.Specht.cardRepresentation_irreducible line 441
  29. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.relabelledUnitary_neq line 445
  30. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.cardRepresentation_distinct line 470
  31. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.card_conjugacy_shapes line 475
  32. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.row_zero_of_full_row line 480
  33. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.tabloid_subsingleton_of_full_row line 486
  34. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.representation_full_row line 497
  35. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.relabelled_full_row line 507
  36. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.sample_uniform_left line 518
  37. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.uniform_zero_of_sample_norm_lt_one line 522
  38. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.sampleOperator_trivial line 530
  39. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.uniformOperator_trivial line 542
  40. lemma OAI.ThorpNine.Adaptive.Thorp.UnitaryFinite.weighted_sub line 547
  41. lemma OAI.ThorpNine.Adaptive.Thorp.physical_palindrome_norm line 558
  42. lemma OAI.ThorpNine.Adaptive.Thorp.physical_power_bound line 567
  43. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.card_fourier_decay line 585
  44. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.card_fourier_tall line 618
  45. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.card_fourier_full_row line 634
  46. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.half_geom_sum line 643
  47. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.shape_weight_sum line 651
  48. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.near_shape_term line 671
  49. lemma OAI.ThorpNine.Adaptive.Thorp.Specht.shapes_medium_sum line 693
  50. lemma OAI.ThorpNine.Adaptive.Thorp.sampleLaw_run line 718
  51. lemma OAI.ThorpNine.Adaptive.Thorp.physical_fourier_bound line 729
  52. theorem OAI.ThorpNine.Adaptive.Thorp.eventual_physical_bound line 755
  53. lemma OAI.ThorpNine.Adaptive.Thorp.physical_convergence line 823
  54. lemma OAI.ThorpNine.Adaptive.Thorp.Casimir.K_source_square line 848
  55. lemma OAI.ThorpNine.Adaptive.Thorp.Casimir.density_bound line 857
  56. lemma OAI.ThorpNine.Adaptive.Thorp.Casimir.fromDistance_eq line 872
  57. lemma OAI.ThorpNine.Adaptive.Thorp.Casimir.trace_real line 877