OAI/InformationTheory/BooleanNoise/MonotoneDissipation.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LeanBlast.CourtadeKumar.IsIncreasing.restrict line 22
  2. theorem OAI.LeanBlast.CourtadeKumar.IsIncreasing.pairHalfDifference_nonneg line 31
  3. theorem OAI.LeanBlast.CourtadeKumar.scalar_meanVariance_pos line 41
  4. theorem OAI.LeanBlast.CourtadeKumar.scalar_meanVariance_le_one line 46
  5. theorem OAI.LeanBlast.CourtadeKumar.IsInterior.meanVariance_pos line 49
  6. theorem OAI.LeanBlast.CourtadeKumar.IsInterior.entropyAverage_pos line 53
  7. theorem OAI.LeanBlast.CourtadeKumar.average_one_sub_sq_le_meanVariance line 58
  8. theorem OAI.LeanBlast.CourtadeKumar.monotone_pair_average_geometry line 63
  9. theorem OAI.LeanBlast.CourtadeKumar.halfDifference_sq_lt_meanVariance line 110
  10. theorem OAI.LeanBlast.CourtadeKumar.monotone_split_parameter_bounds line 118
  11. theorem OAI.LeanBlast.CourtadeKumar.meanSquare_ratio_le_jensen_ratio line 140
  12. theorem OAI.LeanBlast.CourtadeKumar.jensen_ratio_mem_unit_interval line 151
  13. theorem OAI.LeanBlast.CourtadeKumar.normalized_variance_gap_nonneg line 158
  14. theorem OAI.LeanBlast.CourtadeKumar.normalized_variance_gap_identity line 164
  15. theorem OAI.LeanBlast.CourtadeKumar.normalized_jensen_correction_le line 168
  16. theorem OAI.LeanBlast.CourtadeKumar.scaled_perspective_bound line 188
  17. theorem OAI.LeanBlast.CourtadeKumar.monotone_dissipation_step_algebra line 210
  18. theorem OAI.LeanBlast.CourtadeKumar.monotone_pair_correction line 219
  19. theorem OAI.LeanBlast.CourtadeKumar.monotone_dissipation_step_of_perspective line 231
  20. theorem OAI.LeanBlast.CourtadeKumar.two_point_perspective_jensen line 260
  21. theorem OAI.LeanBlast.CourtadeKumar.monotone_dissipation_zero line 285
  22. theorem OAI.LeanBlast.CourtadeKumar.averaged_normalized_pair_of_pointwise line 297
  23. theorem OAI.LeanBlast.CourtadeKumar.restricted_monotone_dissipation_lower line 330
  24. theorem OAI.LeanBlast.CourtadeKumar.monotone_dissipation_from_scalar_lemmas line 353
  25. theorem OAI.LeanBlast.CourtadeKumar.monotone_dissipation line 398