equivalence of integral to a sum

Stream: Is there code for X?

[Pietro Lavino]

Context: I am trying to prove that measure theoretic entropy is the average of the information function, where information function depends on a partition, and a point, since the information function given a partition is constant on the sets in partition except some set of measure zero, i would want to go from the integral form to a sum.

Question: I need to find a way to rewrite a bochner integral to a series given that the function being integrated is constant over sets in a countable partition, except for some points in a set of measure zero.
I provide below the code for further context, thank you.

import Mathlib.Topology.Instances.Real
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





open MeasureTheory
open ENNReal
open Set
open Function
open scoped BigOperators
open Finset
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) = Set.univ)  -- 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)

def info {α : Type*} {m : MeasurableSpace α} {μ : Measure α} [IsProbabilityMeasure μ]
  (p : partition m μ) (x : α) :ℝ := by
    have h: x ∈ Set.univ := by tauto
    rw[← p.cover] at h; rw[mem_iUnion] at h
    choose a _ using h
    exact (-Real.log (μ (p.f (a))).toReal)

theorem ent_inf {α : Type*} {m : MeasurableSpace α} {μ : Measure α} [IsProbabilityMeasure μ]
  (p : partition m μ): met_entropy p = ∫ x, info p x ∂μ := by
  unfold met_entropy
  sorry

end section

trying to solve the theorem ent_inf. I tried to represent as something of type α → ℝ as I though that to be necessary by defining:

def infof {α : Type*} {m : MeasurableSpace α} {μ : Measure α} [IsProbabilityMeasure μ]
  (p : partition m μ) : α → ℝ :=
λ x ↦ info p x

but the statements are received by Lean as equivalent.

[Kalle Kytölä]

I believe you would like to use docs#MeasureTheory.integral_iUnion_ae, docs#MeasureTheory.setIntegral_congr_ae, docs#MeasureTheory.setIntegral_const in this order.

However, you might have made your goal unnecessarily difficult by some choices here.

• A small improvement would be to use the existing docs#MeasureTheory.AEDisjoint in your disjoint condition.
• A bigger problem is using a tactic mode construction in your definition info --- the term produced by the tactic mode can become very difficult to prove things about. I believe it is almost always a bad idea to construct data (rather than proofs) in tactic mode.
• Finally, you must make sure that the junk values of your met_entropy (defined in terms of docs#tsum) coincide with the junk values produced by docs#MeasureTheory.setIntegral_congr_ae in case your info is not docs#MeasureTheory.Integrable.
• ...

Towards addressing the second bullet point I would consider something like the following instead (sorry, this is a rough sketch, not fully thought through, but hopefully it contains some ideas in the right direction):

noncomputable def partition.partOf {α : Type*} {m : MeasurableSpace α} {μ : Measure α}
    (p : partition m μ) (x : α) : ℕ :=
  Exists.choose
    (show ∃ n, x ∈ p.f n from (mem_iUnion (x := x) (s := p.f)).mp <| p.cover.symm ▸ mem_univ x)

lemma partition.partOf_spec {α : Type*} {m : MeasurableSpace α} {μ : Measure α}
    (p : partition m μ) (x : α) :
    x ∈ p.f (p.partOf x) :=
  Exists.choose_spec
    (show ∃ n, x ∈ p.f n from (mem_iUnion (x := x) (s := p.f)).mp <| p.cover.symm ▸ mem_univ x)

-- This should be the same as your definition, but given in term mode and therefore less painful to reason about.
def info {α : Type*} {m : MeasurableSpace α} {μ : Measure α} [IsProbabilityMeasure μ]
    (p : partition m μ) (x : α) : ℝ :=
  (-Real.log (μ (p.f (p.partOf x))).toReal)

-- You will probably want to know that your partition parts are a.e. the sets where your function choice takes a particular value.
lemma partition.partOf_eq_ae {α : Type*} {m : MeasurableSpace α} {μ : Measure α}
    (p : partition m μ) (n : ℕ) :
    (p.partOf) ⁻¹' {n} =ᵐ[μ] p.f n :=
  sorry

-- Then you should be able prove that your info is a.e. equal to something that is easier to integrate explicitly.
lemma info_ae_eq {α : Type*} {m : MeasurableSpace α} (μ : Measure α) [IsProbabilityMeasure μ]
    (p : partition m μ) :
    info (μ := μ) p =ᵐ[μ] fun x ↦ ∑' n, (p.partOf ⁻¹' {n}).indicator (fun _ ↦ (-Real.log (μ (p.f n)).toReal)) x := by
  sorry

-- I believe the following lemmas should then help towards your original goal.
#check integral_iUnion_ae
#check setIntegral_congr_ae
#check setIntegral_const

-- ...perhaps starting like this:
theorem ent_inf {α : Type*} {m : MeasurableSpace α} {μ : Measure α} [IsProbabilityMeasure μ]
    (p : partition m μ) :
    met_entropy p = ∫ x, info p x ∂μ := by
  by_cases junk : ¬ Integrable (info (μ := μ) p) μ
  · simp [integral_undef junk]
    sorry -- You should prove that your `tsum` defining `info` has the same junk value as `integral`
  simp only [not_not, integrable_congr (info_ae_eq μ p)] at junk
  rw [integral_congr_ae (info_ae_eq μ p)]
  unfold met_entropy
  sorry

[Pietro Lavino]

Kalle Kytölä kiitos!

[Pietro Lavino]

Kalle Kytölä
when taking the inverse of p.partOf for some N, since p.partOf chooses one out of the possibly many indexes that indicate a partition that contain that point, does the inverse include all points that could have N as output under p.partOf or only a subset of them, the ones that Exists.choose actually ends up choosing?

[Kalle Kytölä]

p.partOf ⁻¹' {n} includes only those points where exactly the nth part was chosen. The main reason I thought this is helpful is that it gives you a way to know what exact value for info you end up getting. Namely, p.partOf ⁻¹' {n} is exactly a set where your function info gets a certain constant value related to the measure of the set p.f n in your partition. (Note that your original tactic mode definition involved choice as well! But your info was not necessarily constant on p.f n because of potential null set overlaps and the choice involved.)

The lemma partition.partOf_eq_ae was there to state that this set coincides with p.f n up to a null set. That should follow from a.e. disjointness.

I certainly didn't fully think through the best way to go about your question! I just tried to indicate what I think should be the key lemmas, and where you might have made your goal harder than necessary.

And although I think p.partOf ⁻¹' {n} should be helpful, it has some downsides of its own. For example your sets p.f n were measurable on the nose, but the set p.partOf ⁻¹' {n} is only null-measurable (differs from a measurable set by a null set) --- docs#MeasureTheory.NullMeasurableSet.

Making good definitions is hard! To make definitions usable, one often needs to provide some amount of API that mathematicians just "see", but the computer doesn't. I was suggesting that partition.partOf_eq_ae and info_ae_eq might be parts of API that you need, if you want to stick to your current definition of partition and info (apart from tactic mode to term mode switch) and met_entropy, before it becomes as easy as in math to prove basic things about these. But I did not fully think through what might be optimal (nor would I know), I just wanted to encourage you to think about a good implementation that makes your goal as painless as possible.

[Kalle Kytölä]

Regarding the original "is there code for X?" question itself, I think docs#MeasureTheory.integral_iUnion_ae, docs#MeasureTheory.setIntegral_const are one answer. It may well be that some lemmas that would make things more convenient are missing, but I think the bigger difficulty is getting from your definitions to something that one might reasonably expect a library lemma for.

[Kalle Kytölä]

Maybe I will still add a lemma (combining the existing library results I mentioned) which might be useful in your case, and which might even be worth adding to the library:

import Mathlib

open MeasureTheory ENNReal Set Function Finset
open scoped BigOperators

lemma should_this_be_in_the_library
    {X : Type*} [MeasurableSpace X] (μ : Measure X) {ι : Type*} [Countable ι]
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    {As : ι → Set X} (As_mble : ∀ i, NullMeasurableSet (As i) μ)
    (As_disj : Pairwise (AEDisjoint μ on As))
    {f : X → E} (f_intble : IntegrableOn f (⋃ i, As i) μ)
    {cs : ι → E} (f_ae_loc_cst : ∀ i, f =ᵐ[μ.restrict (As i)] fun _ ↦ cs i) :
    ∫ x in (⋃ i, As i), f x ∂μ = ∑' i, (μ (As i)).toReal • cs i := by
  rw [integral_iUnion_ae (μ := μ) (s := As) As_mble As_disj f_intble]
  congr; funext i
  simpa [setIntegral_const (cs i)] using
    setIntegral_congr_ae₀ (g := fun _ ↦ cs i) (s := As i) (μ := μ) (As_mble i)
      (ae_imp_of_ae_restrict (f_ae_loc_cst i))

[Kalle Kytölä]

If that "how to integrate a function which is a.e. locally constant on each of countably many a.e. disjoint parts" (with docs#tsum spelling) is added, then I believe a similar "how to integrate a function which is a.e. locally constant on each of finitely many a.e. disjoint parts" should also be added (with docs#Finset.sum spelling).

[Pietro Lavino]

Running in some weird typeclass error is there a clear mistake I am not catching?; in one proof i use refine (measure_biUnion_null_iff ?hI).mpr ?_ and it works just fine but in another proof I get typeclass instance problem is stuck, it is often due to metavariables. I think the problem is that Lean for some reason catches a correct Outer measure class implicitly ( as it is one of the implicit arguments of the theorem I am using) but it is not in the second case OuterMeasureClass ?m.67892 ?m.67890.

import Mathlib.Topology.Instances.Real
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
open MeasureTheory ENNReal Set Function BigOperators Finset

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) = Set.univ)  -- The union of all sets covers the entire space

lemma countable_complement_singleton  (n : ℕ ) :
  Set.Countable {i | i ≠ n} := by
  apply Set.countable_iff_exists_injective.mpr
  use (λ x => x)
  · intro x y hxy
    dsimp at hxy; ext; exact hxy

lemma e2 {α : Type*} {m : MeasurableSpace α} {μ : Measure α} [IsProbabilityMeasure μ]
    (p : partition m μ) (n : ℕ): μ (⋃ (i : ℕ) (h: i ≠ n), (p.f n ∩ p.f i)) = 0 := by
    refine (measure_biUnion_null_iff ?hI).mpr ?_
    · exact (countable_complement_singleton n)
    · intro s h
      exact ((p.disjoint n s) (fun a => h (id (Eq.symm a))))

lemma eqset₂  {α : Type*} {m : MeasurableSpace α} {μ : Measure α} [IsProbabilityMeasure μ]
    (p : partition m μ)  : μ (⋃ (n : ℕ),( ⋃ (i : ℕ)(h: i ≠ n), (p.f n ∩ p.f i))) = 0 := by
    refine (measure_biUnion_null_iff _).mpr ?_
```

[Ruben Van de Velde]

If you explicitly pass (\m := \m), you get a better error

[Ruben Van de Velde]

Try iUnion instead of biUnion

[Pietro Lavino]

Very weird lean tool (id (Ne.symm _))seems to easily prove non-trivial terms in my proofs or even false one. In my proof I wanted to prove x' \notin p.partOf ⁻¹' {b} and although simply lean seems to solve this goal with this function that even upon inspection does not seem to be able to solve such a statement: is there some weird mistake allowing this to happen? This weird thing happens in my proof of lemma pre_info_ae_eq which is at the end of the following code... I was trying out even statements like 2=3 and same function would solve for that too.

import Mathlib.Topology.Instances.Real
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

open MeasureTheory ENNReal Set Function BigOperators Finset

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) = Set.univ)  -- The union of all sets covers the entire space

noncomputable def partition.partOf {α : Type*} {m : MeasurableSpace α} {μ : Measure α}[IsProbabilityMeasure μ]
    (p : partition m μ) (x : α) : ℕ :=
  Exists.choose
    (show ∃ n, x ∈ p.f n from (mem_iUnion (x := x) (s := p.f)).mp <| p.cover.symm ▸ mem_univ x)

lemma partition.partOf_spec {α : Type*} {m : MeasurableSpace α} {μ : Measure α}[IsProbabilityMeasure μ]
    (p : partition m μ) (x : α) :
    x ∈ p.f (p.partOf x) :=
  Exists.choose_spec
    (show ∃ n, x ∈ p.f n from (mem_iUnion (x := x) (s := p.f)).mp <| p.cover.symm ▸ mem_univ x)

noncomputable section

def info {α : Type*} {m : MeasurableSpace α} {μ : Measure α} [IsProbabilityMeasure μ]
    (p : partition m μ) (x : α) : ℝ :=
  (-Real.log (μ (p.f (p.partOf x))).toReal)

end section

def eqset₀ {α : Type*} {m : MeasurableSpace α} {μ : Measure α} [IsProbabilityMeasure μ]
    (p : partition m μ) : ℕ → Set α :=
  λ n ↦ p.f n \ (⋃ (i : ℕ) (h: i ≠ n), (p.f i))

def eqset  {α : Type*} {m : MeasurableSpace α} {μ : Measure α} [IsProbabilityMeasure μ]
    (p : partition m μ): Set α :=
  ⋃ (i : ℕ), eqset₀ p i

lemma pre_info_ae_eq {α : Type*} {m : MeasurableSpace α} (μ : Measure α) [IsProbabilityMeasure μ]
    (p : partition m μ) : eqset p ⊆  {x | info p x = ∑' n, (p.partOf ⁻¹' {n}).indicator (λ _ ↦ -Real.log (μ (p.f n)).toReal) x} := by
    intro x' hx'
    show info p x' = ∑' (n : ℕ), (p.partOf ⁻¹' {n}).indicator (fun x => -(μ (p.f n)).toReal.log) x'
    let N := p.partOf x'
    have h:= p.partOf_spec x'
    have h₁: ∑' (n : ℕ), (p.partOf ⁻¹' {n}).indicator (fun x => -(μ (p.f n)).toReal.log) x' = (p.partOf ⁻¹' {N}).indicator (fun x => -(μ (p.f N)).toReal.log) x' := by
      apply tsum_eq_single
      intro b hbn
      exact indicator_of_not_mem (id (Ne.symm hbn)) fun x => -(μ (p.f b)).toReal.log
    rw[h₁]
    exact Eq.symm (indicator_of_mem rfl fun x => -(μ (p.f N)).toReal.log)

[Pietro Lavino]

Ruben Van de Velde thanks, apply ended up being the cleanest/working way