functions outputting ENNReal, by including proof of nng

Stream: Is there code for X?

[Pietro Lavino]

I am (re-)writing functions for measure theoretic entropy and the information function i initially wrote these as Real function use the real logarithm then used the ennreal log which however outputs EReal. I would like both have ENNReal outputs most importantly the entropy function, I have found a way by taking the real log and then coercing that real value to ENNReal via ENNReal.ofReal. however this transformation almost looses the information that the values were indeed originally nonnegative. Is there a way to provide inside the defintion of a function a proof of its nonnegativity which allows for "true coercion" from "EReal to ENNReal"

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.Analysis.Subadditive
import Mathlib.Analysis.SpecialFunctions.Log.ENNReal
import Mathlib.Analysis.Convex.Function
import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog



--fkt lemma is fully contained in lean
--and is described by the followinf theorems


#check Subadditive --definition
#check Subadditive.lim
#check Subadditive.tendsto_lim

--this version is catching up to the progress in one
-- but with measure theoretic defintion of cover
-- which calls for different definition of info.
-- all that is left is one small detail in max_ent and max_entropy
-- and dealing with case o funciton not being integrable, probably can prove it is integrable.

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)ᶜ  = 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)

 def met_entropy_ennreal {α : Type*} {m : MeasurableSpace α} {μ : Measure α} [IsProbabilityMeasure μ]
  (p : partition m μ) : ENNReal :=
  (∑' (n : ℕ),
    (μ (p.f n)) * ENNReal.ofReal (-Real.log ((μ (p.f n)).toReal)))

 def met_entropy_ereal {α : Type*} {m : MeasurableSpace α} {μ : Measure α} [IsProbabilityMeasure μ]
  (p : partition m μ) : EReal :=
  -∑' (n : ℕ),
    (μ (p.f n))* ENNReal.log ((μ (p.f n)))

def partition.partOf {α : Type*} {m : MeasurableSpace α} {μ : Measure α}  [IsProbabilityMeasure μ]
  (p : partition m μ ) (x : α)  : ℕ :=
  ite (x ∈ (⋃ n, p.f n)) (Classical.epsilon (λ n ↦ x ∈  p.f n)) 0

lemma partition.partOf_spec {α : Type*} {m : MeasurableSpace α} {μ : Measure α}[IsProbabilityMeasure μ]
    (p : partition m μ) (x : α) (hx : x ∈ ⋃ n, p.f n):
    x ∈ p.f (p.partOf x) := by
    unfold partition.partOf
    rw [if_pos hx]
    rw[mem_iUnion] at hx
    exact Classical.epsilon_spec hx

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

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

def info_ereal {α : Type*} {m : MeasurableSpace α} {μ : Measure α}  [IsProbabilityMeasure μ]
  (p : partition m μ ) (x : α): EReal :=
  (-ENNReal.log (μ (p.f (p.partOf x))))

the ENNReal definitions would indeed work, as entropy could actually be infinite and the values are the same i would get without the coercions, but My question is really whether there are ways of including proofs of nonnegativity inside function for a "true" correspondence that does not go through the rude simplification of say ENNReal.ofReal

[Ira Fesefeldt]

If you want to create an ENNReal from a Real, that's easy. You can use the subtype constructor to create an NNReal like this:

import Mathlib

def real_num : ℝ := sorry

theorem real_num_nn : 0 ≤ real_num := sorry

def ennreal_num : ENNReal := ENNReal.ofNNReal ⟨real_num, real_num_nn⟩

Using ofReal and ENNReal.ofReal_eq_coe_nnreal gives you essential the same.

Creating an ENNReal from an EReal may require a bit more code. At least I couldn't find a predefined function right now mapping EReals and nonnegative proofs to ENNReals - except for an CanLift that allows you to lift them in a proof. But you can create something like this:

import Mathlib

noncomputable def EReal.toENNReal (a : EReal) (h : 0 ≤ a): ENNReal := match a with
  | ⊥ => by absurd h; exact of_decide_eq_false rfl
  | ⊤ => ⊤
  | (a : Real) => ENNReal.ofNNReal ⟨a, EReal.coe_nonneg.mp h⟩

And add some lemmas about this function.

Or stick with EReal and use the lift tactic whenever required.

[Yury G. Kudryashov]

There are two functions that I think may make sense to add to the library here: a function ENNReal.ofEReal that behaves similarly to ENNReal.ofReal, i.e. it glues all negative values to zero, and nnabs.