Zulip Chat Archive

Stream: mathlib4

Topic: Log.ENNReal is not in Mathlib version in mathlib4 repo

Pietro Lavino (Jun 26 2024 at 20:48):

Is there a reason why this is the case while it is present in the online documentation? or am I doing something wrong?

Ruben Van de Velde (Jun 26 2024 at 21:19):

Where are you looking in the documentation and where are you looking in the repository?

Pietro Lavino (Jun 26 2024 at 21:26):

I am looking in Mathlib as it is represented inside the mathlib4 repo inside vs code editor and I found Log.ENNReal in https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/SpecialFunctions/Log/ENNReal.html

Ruben Van de Velde (Jun 26 2024 at 21:38):

It's here in the repository: https://github.com/leanprover-community/mathlib4/blob/fed9531b808337631ee5ed4b515b5ac374a2fe68/Mathlib/Analysis/SpecialFunctions/Log/ENNReal.lean as of three days ago

Ruben Van de Velde (Jun 26 2024 at 21:38):

You may have an outdated version locally

Pietro Lavino (Jun 28 2024 at 01:50):

Ruben Van de Velde said:

It's here in the repository: https://github.com/leanprover-community/mathlib4/blob/fed9531b808337631ee5ed4b515b5ac374a2fe68/Mathlib/Analysis/SpecialFunctions/Log/ENNReal.lean as of three days ago

I have checked the master branch pulled and Log still seems to be missing the ENNreal file, this is what i get on my terminal

ietrolavino@Pietros-MacBook-Air mathlib4 % pietrolavino@Pietros-MacBook-Air mathlib4 % ls -l Mathlib/Analysis/SpecialFunctions/Log

total 144
-rw-r--r-- 1 pietrolavino staff 19957 13 Jun 14:09 Base.lean
-rw-r--r-- 1 pietrolavino staff 24402 13 Jun 14:09 Basic.lean
-rw-r--r-- 1 pietrolavino staff 15134 13 Jun 14:09 Deriv.lean
-rw-r--r-- 1 pietrolavino staff 3369 13 Jun 14:09 Monotone.lean
-rw-r--r-- 1 pietrolavino staff 5275 13 Jun 14:09 NegMulLog.lean

Kim Morrison (Jun 28 2024 at 03:07):

Not sure what you've done, it's there for me!

Ruben Van de Velde (Jun 28 2024 at 05:16):

What's the output of git show?

Pietro Lavino (Jul 05 2024 at 19:09):

Ruben Van de Velde said:

What's the output of git show?

commit 2e745027eda737ee5835bb1d1fc1b46cb1235f35 (HEAD -> Metric-entropy, origin/Metric-entropy)

Merge: f536cf360 27f915111

Author: Pietro Lavino <pietrolavino@Pietros-MacBook-Air.local>

Date: Thu Jun 27 19:33:53 2024 -0700

saving changes
diff --cc MyProject/1.3.lean
index 8fd031d1f,693400da6..4339c6a14
--- a/MyProject/1.3.lean
+++ b/MyProject/1.3.lean

@@@ -1,9 -1,128 +1,125 @@@

import Mathlib.Analysis.NormedSpace.FiniteDimension

import Mathlib.Analysis.Convolution

import Mathlib.MeasureTheory.Function.Jacobian

import Mathlib.MeasureTheory.Integral.Bochner

import Mathlib.MeasureTheory.Measure.Lebesgue.Basic

import Mathlib.Analysis.SpecialFunctions.Log.Basic

import Mathlib.Data.ENNReal.Real

import Init.Data.Fin.Basic

import Mathlib.Data.Set.Lattice

import Mathlib.Data.Set.Function

import Mathlib.Analysis.SpecialFunctions.Log.Basic

import Mathlib.Analysis.Convex.Basic

import Mathlib.Data.Real.Basic

import Mathlib.Algebra.BigOperators.Ring

import Mathlib.MeasureTheory.Measure.NullMeasurable

import Mathlib.SetTheory.Cardinal.Basic

import Mathlib.Analysis.Subadditive

--fkt lemma is fully contained in lean

--and is described by the followinf theorems

#check Subadditive --definition

#check Subadditive.lim

#check Subadditive.tendsto_lim
+
+

#check MeasureTheory.MeasurePreserving

#check Measurable

open MeasureTheory ENNReal Set Function BigOperators Finset

#check tsum
+

structure partition {α : Type*} (m : MeasurableSpace α) (μ : Measure α) [IsProbabilityMeasure μ] :=

f : ℕ → Set α -- A function from natural numbers to sets of terms in α

measurable : ∀ n, MeasurableSet (f n) -- Each set is measurable

(disjoint : ∀ i j, i ≠ j → μ (f i ∩ f j) = 0) -- The sets are pairwise disjoint

(cover : μ (⋃ n, f n)ᶜ = 0) -- The union of all sets covers the entire space
+

:
ic-entropy)

Merge: f536cf360 27f915111

Author: Pietro Lavino <pietrolavino@Pietros-MacBook-Air.local>

Date: Thu Jun 27 19:33:53 2024 -0700

saving changes
diff --cc MyProject/1.3.lean
index 8fd031d1f,693400da6..4339c6a14
--- a/MyProject/1.3.lean
+++ b/MyProject/1.3.lean

@@@ -1,9 -1,128 +1,125 @@@

import Mathlib.Analysis.NormedSpace.FiniteDimension

import Mathlib.Analysis.Convolution

import Mathlib.MeasureTheory.Function.Jacobian

import Mathlib.MeasureTheory.Integral.Bochner

import Mathlib.MeasureTheory.Measure.Lebesgue.Basic

import Mathlib.Analysis.SpecialFunctions.Log.Basic

import Mathlib.Data.ENNReal.Real

import Init.Data.Fin.Basic

import Mathlib.Data.Set.Lattice

import Mathlib.Data.Set.Function

import Mathlib.Analysis.SpecialFunctions.Log.Basic

import Mathlib.Analysis.Convex.Basic

import Mathlib.Data.Real.Basic

import Mathlib.Algebra.BigOperators.Ring

import Mathlib.MeasureTheory.Measure.NullMeasurable

import Mathlib.SetTheory.Cardinal.Basic

import Mathlib.Analysis.Subadditive

--fkt lemma is fully contained in lean

--and is described by the followinf theorems

#check Subadditive --definition

#check Subadditive.lim

#check Subadditive.tendsto_lim
+
+

#check MeasureTheory.MeasurePreserving

#check Measurable

open MeasureTheory ENNReal Set Function BigOperators Finset

#check tsum
+

structure partition {α : Type*} (m : MeasurableSpace α) (μ : Measure α) [IsProbabilityMeasure μ] :=

f : ℕ → Set α -- A function from natural numbers to sets of terms in α

measurable : ∀ n, MeasurableSet (f n) -- Each set is measurable

(disjoint : ∀ i j, i ≠ j → μ (f i ∩ f j) = 0) -- The sets are pairwise disjoint

(cover : μ (⋃ n, f n)ᶜ = 0) -- The union of all sets covers the entire space
+

:
ic-entropy)

Merge: f536cf360 27f915111

Author: Pietro Lavino <pietrolavino@Pietros-MacBook-Air.local>

Date: Thu Jun 27 19:33:53 2024 -0700

saving changes
diff --cc MyProject/1.3.lean
index 8fd031d1f,693400da6..4339c6a14
--- a/MyProject/1.3.lean
+++ b/MyProject/1.3.lean

@@@ -1,9 -1,128 +1,125 @@@

import Mathlib.Analysis.NormedSpace.FiniteDimension

import Mathlib.Analysis.Convolution

import Mathlib.MeasureTheory.Function.Jacobian

import Mathlib.MeasureTheory.Integral.Bochner

import Mathlib.MeasureTheory.Measure.Lebesgue.Basic

import Mathlib.Analysis.SpecialFunctions.Log.Basic

import Mathlib.Data.ENNReal.Real

import Init.Data.Fin.Basic

import Mathlib.Data.Set.Lattice

import Mathlib.Data.Set.Function

import Mathlib.Analysis.SpecialFunctions.Log.Basic

import Mathlib.Analysis.Convex.Basic

import Mathlib.Data.Real.Basic

import Mathlib.Algebra.BigOperators.Ring

import Mathlib.MeasureTheory.Measure.NullMeasurable

import Mathlib.SetTheory.Cardinal.Basic

import Mathlib.Analysis.Subadditive

--fkt lemma is fully contained in lean

--and is described by the followinf theorems

#check Subadditive --definition

#check Subadditive.lim

#check Subadditive.tendsto_lim
+
+

#check MeasureTheory.MeasurePreserving

#check Measurable

open MeasureTheory ENNReal Set Function BigOperators Finset

#check tsum
+

structure partition {α : Type*} (m : MeasurableSpace α) (μ : Measure α) [IsProbabilityMeasure μ] :=

f : ℕ → Set α -- A function from natural numbers to sets of terms in α

measurable : ∀ n, MeasurableSet (f n) -- Each set is measurable

(disjoint : ∀ i j, i ≠ j → μ (f i ∩ f j) = 0) -- The sets are pairwise disjoint

(cover : μ (⋃ n, f n)ᶜ = 0) -- The union of all sets covers the entire space
+

noncomputable section

def met_entropy {α : Type*} {m : MeasurableSpace α} {μ : Measure α} [IsProbability:
ic-entropy)

Merge: f536cf360 27f915111

Author: Pietro Lavino <pietrolavino@Pietros-MacBook-Air.local>

Date: Thu Jun 27 19:33:53 2024 -0700

saving changes
diff --cc MyProject/1.3.lean
index 8fd031d1f,693400da6..4339c6a14
--- a/MyProject/1.3.lean
+++ b/MyProject/1.3.lean

@@@ -1,9 -1,128 +1,125 @@@

import Mathlib.Analysis.NormedSpace.FiniteDimension

import Mathlib.Analysis.Convolution

import Mathlib.MeasureTheory.Function.Jacobian

import Mathlib.MeasureTheory.Integral.Bochner

import Mathlib.MeasureTheory.Measure.Lebesgue.Basic

import Mathlib.Analysis.SpecialFunctions.Log.Basic

import Mathlib.Data.ENNReal.Real

import Init.Data.Fin.Basic

import Mathlib.Data.Set.Lattice

import Mathlib.Data.Set.Function

import Mathlib.Analysis.SpecialFunctions.Log.Basic

import Mathlib.Analysis.Convex.Basic

import Mathlib.Data.Real.Basic

import Mathlib.Algebra.BigOperators.Ring

import Mathlib.MeasureTheory.Measure.NullMeasurable

import Mathlib.SetTheory.Cardinal.Basic

import Mathlib.Analysis.Subadditive

--fkt lemma is fully contained in lean

--and is described by the followinf theorems

#check Subadditive --definition

#check Subadditive.lim

#check Subadditive.tendsto_lim
+
+

#check MeasureTheory.MeasurePreserving

#check Measurable

open MeasureTheory ENNReal Set Function BigOperators Finset

#check tsum
+

structure partition {α : Type*} (m : MeasurableSpace α) (μ : Measure α) [IsProbabilityMeasure μ] :=

f : ℕ → Set α -- A function from natural numbers to sets of terms in α

measurable : ∀ n, MeasurableSet (f n) -- Each set is measurable

(disjoint : ∀ i j, i ≠ j → μ (f i ∩ f j) = 0) -- The sets are pairwise disjoint

(cover : μ (⋃ n, f n)ᶜ = 0) -- The union of all sets covers the entire space
+

noncomputable section

def met_entropy {α : Type*} {m : MeasurableSpace α} {μ : Measure α} [IsProbabilityMeasure μ]

(p : partition m μ) : ℝ :=

-∑' (n : ℕ),

(μ (p.f n)).toReal* Real.log ((μ (p.f n)).toReal)
+
+

-- defining conditional entropy

:

Kevin Buzzard (Jul 05 2024 at 21:50):

Just to be clear -- is this the output whilst in the mathlib repo? If so then it looks to me like you're not on the master branch (you're perhaps on a Metric-entropy branch) which might explain why you can't see the file you want (if your branch isn't fully merged with a recent master).

Pietro Lavino (Jul 05 2024 at 22:51):

Kevin Buzzard said:

Just to be clear -- is this the output whilst in the mathlib repo? If so then it looks to me like you're not on the master branch (you're perhaps on a Metric-entropy branch) which might explain why you can't see the file you want (if your branch isn't fully merged with a recent master).

Yeah this is the branch I work on Metric -entropy, I however get similar messages on the master branch, as you can see The Log file still does not contain the ENNReal file.

pietrolavino@Pietros-MacBook-Air mathlib4 % git checkout master

Already on 'master'

Your branch is ahead of 'origin/master' by 1 commit.

(use "git push" to publish your local commits)

pietrolavino@Pietros-MacBook-Air mathlib4 % git fetch origin

pietrolavino@Pietros-MacBook-Air mathlib4 % git merge maste

merge: maste - not something we can merge

pietrolavino@Pietros-MacBook-Air mathlib4 % git merge master

Already up to date.

pietrolavino@Pietros-MacBook-Air mathlib4 % git show

commit 27f915111a4457c3c3d3168cc51e4d6ee5bfa604 (HEAD -> master)

Author: Pietro Lavino <pietrolavino@Pietros-MacBook-Air.local>

Date: Thu Jun 27 18:55:16 2024 -0700

Working on MyProject files
diff --git a/MyProject/1.3.lean b/MyProject/1.3.lean
new file mode 100644
index 000000000..693400da6
--- /dev/null
+++ b/MyProject/1.3.lean

@@ -0,0 +1,128 @@
+import Mathlib.Analysis.NormedSpace.FiniteDimension
+import Mathlib.Analysis.Convolution
+import Mathlib.MeasureTheory.Function.Jacobian
+import Mathlib.MeasureTheory.Integral.Bochner
+import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
+import Mathlib.Analysis.SpecialFunctions.Log.Basic
+import Mathlib.Data.ENNReal.Real
+import Init.Data.Fin.Basic
+import Mathlib.Data.Set.Lattice
+import Mathlib.Data.Set.Function
+import Mathlib.Analysis.SpecialFunctions.Log.Basic
+import Mathlib.Analysis.Convex.Basic
+import Mathlib.Data.Real.Basic
+import Mathlib.Algebra.BigOperators.Ring
+import Mathlib.MeasureTheory.Measure.NullMeasurable
+import Mathlib.SetTheory.Cardinal.Basic
+
+
+
+
+
+#check MeasureTheory.MeasurePreserving
+#check Measurable
+open MeasureTheory ENNReal Set Function BigOperators Finset
+#check tsum
+
+structure partition {α : Type*} (m : MeasurableSpace α) (μ : Measure α) [IsProbabilityMeasure μ] :=
+ f : ℕ → Set α -- A function from natural numbers to sets of terms in α
+ measurable : ∀ n, MeasurableSet (f n) -- Each set is measurable
+ (disjoint : ∀ i j, i ≠ j → μ (f i ∩ f j) = 0) -- The sets are pairwise disjoint
+ (cover : μ (⋃ n, f n)ᶜ = 0) -- The union of all sets covers the entire space
+
+noncomputable section
+def met_entropy {α : Type*} {m : MeasurableSpace α} {μ : Measure α} [IsProbabilityMeasure μ]
+ (p : partition m μ) : ℝ :=
+ -∑' (n : ℕ),
+ (μ (p.f n)).toReal* Real.log ((μ (p.f n)).toReal)

pietrolavino@Pietros-MacBook-Air mathlib4 % cd Mathlib/Analysis/SpecialFunctions/Log

pietrolavino@Pietros-MacBook-Air Log % ls -a

. Base.lean Deriv.lean NegMulLog.lean

.. Basic.lean Monotone.lean

pietrolavino@Pietros-MacBook-Air Log %

Kevin Buzzard (Jul 06 2024 at 00:18):

The master branch of mathlib on github does contain the ENNReal file https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/SpecialFunctions/Log/ENNReal.html as you can see on github, and it's there for several other people (including me), so the problem is definitely at your end. What does git remote --v report? Are you pulling from git@github.com:leanprover-community/mathlib4.git ? Did you try git pull when on master?

Pietro Lavino (Jul 06 2024 at 00:30):

Ruben Van de Velde said:

You may have an outdated version locally

this is what i get on git remote --v , the l2718 is the fork i am working on, is this indicating a wrong configuration?

pietrolavino@Pietros-MacBook-Air mathlib4 % pietrolavino@Pietros-MacBook-Air mathlib4 % git remote --v
origin git@github.com:l2718/mathlib4.git (fetch)
origin git@github.com:l2718/mathlib4.git (push)

Kevin Buzzard (Jul 06 2024 at 00:41):

Right so you're not pulling from the leanprover-community version of mathlib, which has the file you want, you're pulling from some fork which perhaps has not been synced with the official version of mathlib recently.

Eric Wieser (Jul 06 2024 at 09:06):

(also, please read #backticks and use it for pasting command output)

Pietro Lavino (Jul 07 2024 at 01:22):

after merging a bunch work was needed to get files to work again is it good practice in order to avoid this happening in future to be syncing the fork and pulling from it everyday before working?

Kevin Buzzard (Jul 07 2024 at 08:45):

In my experience there are two approaches.

If you're making a project for fun, or to learn Lean, or for a one-off publication, then you can just make your own repo which depends on mathlib, or even work on a branch if it's a smaller project, and then not bump mathlib at all, get it over the line, write the paper if that's your goal, and then forget about it.

But if you want to help the community then making a one-off project is useless for precisely the reasons you're pointing out (nobody can use it in 6 months' time because it doesn't work any more with modern mathlib) and you have to start making the pull requests to get your work into mathlib, and the sooner the better, because your brilliant definition on which everything else depends might not be acceptable to the mathlib reviewers and then you have to change it and then your entire project breaks.

With FLT we're bumping mathlib every few weeks but also moving stuff as fast as we can out of FLT into mathlib.

Kevin Buzzard (Jul 07 2024 at 08:47):

This is the price which this community pays in order to continue to offer a globally coherent product (mathlib). Other mathematics communities in other provers put less importance on this, so you end up with abandoned projects which do something useful but which don't work any more, or multiple projects which do the same thing. For mathlib this is unacceptable but this design decision comes with the big cost which you're experiencing. However if your work ends up in mathlib then it's no longer your problem, it lives forever because the maintainers and reviewers will keep it alive.

Ruben Van de Velde (Jul 07 2024 at 09:47):

And also we're aware that updating mathlib is more hassle than we'd like, and there's various ideas about improving the experience, that are (as I understand it) waiting for engineering resources

Last updated: May 02 2025 at 03:31 UTC