OAI/Combinatorics/Progressions/Estimates/NormalizedDeterminantCutoff.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.unitTestClip_lipschitz line 15
  2. theorem OAI.Erdos3.unitTestClip_eq_self line 18
  3. theorem OAI.Erdos3.unitTestClip_norm_le_one line 22
  4. def OAI.Erdos3.clippedSelectedDeterminant line 25
  5. theorem OAI.Erdos3.clippedSelectedDeterminant_eq_det line 29
  6. theorem OAI.Erdos3.real_perm_sign_norm line 38
  7. theorem OAI.Erdos3.clippedSelectedDeterminant_lipschitz line 42
  8. def OAI.Erdos3.normalizedDeterminantCutoff line 89
  9. theorem OAI.Erdos3.normalizedDeterminantCutoff_range line 94
  10. theorem OAI.Erdos3.normalizedDeterminantCutoff_lipschitz line 100
  11. theorem OAI.Erdos3.normalizedDeterminantCutoff_eq_one line 109
  12. theorem OAI.Erdos3.normalizedDeterminantCutoff_eq_zero line 127
  13. theorem OAI.Erdos3.normalizedDeterminantCutoff_indicator_bounds line 142
  14. def OAI.Erdos3.spatialMatrixBlockCutoff line 158
  15. theorem OAI.Erdos3.spatialMatrixBlockCutoff_range line 162
  16. theorem OAI.Erdos3.spatialMatrixBlockCutoff_lipschitz line 168
  17. theorem OAI.Erdos3.spatialMatrixBlockCutoff_indicator_bounds line 176