OAI/InformationTheory/SoftChannel/JensenGaps.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LeanBlast.CourtadeKumar.JensenGaps_entropySeriesCoeff line 22
2. theorem OAI.LeanBlast.CourtadeKumar.JensenGaps_entropy_series_gap_lower line 24
3. theorem OAI.LeanBlast.CourtadeKumar.JensenGaps_entropy_series_gap_strengthened line 40
4. theorem OAI.LeanBlast.CourtadeKumar.JensenGaps_normalized_ratio_weights_data line 64
5. theorem OAI.LeanBlast.CourtadeKumar.JensenGaps_rescale_perspective_gap line 78
6. theorem OAI.LeanBlast.CourtadeKumar.JensenGaps_pair_reciprocal_square_identity line 100
7. theorem OAI.LeanBlast.CourtadeKumar.JensenGaps_weighted_pair_gap_combine line 108
8. theorem OAI.LeanBlast.CourtadeKumar.JensenGaps_lambda_ratio_min_le line 144
9. theorem OAI.LeanBlast.CourtadeKumar.JensenGaps_cube_uniform_weights_sum_one line 159
10. theorem OAI.LeanBlast.CourtadeKumar.JensenGaps_cubeAverage_as_weighted_sum line 163