[Merged by Bors] - feat: Binary entropy by adomasbaliuka · Pull Request #9734 · leanprover-community/mathlib4

adomasbaliuka · 2024-01-14T02:23:22Z

Define the (Shannon) binary and q-ary entropy functions.

The binary entropy function is used in information theory; for example, in Shannon's theorems.

depends on: [Merged by Bors] - feat: Generalize statements about deriv of MulLog #14594
depends on: [Merged by Bors] - feat: Compute derivative of fun x ↦ f (a - x) #15828
depends on: [Merged by Bors] - chore: Fix statement of eq_iff_not_lt_of_le #15829

The lemmas are mostly "trivial", especially using Mathlib.Analysis.SpecialFunctions.Log.NegMulLog.
This is the kind of application that NegMulLog was made for.

If Mathlib is to include Shannon's theorems in the future (already formalized in Coq), this might hopefully save someone a few minutes.

iczelia · 2024-01-14T08:51:40Z

Shouldn't binary entropy be put under InformationTheory? Why not use capital H_2 for the function's name?

adomasbaliuka · 2024-01-14T14:07:09Z

@kspalaiologos Thanks for the comment! I moved it to InformationTheory. For the name, did you mean to use H₂ or H_2? The danger is that it might be confused with Rényi entropy (collision entropy), which is written H₂.

Mathlib/InformationTheory/BinaryEntropy.lean

YaelDillies · 2024-02-13T09:09:33Z

@b-mehta and I have material about the binary entropy function. We needed it a year ago in the context of the progress on the Frankl set family conjecture. I suggest we wait for Bhavik to provide the code to compare.

b-mehta · 2024-02-14T01:21:16Z

Yes, I developed that further since this function is fundamental to my Ramsey proof. I will make a detailed comparison in the next day or two.

…p)*log(1-p)

YaelDillies · 2024-08-15T09:28:26Z

There were still too many small things to fix for the review to converge quickly, so I took the freedom to clean things up myself. Your PR now depends on two small prerequisite PRs.

ghost · 2024-08-15T18:05:36Z

This PR/issue depends on:

~~[Merged by Bors] - feat: Generalize statements about deriv of MulLog #14594~~
~~[Merged by Bors] - feat: Compute derivative of fun x ↦ f (a - x) #15828~~
~~[Merged by Bors] - chore: Fix statement of eq_iff_not_lt_of_le #15829~~
By Dependent Issues (🤖). Happy coding!

YaelDillies

Now looks good enough to me

maintainer merge

github-actions · 2024-08-15T19:31:24Z

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

github-actions · 2024-08-16T08:45:23Z

PR summary 1c7ad929c6

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Analysis.SpecialFunctions.BinaryEntropy`	1634

Declarations diff

+ Continuous.mul_log
+ binEntropy
+ binEntropy_continuous
+ binEntropy_eq_log_two
+ binEntropy_eq_negMulLog_add_negMulLog_one_sub
+ binEntropy_eq_negMulLog_add_negMulLog_one_sub'
+ binEntropy_eq_zero
+ binEntropy_le_log_two
+ binEntropy_lt_log_two
+ binEntropy_neg_of_neg
+ binEntropy_neg_of_one_lt
+ binEntropy_nonneg
+ binEntropy_nonpos_of_nonpos
+ binEntropy_nonpos_of_one_le
+ binEntropy_one
+ binEntropy_one_sub
+ binEntropy_pos
+ binEntropy_strictAntiOn
+ binEntropy_strictMonoOn
+ binEntropy_two_inv
+ binEntropy_two_inv_add
+ binEntropy_zero
+ deriv2_binEntropy
+ deriv2_qaryEntropy
+ deriv_binEntropy
+ deriv_qaryEntropy
+ differentiableAt_binEntropy
+ differentiableAt_binEntropy_iff_ne_zero_one
+ differentiableAt_qaryEntropy
+ hasDerivAt_binEntropy
+ hasDerivAt_qaryEntropy
+ inv_div_comm
+ not_continuousAt_deriv_qaryEntropy_one
+ not_continuousAt_deriv_qaryEntropy_zero
+ qaryEntropy
+ qaryEntropy_continuous
+ qaryEntropy_neg_of_neg
+ qaryEntropy_nonneg
+ qaryEntropy_nonpos_of_nonpos
+ qaryEntropy_one
+ qaryEntropy_pos
+ qaryEntropy_strictAntiOn
+ qaryEntropy_strictMonoOn
+ qaryEntropy_two
+ qaryEntropy_zero
+ strictConcaveOn_qaryEntropy
+ strictConcave_binEntropy
+ ⟨_,

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean

Co-authored-by: Johan Commelin <johan@commelin.net>

github-actions · 2024-08-17T10:26:18Z

PR summary a50c9f14e1

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Analysis.SpecialFunctions.BinaryEntropy`	1635

Declarations diff

+ Continuous.mul_log
+ binEntropy
+ binEntropy_continuous
+ binEntropy_eq_log_two
+ binEntropy_eq_negMulLog_add_negMulLog_one_sub
+ binEntropy_eq_negMulLog_add_negMulLog_one_sub'
+ binEntropy_eq_zero
+ binEntropy_le_log_two
+ binEntropy_lt_log_two
+ binEntropy_neg_of_neg
+ binEntropy_neg_of_one_lt
+ binEntropy_nonneg
+ binEntropy_nonpos_of_nonpos
+ binEntropy_nonpos_of_one_le
+ binEntropy_one
+ binEntropy_one_sub
+ binEntropy_pos
+ binEntropy_strictAntiOn
+ binEntropy_strictMonoOn
+ binEntropy_two_inv
+ binEntropy_two_inv_add
+ binEntropy_zero
+ deriv2_binEntropy
+ deriv2_qaryEntropy
+ deriv_binEntropy
+ deriv_qaryEntropy
+ differentiableAt_binEntropy
+ differentiableAt_binEntropy_iff_ne_zero_one
+ differentiableAt_qaryEntropy
+ hasDerivAt_binEntropy
+ hasDerivAt_qaryEntropy
+ inv_div_comm
+ not_continuousAt_deriv_qaryEntropy_one
+ not_continuousAt_deriv_qaryEntropy_zero
+ qaryEntropy
+ qaryEntropy_continuous
+ qaryEntropy_neg_of_neg
+ qaryEntropy_nonneg
+ qaryEntropy_nonpos_of_nonpos
+ qaryEntropy_one
+ qaryEntropy_pos
+ qaryEntropy_strictAntiOn
+ qaryEntropy_strictMonoOn
+ qaryEntropy_two
+ qaryEntropy_zero
+ strictConcaveOn_qaryEntropy
+ strictConcave_binEntropy
+ ⟨_,

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

github-actions · 2024-08-17T23:39:53Z

PR summary ef058a9609

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Analysis.SpecialFunctions.BinaryEntropy`	1638

Declarations diff

+ Continuous.mul_log
+ binEntropy
+ binEntropy_continuous
+ binEntropy_eq_log_two
+ binEntropy_eq_negMulLog_add_negMulLog_one_sub
+ binEntropy_eq_negMulLog_add_negMulLog_one_sub'
+ binEntropy_eq_zero
+ binEntropy_le_log_two
+ binEntropy_lt_log_two
+ binEntropy_neg_of_neg
+ binEntropy_neg_of_one_lt
+ binEntropy_nonneg
+ binEntropy_nonpos_of_nonpos
+ binEntropy_nonpos_of_one_le
+ binEntropy_one
+ binEntropy_one_sub
+ binEntropy_pos
+ binEntropy_strictAntiOn
+ binEntropy_strictMonoOn
+ binEntropy_two_inv
+ binEntropy_two_inv_add
+ binEntropy_zero
+ deriv2_binEntropy
+ deriv2_qaryEntropy
+ deriv_binEntropy
+ deriv_qaryEntropy
+ differentiableAt_binEntropy
+ differentiableAt_binEntropy_iff_ne_zero_one
+ differentiableAt_qaryEntropy
+ hasDerivAt_binEntropy
+ hasDerivAt_qaryEntropy
+ inv_div_comm
+ not_continuousAt_deriv_qaryEntropy_one
+ not_continuousAt_deriv_qaryEntropy_zero
+ qaryEntropy
+ qaryEntropy_continuous
+ qaryEntropy_neg_of_neg
+ qaryEntropy_nonneg
+ qaryEntropy_nonpos_of_nonpos
+ qaryEntropy_one
+ qaryEntropy_pos
+ qaryEntropy_strictAntiOn
+ qaryEntropy_strictMonoOn
+ qaryEntropy_two
+ qaryEntropy_zero
+ strictConcaveOn_qaryEntropy
+ strictConcave_binEntropy
+ ⟨_,

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

dupuisf · 2024-08-18T01:14:05Z

Alright, let's get this merged! :-)

bors r+

Define the (Shannon) binary and q-ary entropy functions. The binary entropy function is used in information theory; for example, in Shannon's theorems. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

mathlib-bors · 2024-08-18T02:14:17Z

Pull request successfully merged into master.

Build succeeded:

Define the (Shannon) binary and q-ary entropy functions. The binary entropy function is used in information theory; for example, in Shannon's theorems. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

adomasbaliuka added help-wanted The author needs attention to resolve issues WIP Work in progress new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! labels Jan 14, 2024

adomasbaliuka marked this pull request as draft January 14, 2024 02:25

adomasbaliuka force-pushed the adomas_binary_entropy branch from 594c71d to 1d22a13 Compare January 23, 2024 00:15

adomasbaliuka marked this pull request as ready for review January 23, 2024 00:16

adomasbaliuka force-pushed the adomas_binary_entropy branch from 1d22a13 to f209f6e Compare February 1, 2024 13:01

kim-em reviewed Feb 13, 2024

View reviewed changes