Measure.comap injectivity

Stream: mathlib4

[Bjørn Kjos-Hanssen]

Measure.comap is defined as follows:

/-- Pullback of a `Measure`. If `f` sends each measurable set to a null-measurable set,
then for each measurable set `s` we have `comap f μ s = μ (f '' s)`. -/
def comap [MeasurableSpace α] (f : α → β) (μ : Measure β) : Measure α :=
  if hf : Injective f ∧ ∀ s, MeasurableSet s → NullMeasurableSet (f '' s) μ then
    (OuterMeasure.comap f μ.toOuterMeasure).toMeasure fun s hs t => by
      simp only [OuterMeasure.comap_apply, image_inter hf.1, image_diff hf.1]
      exact (measure_inter_add_diff₀ _ (hf.2 s hs)).symm
  else 0

Why do we insist that f is injective? Is there an alternative version that doesn't?
For example, the natural map sending a binary expansion to the corresponding real number is not injective, so I can prove some strange result this way. (Specifically, that the fair coin measure on Cantor space is the zero measure.)

[Yury G. Kudryashov]

AFAICT, there is no better version of Measure.comap in Mathlib.

[Yury G. Kudryashov]

You can replace the condition with inferInstance ≤ (OuterMeasure.comap f μ.toOuterMeasure.)caratheodory

[Yury G. Kudryashov]

I mean, make a PR to Mathlib that changes the condition.

[Bjørn Kjos-Hanssen]

Thanks @Yury G. Kudryashov !
I don't know what ≤ means in this context though?

[Yury G. Kudryashov]

In this context it means that every measurable set is Caratheodory measurable w.r.t. OuterMeasure.comap f μ.toOuterMeasure

[Yury G. Kudryashov]

You will have to prove this under some weaker assumptions on f.

[Yury G. Kudryashov]

(e.g., a.e.-injectivity, or maybe something even weaker)

[Yury G. Kudryashov]

There are quite a few definitions in Mathlib that can be generalized. Fortunately, we can do it once someone needs a more general version.

[Bjørn Kjos-Hanssen]

Makes sense. As a smaller change, ideally the current version should have injectivity as an explicit assumption rather than hidden in the ite, I think.

[Yury G. Kudryashov]

No, we use this design everywhere. E.g., deriv doesn't require the function to be differentiable.

[Yury G. Kudryashov]

Probably, the first change is to fix the docstring to say explicitly that it's zero unless $f$ is injective and sends measurable sets to (null) measurable sets.

[Yury G. Kudryashov]

If you turn Injective f into an argument, then you'll have to supply it every time you write Measure.comap, not just when you apply theorems about it. Also, rw [(h : f = g)] will fail.

[Bjørn Kjos-Hanssen]

Okay I can try to make a PR. I added the changes in the docstring to my copy of the file which is part of my copy of mathlib

Another option for dealing with the Cantor set and $\mathbb R$, I suppose, could be to restrict the Cantor set to a subtype so that the map into $\mathbb R$ becomes injective:

noncomputable def real_of_cantor :=
  λ (x : ℕ → Bool) ↦ tsum (λ n : ℕ ↦ ite (x n = true) ((1:ℝ) / (2 ^ n.succ)) 0)

noncomputable def CantorLebesgueMeasure : MeasureTheory.Measure (ℕ → Bool) :=
MeasureTheory.Measure.comap real_of_cantor MeasureTheory.volume -- bad currently, since not injective

noncomputable def CantorLebesgueMeasureSubtype :
  MeasureTheory.Measure (  -- those that don't end 0 1^∞
    {x : ℕ → Bool // ¬ ∃ k, x k = false ∧ ∀ l, k < l → x l = true}
  ) :=
  MeasureTheory.Measure.comap (λ x ↦ real_of_cantor x.1) MeasureTheory.volume

[Yaël Dillies]

As a simple change, can you replace injectivity by ae injectivity?

[Yaël Dillies]

That should cover your Cantor set example

[Bjørn Kjos-Hanssen]

That's a good idea.

Alternatively, I don't know if Mathlib already has a way to define a measure by "extending by zero".
E.g., define a measure on ℕ → Bool by:

$\mu(A)=\mathrm{CantorLebesgueMeasureSubtype}(A \cap${x : ℕ → Bool // ¬ ∃ k, x k = false ∧ ∀ l, k < l → x l = true}$\}$?

[Floris van Doorn]

I'm probably misunderstanding what you mean, but do you mean docs#MeasureTheory.Measure.restrict ?

[Bjørn Kjos-Hanssen]

Hmm, restrict seems to assume you already have a measure on the bigger set (or type).

I mean for example, say you have a measure on $\{0,1\}$. What's the Mathlib way to extend that to a measure on $\mathbb N$ by declaring that all numbers other than 0 and 1 have measure zero?

[Kevin Buzzard]

For other structures in mathlib which I'm more familiar with, that would be called .map

[Bjørn Kjos-Hanssen]

That makes sense, thanks @Kevin Buzzard
https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Measure/MeasureSpace.html#MeasureTheory.Measure.map

[Yury G. Kudryashov]

Should we redefine Measure.comap f μ s as the integral of Set.encard (f ⁻¹' {y} ∩ s) (or the integral of Set.encard (f ⁻¹' {y}) over f '' s)?

[Yury G. Kudryashov]

This makes sense for coverings and is equal to the old definition for an injective map.

[Bjørn Kjos-Hanssen]

Sounds great. What would the new definition be exactly?

[Yury G. Kudryashov]

Something like

def Measure.comap f μ : Measure α :=
  if (assumptions needed for the proof below to work) then
    .ofMeasurable (fun s _ ↦ ∫⁻ y, (f ⁻¹' {y} ∩ s).encard.toENNReal ∂μ (by simp) (harder_part_of_the_proof)
  else 0

[Yury G. Kudryashov]

I didn't think what assumptions are needed to make it work yet. Of course, this change of a definition will move comap after lintegral in the import graph.