OAI/InformationTheory/BooleanNoise/ComparisonEstimates.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LeanBlast.CourtadeKumar.comparisonC line 13
  2. def OAI.LeanBlast.CourtadeKumar.comparisonBracket line 16
  3. theorem OAI.LeanBlast.CourtadeKumar.comparisonC_eq_log_div line 19
  4. theorem OAI.LeanBlast.CourtadeKumar.comparisonC_lt_eleven_fourths line 25
  5. theorem OAI.LeanBlast.CourtadeKumar.hasDerivAt_comparisonC line 37
  6. theorem OAI.LeanBlast.CourtadeKumar.hasDerivAt_comparisonBracket line 41
  7. theorem OAI.LeanBlast.CourtadeKumar.comparisonBracket_derivative_neg line 51
  8. theorem OAI.LeanBlast.CourtadeKumar.comparisonBracket_antitone line 70
  9. theorem OAI.LeanBlast.CourtadeKumar.comparisonC_middle_bound line 83
  10. theorem OAI.LeanBlast.CourtadeKumar.comparisonC_integral_bracket_nonneg line 96
  11. theorem OAI.LeanBlast.CourtadeKumar.comparison_large_regime line 115
  12. theorem OAI.LeanBlast.CourtadeKumar.comparison_middle_regime line 130