OAI/Probability/BinarySweep/Mixing/ShapeDimension.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BinaryCoordinateSweeps.Young.rowLen_one_le_tail line 15
  2. lemma OAI.BinaryCoordinateSweeps.Young.rowLen_one_pos_of_tail line 29
  3. lemma OAI.BinaryCoordinateSweeps.Young.longOriented_dimension line 38
  4. lemma OAI.BinaryCoordinateSweeps.Young.dimension_grows line 45
  5. lemma OAI.BinaryCoordinateSweeps.Young.partition_dimension_pos line 60
  6. lemma OAI.BinaryCoordinateSweeps.Young.partition_dimension_grows line 64
  7. lemma OAI.BinaryCoordinateSweeps.Young.partition_log_lower line 71
  8. lemma OAI.BinaryCoordinateSweeps.Young.partition_dimension_gt_one line 76
  9. lemma OAI.BinaryCoordinateSweeps.Young.row_shape_cells line 89
  10. lemma OAI.BinaryCoordinateSweeps.Young.row_shape_tabloid line 98
  11. lemma OAI.BinaryCoordinateSweeps.Young.hilbertSpecht_row line 105
  12. lemma OAI.BinaryCoordinateSweeps.Young.row_average_zero line 112
  13. lemma OAI.BinaryCoordinateSweeps.Young.transpose_slot_moment line 121
  14. theorem OAI.BinaryCoordinateSweeps.Young.flat_shape_moment_zero line 136
  15. lemma OAI.BinaryCoordinateSweeps.sign_convolution line 162
  16. lemma OAI.BinaryCoordinateSweeps.sweep_sign_zero line 181
  17. lemma OAI.BinaryCoordinateSweeps.sweep_centered_mass line 186
  18. lemma OAI.BinaryCoordinateSweeps.sweep_centered_sign line 194
  19. lemma OAI.BinaryCoordinateSweeps.variation_fourier_equiv line 200