Double `Filter.Eventually`

Stream: Is there code for X?

[Jihoon Hyun]

I'm trying to prove the following:

import Mathlib

open MeasureTheory

example
    {α₁ : Type*} [MeasureSpace α₁] {β₁ : Type*} [MeasureSpace β₁] (e₁ : β₁ ≃ᵐ α₁)
    {α₂ : Type*} [MeasureSpace α₂] {β₂ : Type*} [MeasureSpace β₂] (e₂ : β₂ ≃ᵐ α₂)
    {p : α₁ → α₂ → Prop} (h : ∀ᵐ (a₁ : α₁) (a₂ : α₂), p a₁ a₂) :
    ∀ᵐ (b₁ : β₁) (b₂ : β₂), p (e₁ b₁) (e₂ b₂) := by
  sorry

Is there a nice theorem which can handle double 'almost everywhere' easily?
Also, this would easily come up with another version with a doubly nested Filter.Eventually (∀ᶠ). Do we have a tool to prove that as well?

[Aaron Liu]

Why do you have both docs#MeasureTheory.MeasurableSpace and docs#MeasureTheory.MeasureSpace

[Aaron Liu]

This will cause problems

[Aaron Liu]

I'm pretty sure to prove this you have to assume that e₁ and e₂ are docs#MeasureTheory.Measure.QuasiMeasurePreserving

[Jihoon Hyun]

Why do you have both..

Thanks, this is now fixed in the example.

I'm pretty sure to prove this you have to assume that e₁ and e₂ are docs#MeasureTheory.Measure.QuasiMeasurePreserving

According to docs#MeasurableEquiv.quasiMeasurePreserving_symm , they are already QuasiMeasurePreserving.

Still, is there a nice way to deal with inner ∀ᵐ or ∀ᶠs? I don't think there is a nice lemma dealing with these.

[Yury G. Kudryashov]

Nothing in your assumptions say that e₁ or e₂ play nicely with the measures.

[Yury G. Kudryashov]

You only assume that they're measurable with measurable inverses.

[Aaron Liu]

Jihoon Hyun said:

According to docs#MeasurableEquiv.quasiMeasurePreserving_symm , they are already QuasiMeasurePreserving.

This says they are QuasiMeasurePreserving from MeasureTheory.Measure.map (⇑e) volume to volume, but I need it to be QuasiMeasurePreserving from volume to volume.

[Yury G. Kudryashov]

If you add (h₁ : QuasiMeasurePreserving e₁) and similarly for e₂, then you can filter_upwards [h₁.ae h] with a ha using h₂.ae ha

[Yury G. Kudryashov]

(not tested)

[Aaron Liu]

Yury G. Kudryashov said:

filter_upwards [h₁.ae h] with a ha using h₂.ae ha

This does work

[Jihoon Hyun]

Aaron Liu 말함:

Yury G. Kudryashov said:

filter_upwards [h₁.ae h] with a ha using h₂.ae ha

This does work

Now I wonder why this works..

[Jihoon Hyun]

I only know that filter_upwards converts ∀ᵐ into ∀, but how does this work here?

[Kevin Buzzard]

You can hover over it to find out what it actually does (it's cleverer than just turning ∀ᵐ into ∀)

[Jihoon Hyun]

Thanks, it should take some time for me to digest..

[Yury G. Kudryashov]

If you unfold everything, you get (h₁.ae h).mono fun a ha => h₂.ae ha