Essential range of a Borel function

Stream: Is there code for X?

[Jon Bannon]

I'm going to try a small PR in order to get used to the new PR paradigm, and was wondering whether the essential range of a Borel function already exists (in some implicit form) in Mathlib, and if not, whether the following definition would be ok as a starting point for a PR (i.e. was coming at the definition in a reasonable way for Mathlib):

import Mathlib

namespace MeasureTheory

section BorelSpace

open BorelSpace

variable {X : Type*} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X]

def support (μ : Measure X) : Set X := {x : X | ∀ U ∈ nhds x, μ (interior U) > 0}

variable {Y : Type*} [TopologicalSpace Y] [MeasurableSpace Y]

def ess_range (μ : Measure X) (f : X → Y) : Set Y :=
  support (Measure.map f μ)

end BorelSpace

[Kim Morrison]

I don't know this corner of the library, so won't comment on whether this exists somewhere.

But for a PR, you should include at least some basic theorems (e.g. perhaps ess_range is contained in closure of range? a.e. equal functions have the same ess_range?), just to verify the definitions are as intended.

[Aaron Liu]

Why are you measuring the interior of U?

[Jon Bannon]

@Aaron Liu : Measuring the interior of U may not be necessary. Typically, this set is defined using open neighborhoods, though, which is why I included this.

[Aaron Liu]

def support' (μ : Measure X) : Set X := {x : X | ∀ U ∈ nhds x, 0 < μ U}

example : @support = @support' := by
  ext X _ _ μ x
  constructor
  · intro h U hU
    calc
      0 < μ (interior U) := h U hU
      _ ≤ μ U := measure_mono interior_subset
  · intro h U hU
    exact h (interior U) (interior_mem_nhds.mpr hU)

[Jon Bannon]

Probably good enough to just state this without the interior...

[Jon Bannon]

Anyhow, what I want to know is whether this should be a PR at all (once I include proofs of some basic results that show the definitions aren't wrongheaded!)

[Jon Bannon]

The following works. It seems to be, though, that the assumptions on the essential range are too strong for the theorem (according to a linter...but this seems off).

theorem ess_range_eq_of_ae_eq {μ : Measure X} (f g : X → Y) (hfg : f =ᵐ[μ] g) : ess_range μ f = ess_range μ g := by
  dsimp [ess_range, support]; ext ; congr! 6
  exact congrFun (congrArg DFunLike.coe <| Measure.map_congr hfg) _

[Jireh Loreaux]

Some other comments:

1. Per #naming, ess_range should be lower camel-cased to essRange.
2. I think it should probably be protected MeasureTheory.Measure.support (potentially without the protected, but definitely with Measure to allow for dot notation).
3. Showing IsClosed μ.support would be a key initial lemma.
4. You could also provide a few lemmas relating support to different measures, e.g., μ ≤ ν → μ.support ≤ ν.support.
5. I would probably make two separate PRs for support and essRange, although you could list them both simultaneously with the latter being motivation for the former.

[Jon Bannon]

@Jireh Loreaux I think I like the protected, to keep this from being confused with the (pointwise, bare) function support.

[Jon Bannon]

@Jireh Loreaux I also think you have sorted why we need open neighborhoods in the support def...one needs this to prove IsClosed μ.support. Cool. I think I have enough to go on here for a PR. Thanks everyone!