advice, how write function with default values

Stream: Is there code for X?

[Pietro Lavino]

I am writing an expression for the information function given a point in a probability space, it should give back -log ( \mu (s)) where s is a set in the partition containing the input x. I was previously working with a definition of partition that required it cover the entire space Exists.choose did the job. But I have now change the definition to allow partition to cover the space up to a null set. So now I was thinking that I could either make the information function have as domain the cover of the partition or that it gives some default value if the point is not covered by the partition. I found that I could make it by including in the hypothesis the "decidable" of whether was x was covered by partition but that made my function weird as in it was of the type alpha \r decidable \r n. which seemed inconvenient. what other options that could make integrating this function the least painful? This is what I have for now, where I am technically artificially modifying the domain, but ideally the function would just give back a default value if point is not covered.

import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.MeasureTheory
open MeasureTheory
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 def partition.partOf {α : Type*} {m : MeasurableSpace α} {μ : Measure α}  [IsProbabilityMeasure μ]
  (p : partition m μ ) (x : α) (hx : x ∈ ⋃ n, p.f n) : ℕ :=
Exists.choose (show ∃ n, x ∈ p.f n from (mem_iUnion (x := x) (s := p.f)).mp hx)

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 hx) :=
  Exists.choose_spec (show ∃ n, x ∈ p.f n from (mem_iUnion (x := x) (s := p.f)).mp hx)

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

[Yury G. Kudryashov]

I suggest that you use classical decidability. E.g., you can use docs#Classical.epsilon

[Yury G. Kudryashov]

BTW, do you want to deal with a sequence of sets or a countable set of sets?

[Yury G. Kudryashov]

Possible reasons to use a family of sets:

• with a set of sets, you can easily allow finite partitions (if you ask for Set.Countable without asking for Set.Infinite);
• some natural operations like "pairwise intersections of these 2 partitions" get more natural definitions;
• with the sequence approach, a permutation leads to a different partition and you need to introduce an equivalence relation + prove theorems about it. OTOH, you'll need a relation for "a.e. same partition" anyway.

[Pietro Lavino]

Yury G. Kudryashov
I will give the different definition of partition a try, for the information function u are suggesting to use Classical.epsilon instead of Exists.choose (what are the advantages/changes), but do you think it is best to keep the hypothesis of being covered or perhaps using an if /else statement and including [dec : Decidable (x ∈ (⋃ n, p.f n))] in the hypothesis? Thank you

[Yury G. Kudryashov]

You should use open scoped Classical instead of assuming that this predicate is decidable.