OAI/Probability/BinarySweep/SparseBounds/CenteredPlacement.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BinaryCoordinateSweeps.Young.subPlacement_univ_injective line 16
  2. def OAI.BinaryCoordinateSweeps.Young.partialPlacement line 22
  3. lemma OAI.BinaryCoordinateSweeps.Young.partialPlacement_apply line 29
  4. lemma OAI.BinaryCoordinateSweeps.Young.partialPlacement_univ line 37
  5. def OAI.BinaryCoordinateSweeps.Young.placementAverage line 48
  6. def OAI.BinaryCoordinateSweeps.Young.partialPlacementAverage line 51
  7. def OAI.BinaryCoordinateSweeps.Young.centeredPlacement line 54
  8. lemma OAI.BinaryCoordinateSweeps.Young.partialPlacement_specht_zero line 59
  9. lemma OAI.BinaryCoordinateSweeps.Young.partialPlacementAverage_specht_zero line 67
  10. theorem OAI.BinaryCoordinateSweeps.Young.centeredPlacement_specht line 73
  11. lemma OAI.BinaryCoordinateSweeps.Young.placementAverage_specht line 88
  12. def OAI.BinaryCoordinateSweeps.Young.placementCoeffs line 103
  13. def OAI.BinaryCoordinateSweeps.Young.partialHilbert line 105
  14. def OAI.BinaryCoordinateSweeps.Young.partialKernel line 108
  15. lemma OAI.BinaryCoordinateSweeps.Young.partialKernel_toLin line 112
  16. lemma OAI.BinaryCoordinateSweeps.Young.partialKernel_adjoint line 126
  17. lemma OAI.BinaryCoordinateSweeps.Young.partialHilbert_adjoint line 137
  18. def OAI.BinaryCoordinateSweeps.Young.centeredHilbert line 142
  19. lemma OAI.BinaryCoordinateSweeps.Young.centeredHilbert_sum line 147
  20. lemma OAI.BinaryCoordinateSweeps.Young.centeredHilbert_adjoint line 155
  21. def OAI.BinaryCoordinateSweeps.Young.spechtPlacementHilbert line 166
  22. lemma OAI.BinaryCoordinateSweeps.Young.spechtPlacementHilbert_injective line 170
  23. lemma OAI.BinaryCoordinateSweeps.Young.centeredHilbert_specht line 174