OAI/Combinatorics/Progressions/Dynamics/BooleanCanonicalLogBudget.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.productMinorEntryLog line 11
  2. def OAI.Erdos3.productMinorPartialLog line 12
  3. def OAI.Erdos3.productMinorInverseLog line 13
  4. def OAI.Erdos3.productMinorDerivativeLog line 15
  5. def OAI.Erdos3.productMinorDeterminantLog line 17
  6. theorem OAI.Erdos3.productMinorEntryBound_le_exp line 20
  7. theorem OAI.Erdos3.productMinorPartialBound_le_exp line 38
  8. theorem OAI.Erdos3.productMinorInverseBound_le_exp line 54
  9. theorem OAI.Erdos3.productMinorDerivativeBound_le_exp line 71
  10. theorem OAI.Erdos3.productMinorDeterminantDerivativeBound_le_exp line 84
  11. def OAI.Erdos3.jointBooleanInverseBudget line 119
  12. def OAI.Erdos3.jointBooleanDerivativeBudget line 123
  13. theorem OAI.Erdos3.jointBooleanInverseBudget_le line 128
  14. theorem OAI.Erdos3.jointBooleanDerivativeBudget_le line 137
  15. def OAI.Erdos3.cubeMinorConstantLog line 156
  16. def OAI.Erdos3.cubeMinorScaleLog line 159
  17. def OAI.Erdos3.cubeMinorThresholdLog line 161
  18. theorem OAI.Erdos3.cubeMinorProbabilityConstant_le_exp line 164
  19. theorem OAI.Erdos3.cubeMinorProbabilityScale_le_exp line 182
  20. theorem OAI.Erdos3.cubeMinorThreshold_inverse_le_exp line 192
  21. theorem OAI.Erdos3.canonicalCubeMinorThreshold_inverse_le_exp line 205
  22. def OAI.Erdos3.canonicalBooleanMinorLog line 227
  23. def OAI.Erdos3.jointBooleanInverseLog line 232
  24. def OAI.Erdos3.jointBooleanDerivativeLog line 237
  25. def OAI.Erdos3.booleanAxisWeightLog line 242
  26. def OAI.Erdos3.jointBooleanWeightLog line 249
  27. theorem OAI.Erdos3.canonicalBooleanMinorLog_nonneg line 253
  28. theorem OAI.Erdos3.jointBooleanInverseLog_nonneg line 259
  29. theorem OAI.Erdos3.jointBooleanDerivativeLog_nonneg line 269
  30. theorem OAI.Erdos3.jointBooleanInverseBudget_canonical_le_exp line 279
  31. theorem OAI.Erdos3.jointBooleanDerivativeBudget_le_exp line 304