OAI/Probability/SATComputability/AuxiliaryEnergy.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FixedClauseThreshold.Computability.finiteClauseAverage_iterate line 12
  2. def OAI.FixedClauseThreshold.Computability.relaxedClauseEquiv line 32
  3. theorem OAI.FixedClauseThreshold.Computability.relaxedClauseEquiv_satisfies line 38
  4. theorem OAI.FixedClauseThreshold.Computability.clauseMinimum_zero_iff line 43
  5. theorem OAI.FixedClauseThreshold.Computability.auxiliaryProbability_eq_minimum line 61
  6. theorem OAI.FixedClauseThreshold.Computability.integral_rootMinimum_zero line 78
  7. theorem OAI.FixedClauseThreshold.Computability.rootSatisfiableProbability_eq_auxiliary line 91
  8. def OAI.FixedClauseThreshold.Computability.relaxedFixedMinimum line 97
  9. def OAI.FixedClauseThreshold.Computability.relaxedPoissonMinimum line 100
  10. theorem OAI.FixedClauseThreshold.Computability.relaxedFixedMinimum_nonneg line 103
  11. theorem OAI.FixedClauseThreshold.Computability.relaxedFixedMinimum_le line 106
  12. theorem OAI.FixedClauseThreshold.Computability.relaxedPoissonMinimum_nonneg line 112
  13. theorem OAI.FixedClauseThreshold.Computability.integral_rootMinimum_eq line 115
  14. theorem OAI.FixedClauseThreshold.Computability.poissonRootAverage_minimum_eq line 123