OAI/Combinatorics/MatchingCount/Algorithm/EmpiricalDenom.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.Trial.empiricalDenom line 11
  2. lemma OAI.MatchingFPRAS.Trial.empiricalDenom_pos line 12
  3. lemma OAI.MatchingFPRAS.Trial.ScaleState.observables_grid line 13
  4. lemma OAI.MatchingFPRAS.Trial.ScaleState.means_bits line 31
  5. lemma OAI.MatchingFPRAS.BitArithmetic.alpha_bits line 47
  6. def OAI.MatchingFPRAS.BitArithmetic.matrixBound line 49
  7. lemma OAI.MatchingFPRAS.BitArithmetic.matrixBound_large line 50
  8. lemma OAI.MatchingFPRAS.BitArithmetic.ratioEstimate_bits line 54
  9. lemma OAI.MatchingFPRAS.BitArithmetic.upperEstimate_bits line 61
  10. lemma OAI.MatchingFPRAS.BitArithmetic.scalingTrace_bits line 74
  11. lemma OAI.MatchingFPRAS.Trial.ScaleState.ratioEstimate_bits line 109
  12. lemma OAI.MatchingFPRAS.Trial.ScaleState.matrix_bits line 114
  13. lemma OAI.MatchingFPRAS.Trial.ScaleState.updateVector_bits line 124
  14. lemma OAI.MatchingFPRAS.Trial.initial_scale_bits line 137
  15. def OAI.MatchingFPRAS.Trial.Parameters.empiricalBound line 145
  16. def OAI.MatchingFPRAS.Trial.Parameters.matrixBound line 146
  17. lemma OAI.MatchingFPRAS.Trial.Parameters.empiricalBound_pos line 147
  18. lemma OAI.MatchingFPRAS.Trial.Parameters.matrixBound_large line 149
  19. def OAI.MatchingFPRAS.Trial.Parameters.scaleBound line 151
  20. lemma OAI.MatchingFPRAS.Trial.layers_scale_bits line 153
  21. lemma OAI.MatchingFPRAS.Trial.layers_ratio_bits line 168
  22. lemma OAI.MatchingFPRAS.Trial.output_bits line 178
  23. def OAI.MatchingFPRAS.Trial.rationalOutput line 184
  24. lemma OAI.MatchingFPRAS.Trial.rationalOutput_cast line 186
  25. lemma OAI.MatchingFPRAS.Trial.rationalOutput_nonneg line 190
  26. lemma OAI.MatchingFPRAS.Trial.rationalOutput_accurate line 193
  27. lemma OAI.MatchingFPRAS.FiniteTrial.ScaleState.ratioEstimate_bits line 214
  28. lemma OAI.MatchingFPRAS.FiniteTrial.ScaleState.matrix_bits line 223
  29. lemma OAI.MatchingFPRAS.FiniteTrial.ScaleState.updateVector_bits line 233
  30. lemma OAI.MatchingFPRAS.FiniteTrial.initial_scale_bits line 253
  31. lemma OAI.MatchingFPRAS.FiniteTrial.layers_scale_bits line 256
  32. lemma OAI.MatchingFPRAS.FiniteTrial.layers_ratio_bits line 273
  33. lemma OAI.MatchingFPRAS.FiniteTrial.output_bits line 283
  34. lemma OAI.MatchingFPRAS.BitArithmetic.FractionBound.num_den line 291
  35. lemma OAI.MatchingFPRAS.BitArithmetic.size_mul_le line 311
  36. lemma OAI.MatchingFPRAS.BitArithmetic.size_pow_le line 318
  37. lemma OAI.MatchingFPRAS.BitArithmetic.FractionBound.encode_length line 326
  38. lemma OAI.MatchingFPRAS.BitArithmetic.size_empiricalBound line 336
  39. lemma OAI.MatchingFPRAS.BitArithmetic.size_matrixBound line 340
  40. lemma OAI.MatchingFPRAS.BitArithmetic.size_scaleBound line 348
  41. lemma OAI.MatchingFPRAS.FiniteTrial.scale_encode_length line 359
  42. def OAI.MatchingFPRAS.Counting.schedulePolynomial line 380
  43. lemma OAI.MatchingFPRAS.Counting.polynomial_schedule line 381
  44. lemma OAI.MatchingFPRAS.Counting.leastSchedule_polynomial line 419