OAI/Probability/BinarySweep/TensorBounds/SignedPlacement.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BinaryCoordinateSweeps.PathExtension.signed_restrict_zero line 20
  2. def OAI.BinaryCoordinateSweeps.signedPlacementEntry line 54
  3. lemma OAI.BinaryCoordinateSweeps.signedPlacementEntry_zero line 58
  4. theorem OAI.BinaryCoordinateSweeps.signedPlacementEntry_zero_many line 76
  5. theorem OAI.BinaryCoordinateSweeps.signedPlacementEntry_zero_few line 83
  6. lemma OAI.BinaryCoordinateSweeps.signed_partialKernel_conditional line 96
  7. lemma OAI.BinaryCoordinateSweeps.signed_centeredMatrix_zero line 113
  8. theorem OAI.BinaryCoordinateSweeps.conditional_signed_specht_one_le_zero line 126
  9. theorem OAI.BinaryCoordinateSweeps.conditional_signed_specht_many line 142
  10. theorem OAI.BinaryCoordinateSweeps.conditional_signed_specht_few line 150
  11. def OAI.BinaryCoordinateSweeps.signedCenteredHS line 170
  12. lemma OAI.BinaryCoordinateSweeps.continuousAt_signedCenteredHS line 173
  13. lemma OAI.BinaryCoordinateSweeps.signedCenteredHS_zero line 190
  14. lemma OAI.BinaryCoordinateSweeps.conditional_signed_specht_hs line 197