comap f (c • μ) = c • comap f μ

Stream: Is there code for X?

[Kevin Buzzard]

I want that pullback of a measure commutes with scalar multiplication. I thought it would be rfl but in fact I went down a deep hole and I am still not entirely out of it; there is one sorry left. @Sébastien Gouëzel you warned me that it wouldn't be easy. I have no energy to figure out how NullMeasurableSet works but I learnt a fair bit about the basics of the measure theory part of mathlib today, which was interesting. What I want is the last lemma in this code; am I making a meal of this? I don't know the tricks for this part of the library but I'm quite pleased I got this far, even if it did take up all my FLT time for today :-)

import Mathlib

open scoped NNReal ENNReal

-- I need 0 < c to deal with ι empty,
lemma ENNReal.iInf_smul {ι : Sort*} {c : ℝ≥0} (hc : 0 < c) (f : ι → ℝ≥0∞)  :
    ⨅ i, c • f i = c •  ⨅ i, f i := by
  apply le_antisymm
  · rw [← inv_smul_le_iff_of_pos hc]
    refine le_iInf (fun i ↦ ?_)
    rw [inv_smul_le_iff_of_pos hc]
    exact iInf_le_of_le i le_rfl
  · refine le_iInf (fun i ↦ ?_)
    rw [smul_le_smul_iff_of_pos_left hc]
    exact iInf_le_of_le i le_rfl

namespace MeasureTheory

@[simp] -- should this be `simp`?
lemma OuterMeasure.comap_smul_ennreal {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
    {f : X → Y} {c : ℝ≥0∞}
    {μ : OuterMeasure Y} : comap f (c • μ) = c • comap f μ := rfl

@[simp] -- should this be `simp`?
lemma OuterMeasure.comap_smul_nnreal {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
    {f : X → Y} {c : ℝ≥0}
    {μ : OuterMeasure Y} : comap f (c • μ) = c • comap f μ := rfl

lemma OuterMeasure.caratheodory_le_smul {X : Type*} (μ : OuterMeasure X) {c : ℝ≥0} :
    μ.caratheodory ≤ (c • μ).caratheodory := by
  intro s hs
  rw [OuterMeasure.isCaratheodory_iff] at hs ⊢
  peel hs with t h
  simp [h]

lemma OuterMeasure.toMeasure_smul {X : Type*} [ms : MeasurableSpace X] {c : ℝ≥0}
    (μ : OuterMeasure X) (hμ : ms ≤ μ.caratheodory) :
    (c • μ).toMeasure (hμ.trans μ.caratheodory_le_smul) = c • μ.toMeasure hμ := by
  obtain rfl | hc := eq_zero_or_pos c; · simp
  ext s hs
  simp only [Measure.smul_apply, Measure.nnreal_smul_coe_apply]
  change ⨅ _, _ = _ * ⨅ _, _
  unfold extend
  simp only [coe_smul, Pi.smul_apply, ENNReal.iInf_smul hc, ENNReal.tsum_const_smul]
  rfl

namespace Measure

open scoped NNReal

lemma const_smul_ae_of_ae {X : Type*} [MeasurableSpace X] {μ : Measure X} {s t : Set X} (c : ℝ≥0)
    (hst : t =ᶠ[ae μ] s) : t =ᶠ[ae (c • μ)] s := by
  rw [ae_eq_set] at hst ⊢
  simp [hst]

lemma nullMeasurableSet_smul_of_nullMeasurableSet {X : Type*} [MeasurableSpace X]
    {μ : Measure X} (c : ℝ≥0) {s : Set X} (h : NullMeasurableSet s μ) :
    NullMeasurableSet s (c • μ) := by
  -- is `exists_measurable_superset_ae_eq` an iff for NullMeasurableSet?
  -- It says `NullMeasurableSet s μ → ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s`
  -- If not then the approach below won't work.
  obtain ⟨t, ht⟩ := h.exists_measurable_superset_ae_eq
  have ht' : t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae (c • μ)] s := by
    peel ht
    exact const_smul_ae_of_ae c this
  /-
  ht' : t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae (c • μ)] s
  ⊢ NullMeasurableSet s (c • μ)
  -/
  sorry

lemma nullMeasurableSet_smul_iff_nullMeasurableSet {X : Type*} [MeasurableSpace X]
    {μ : Measure X} {c : ℝ≥0} (hc : 0 < c) {s : Set X} :
    NullMeasurableSet s (c • μ) ↔ NullMeasurableSet s μ := by
  refine ⟨?_, nullMeasurableSet_smul_of_nullMeasurableSet c⟩
  intro h
  apply nullMeasurableSet_smul_of_nullMeasurableSet c⁻¹ at h
  rwa [smul_smul, inv_mul_cancel₀ hc.ne', one_smul] at h

lemma comap_smul {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y] {f : X → Y} {c : ℝ≥0}
    {μ : Measure Y} : comap f (c • μ) = c • comap f μ := by
  obtain rfl | hc := eq_zero_or_pos c; · simp
  by_cases h : Function.Injective f ∧ ∀ (s : Set X), MeasurableSet s → NullMeasurableSet (f '' s) μ
  · unfold comap
    rw [dif_pos h]
    have h' : Function.Injective f ∧
        ∀ (s : Set X), MeasurableSet s → NullMeasurableSet (f '' s) (c • μ) := by
      refine ⟨h.1, ?_⟩
      replace h := h.2
      peel h with s hs h
      rwa [nullMeasurableSet_smul_iff_nullMeasurableSet hc]
    rw [dif_pos h']
    simp only [smul_toOuterMeasure, LinearMap.map_smul_of_tower]
    rw [OuterMeasure.toMeasure_smul]
  · have h' : ¬ (Function.Injective f ∧
        ∀ (s : Set X), MeasurableSet s → NullMeasurableSet (f '' s) (c • μ)) := by
      contrapose! h
      refine ⟨h.1, ?_⟩
      replace h := h.2
      peel h with s hs h
      rwa [nullMeasurableSet_smul_iff_nullMeasurableSet hc] at h
    unfold comap
    rw [dif_neg h, dif_neg h']
    simp

[Rémy Degenne]

lemma nullMeasurableSet_smul_of_nullMeasurableSet {X : Type*} [MeasurableSpace X]
    {μ : Measure X} (c : ℝ≥0) {s : Set X} (h : NullMeasurableSet s μ) :
    NullMeasurableSet s (c • μ) :=
  NullMeasurableSet.mono_ac h (AbsolutelyContinuous.rfl.smul_left c)

[Kevin Buzzard]

I rather suspect that you can golf a lot of the above lemmas :-) (or even convince me that they're not needed!)

[Rémy Degenne]

Yes, I am currently golfing :)

[Kevin Buzzard]

I hope that at least my beginner attempt makes your life easier! The only result which really had some "Lean content" was OuterMeasure.toMeasure_smul where at the end I removed the unfold OuterMeasure.toMeasure Measure.ofMeasurable inducedOuterMeasure extend OuterMeasure.ofFunction and replaced it with a change, and then I had to battle through moving the smul across binders. Everything else was kind of intro, apply, exact, or in the API.

[Rémy Degenne]

import Mathlib

open scoped NNReal ENNReal

namespace MeasureTheory

lemma NullMeasurableSet.smul_measure {X : Type*} [MeasurableSpace X]
    {μ : Measure X} (c : ℝ≥0) {s : Set X} (h : NullMeasurableSet s μ) :
    NullMeasurableSet s (c • μ) :=
  NullMeasurableSet.mono_ac h (Measure.AbsolutelyContinuous.rfl.smul_left c)

lemma nullMeasurableSet_smul_iff_nullMeasurableSet {X : Type*} [MeasurableSpace X]
    {μ : Measure X} {c : ℝ≥0} (hc : 0 < c) {s : Set X} :
    NullMeasurableSet s (c • μ) ↔ NullMeasurableSet s μ := by
  refine ⟨?_, NullMeasurableSet.smul_measure c⟩
  intro h
  apply NullMeasurableSet.smul_measure c⁻¹ at h
  rwa [smul_smul, inv_mul_cancel₀ hc.ne', one_smul] at h

namespace Measure

lemma comap_smul {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y] {f : X → Y} {c : ℝ≥0}
    {μ : Measure Y} : comap f (c • μ) = c • comap f μ := by
  obtain rfl | hc := eq_zero_or_pos c; · simp
  by_cases h : Function.Injective f ∧ ∀ (s : Set X), MeasurableSet s → NullMeasurableSet (f '' s) μ
  · ext s hs
    rw [comap_apply₀ f _ h.1 _ hs.nullMeasurableSet, smul_apply, smul_apply,
      comap_apply₀ f μ h.1 h.2 hs.nullMeasurableSet]
    simpa [nullMeasurableSet_smul_iff_nullMeasurableSet hc] using h.2
  · have h' : ¬ (Function.Injective f ∧
        ∀ (s : Set X), MeasurableSet s → NullMeasurableSet (f '' s) (c • μ)) := by
      contrapose! h
      simpa [nullMeasurableSet_smul_iff_nullMeasurableSet hc] using h
    simp [comap, dif_neg h, dif_neg h']

end Measure

end MeasureTheory

(edited for better names)

[Rémy Degenne]

I kept only the results that are used for comap_smul

[Kevin Buzzard]

Thanks so much!

[Kevin Buzzard]

The simpa trick works without having to use contrapose! at the end:

  · have h' : ¬ (Function.Injective f ∧
        ∀ (s : Set X), MeasurableSet s → NullMeasurableSet (f '' s) (c • μ)) := by
      simpa [nullMeasurableSet_smul_iff_nullMeasurableSet hc] using h

Are you PRing it or am I?

[Rémy Degenne]

I'll PR it.
A remark about the code above: we have a lot of API about measures now, so any time you unpack definitions so much that an OuterMeasure appears, you probably unpacked too much.

[Sébastien Gouëzel]

If you PR it, can you do it for c : ENNReal instead of just NNReal?

[Rémy Degenne]

#25052

[Kevin Buzzard]

Many thanks! I have switched to map for the main definition of FLT now I understand that it's much easier to work with, but there is still one key calculation where I need to use comaps so I will need this and perhaps more; it's the first thing on my job list tomorrow to figure out exactly what, if anything, more I need from comaps.

[Kevin Buzzard]

Actually I know already that I need these:

open Topology in
@[to_additive]
lemma isHaarMeasure_comap_of_isOpenEmbedding {G H : Type*}
    [Group G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G]
    [Group H] [TopologicalSpace H] [MeasurableSpace H] [BorelSpace H]
    {φ : G →* H} (hφ : IsOpenEmbedding φ) (μ : Measure H) [IsHaarMeasure μ] :
    IsHaarMeasure (comap φ μ) := by
  sorry -- issue FLT#507

open Topology in
lemma regular_comap_of_isOpenEmbedding {G H : Type*}
    [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G]
    [TopologicalSpace H] [MeasurableSpace H] [BorelSpace H]
    {φ : G → H} (hφ : IsOpenEmbedding φ) (μ : Measure H) [Regular μ] : Regular (comap φ μ) := by
  sorry -- issue FLT#513

and my plan was to just do them from first principles (or persuade someone else to do them)

[Eric Wieser]

@Yaël Dillies, do I remember correctly that I asked for this result in a PR of yours?

[Yaël Dillies]

It was #20204

[David Ledvinka]

Kevin Buzzard said:

Actually I know already that I need these:

open Topology in
@[to_additive]
lemma isHaarMeasure_comap_of_isOpenEmbedding {G H : Type*}
    [Group G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G]
    [Group H] [TopologicalSpace H] [MeasurableSpace H] [BorelSpace H]
    {φ : G →* H} (hφ : IsOpenEmbedding φ) (μ : Measure H) [IsHaarMeasure μ] :
    IsHaarMeasure (comap φ μ) := by
  sorry -- issue FLT#507

open Topology in
lemma regular_comap_of_isOpenEmbedding {G H : Type*}
    [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G]
    [TopologicalSpace H] [MeasurableSpace H] [BorelSpace H]
    {φ : G → H} (hφ : IsOpenEmbedding φ) (μ : Measure H) [Regular μ] : Regular (comap φ μ) := by
  sorry -- issue FLT#513

and my plan was to just do them from first principles (or persuade someone else to do them)

I have a proof of the first one but I need the additional assumptions
[MeasurableMul G] [MeasurableMul H]

[David Ledvinka]

Technically I think [MeasurableMul G] should follow from [MeasurableMul H] and the fact that φ is an open embedding.

[David Ledvinka]

open Topology in
@[to_additive]
lemma isHaarMeasure_comap_of_isOpenEmbedding {G H : Type*}
    [Group G] [TopologicalSpace G] [MeasurableSpace G] [BorelSpace G] [MeasurableMul G]
    [Group H] [TopologicalSpace H] [MeasurableSpace H] [BorelSpace H] [MeasurableMul H]
    {φ : G →* H} (hφ : IsOpenEmbedding φ) (μ : Measure H) [IsHaarMeasure μ] :
    IsHaarMeasure (comap φ μ) :=
  { map_mul_left_eq_self := by
      intro g
      ext s hs
      rw [map_apply (by fun_prop) hs]
      repeat rw [MeasurableEmbedding.comap_apply hφ.measurableEmbedding]
      have : ⇑φ '' ((fun x ↦ g * x) ⁻¹' s) = (fun x ↦ φ g * x) ⁻¹' (⇑φ '' s) := by
        ext
        constructor
        · intro h
          obtain ⟨y, hy, rfl⟩ := h
          use g * y, hy
          simp
        · intro h
          obtain ⟨y, yins, hy⟩ := h
          use g⁻¹ * y
          constructor
          · simp [yins]
          · simp [hy]
      rw [this, ← map_apply (by fun_prop), map_mul_left_eq_self]
      exact hφ.measurableEmbedding.measurableSet_image.mpr hs
    lt_top_of_isCompact := by
      intro K hK
      rw [MeasurableEmbedding.comap_apply hφ.measurableEmbedding]
      exact IsFiniteMeasureOnCompacts.lt_top_of_isCompact (hK.image hφ.continuous)
    open_pos := by
      intro U hU Une
      rw [MeasurableEmbedding.comap_apply hφ.measurableEmbedding]
      exact IsOpenPosMeasure.open_pos _ (hφ.isOpen_iff_image_isOpen.mp hU) (Une.image φ)
  }

[Kevin Buzzard]

Oh you can definitely have [IsTopologicalGroup G] and [IsTopologicalGroup H]! This gives that multiplication is continuous and hence measurable! In all the applications they're topological groups.

Please feel free to make a PR to FLT: add in the topological group hypotheses (or less, if you want). The relevant file is https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/HaarMeasure/HaarChar/AddEquiv.lean . Thanks so much!

[Kevin Buzzard]

I can PR it for you but please feel free to take the opportunity of being a contributor to the FLT project. If you don't want this then that's also fine, I'll just PR it myself :-)

[David Ledvinka]

Is there a github permissions thread for FLT? I don't have permission to create a branch and the CONTRIBUTING.md doesn't seem to mention it.

[David Ledvinka]

Have a proof of the second as well

[Ruben Van de Velde]

You can submit from a fork

[Kevin Buzzard]

Yes please make a branch not called main and PR from a fork. Also feel free to claim the relevant issues on GitHub so nobody else works on them. Many thanks for contributing to FLT!