OAI/InformationTheory/BooleanNoise/JensenGaps.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LeanBlast.CourtadeKumar.pow_tangent_remainder_nonneg line 21
  2. theorem OAI.LeanBlast.CourtadeKumar.pow_tangent_remainder_lower line 34
  3. abbrev OAI.LeanBlast.CourtadeKumar.entropySeriesCoeff line 50
  4. theorem OAI.LeanBlast.CourtadeKumar.weighted_even_pow_jensen line 52
  5. theorem OAI.LeanBlast.CourtadeKumar.weighted_centered_second_moment line 60
  6. theorem OAI.LeanBlast.CourtadeKumar.weighted_pow_gap_lower line 73
  7. theorem OAI.LeanBlast.CourtadeKumar.weighted_series_gap_hasSum line 101
  8. theorem OAI.LeanBlast.CourtadeKumar.entropy_series_gap_lower line 121
  9. theorem OAI.LeanBlast.CourtadeKumar.entropy_series_gap_strengthened line 137
  10. theorem OAI.LeanBlast.CourtadeKumar.weighted_psi_gap line 161
  11. theorem OAI.LeanBlast.CourtadeKumar.weighted_psi_gap_strengthened line 173
  12. theorem OAI.LeanBlast.CourtadeKumar.normalized_ratio_weights_data line 189
  13. theorem OAI.LeanBlast.CourtadeKumar.rescale_perspective_gap line 203
  14. theorem OAI.LeanBlast.CourtadeKumar.weighted_perspective_gap line 225
  15. theorem OAI.LeanBlast.CourtadeKumar.weighted_perspective_gap_strengthened line 241
  16. theorem OAI.LeanBlast.CourtadeKumar.weighted_abs_mean_le line 256
  17. theorem OAI.LeanBlast.CourtadeKumar.weighted_pair_mean_interior line 262
  18. theorem OAI.LeanBlast.CourtadeKumar.weighted_positive_mean line 274
  19. theorem OAI.LeanBlast.CourtadeKumar.weighted_ratio_centered_identity line 280
  20. theorem OAI.LeanBlast.CourtadeKumar.weighted_ratio_variance_identity line 294
  21. theorem OAI.LeanBlast.CourtadeKumar.weighted_ratio_variance_nonneg line 303
  22. theorem OAI.LeanBlast.CourtadeKumar.weighted_variance_gap_lower_bound line 312
  23. theorem OAI.LeanBlast.CourtadeKumar.weighted_variance_gap_nonneg line 329
  24. theorem OAI.LeanBlast.CourtadeKumar.pair_reciprocal_square_identity line 348
  25. theorem OAI.LeanBlast.CourtadeKumar.weighted_pair_gap_combine line 356
  26. theorem OAI.LeanBlast.CourtadeKumar.weighted_pair_jensen_gap line 392
  27. theorem OAI.LeanBlast.CourtadeKumar.lambda_ratio_min_le line 417
  28. theorem OAI.LeanBlast.CourtadeKumar.weighted_pair_jensen_gap_strengthened line 430
  29. theorem OAI.LeanBlast.CourtadeKumar.cube_uniform_weights_sum_one line 468
  30. theorem OAI.LeanBlast.CourtadeKumar.cubeAverage_as_weighted_sum line 472
  31. theorem OAI.LeanBlast.CourtadeKumar.convexOn_cubeAverage_le line 477
  32. theorem OAI.LeanBlast.CourtadeKumar.pair_variance_gap_lower_bound line 485
  33. theorem OAI.LeanBlast.CourtadeKumar.pair_variance_gap_nonneg line 495
  34. theorem OAI.LeanBlast.CourtadeKumar.pair_jensen_gap line 503
  35. theorem OAI.LeanBlast.CourtadeKumar.pair_jensen_gap_strengthened line 513
  36. theorem OAI.LeanBlast.CourtadeKumar.pair_jensen_gap_nonneg line 524