preimage of functions which use EXists.choose

Stream: Is there code for X?

[Pietro Lavino]

If a function chooses its output out of many possible ones (through Exists.choose), when we take the preimage in Lean of say {n} under this function will this set include all the point that could have chosen n, or only does who actually end up choosing n?

[Edward van de Meent]

i'm not exactly sure what you mean... could you give a #mwe ?

[Pietro Lavino]

Edward van de Meent

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

--defining partition given measure, disjointness defined measure-theoretically
-- cover for now is defined in the set-theoretic sense

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)

lemma partition.partOf_eq_ae {α : Type*} {m : MeasurableSpace α} {μ : Measure α} [IsProbabilityMeasure μ]
    (p : partition m μ) (n : ℕ) :
    (p.partOf) ⁻¹' {n} =ᵐ[μ] p.f n := by
    have h: p.partOf ⁻¹' {n} ⊆ p.f n := by
      intro x hx
      have h := partition.partOf_spec p x
      rw [Set.mem_preimage, Set.mem_singleton_iff] at hx
      rw[hx] at h; assumption
    have h': p.f n ⊆  p.partOf ⁻¹' {n} := by
      sorry

I was referring to my function partition.partOf

[Kevin Buzzard]

That function will always return the same value for the same input (like every function) but the value it returns is completely opaque, it will be unprovable and undisprovable in general to figure out if it equals any given term that you happen to know is in the preimage, the only thing you know about the output is .partOf_spec. Did I answer the question or were you asking something else?

[Pietro Lavino]

Kevin Buzzard Yeah this was it, thanks