ae eq of preimages

Stream: maths

[Yury G. Kudryashov]

I have the following lemma:

theorem Filter.EventuallyEq.of_forall_open_preimage [TopologicalSpace X]
  [T0Space X] [SecondCountableTopology X] {f g : α → X} {l : Filter α}
  [CountableInterFilter l] (a : ∀ (U : Set X), IsOpen U → f ⁻¹' U =ᶠ[l] g ⁻¹' U) : f =ᶠ[l] g

with the main application in mind is l = μ.ae, so two functions are a.e. equal if for any open set, the preimages of this open set are a.e. equal.

[Yury G. Kudryashov]

My question is: do I need all the typeclass assumptions?

[Yury G. Kudryashov]

Clearly, I need T0 but I don't have counterexamples for countability assumptions.

[Yury G. Kudryashov]

BTW, do we have this lemma (e.g., for Measure.ae only)?

[Yury G. Kudryashov]

I see that we have docs4#MeasureTheory.Integrable.ae_eq_of_forall_set_integral_eq but that's a different story.

[Felix Weilacher]

With l not countably complete: take X = alpha = N, l and the topology both the collection of co-finite sets, and f and g any two bijections from N to itself. Then for any open (co-finite) U, the preimages of U are in l, so the condition holds. But f and g need not be a.e. equal.

With X not second countable: Same idea, but with an uncountable set in place of N, and the filter/topology of co-countable sets.

[Yury G. Kudryashov]

Thank you! I'll add these to the docstring.

[Felix Weilacher]

BTW this doesn't really seem like statement about topological spaces, although I can see how that's a case of interest. Do you include a more general statement where X just has a countable collection of sets separating points (taking the place of the opens in the hypothesis a) ?

[Yury G. Kudryashov]

Probably, I should.

[Yury G. Kudryashov]

Or just write a TODO section in the module docstring and wait till someone needs it.

[Yury G. Kudryashov]

BTW, is there a name for a σ-algebra with this property (there exists a countable set of mesaurable sets that separates points)?

[Yury G. Kudryashov]

Because asking for [TopologicalSpace X] [SecondCountableTopology X] [OpensMeasurableSpace X] is possible but looks a bit strange.

[Felix Weilacher]

I'm not sure about a name. For sigma-algebras, i guess one could use docs#measurable_singleton_class plus docs#measurable_space.countably_generated, but even a sigma-algebra is more structure than this statement needs.

[Yury G. Kudryashov]

I'm going to add

class HasCountableSeparatingOn (α : Type _) (p : Set α → Prop) (t : Set α) : Prop where
  protected out : ∃ S : Set (Set α), S.Countable ∧ (∀ s ∈ S, p s) ∧
    t.Pairwise fun x y ↦ ∃ s ∈ S, Xor' (x ∈ s) (y ∈ s)

with instances for IsOpen, IsClosed, and MeasurableSet.

[Pedro Sánchez Terraf]

Yury G. Kudryashov said:

BTW, is there a name for a σ-algebra with this property (there exists a countable set of mesaurable sets that separates points)?

I believe that “countably separated” is an appropriate term, cf. this Transactions paper ( p. 126) by Glimm.

[Felix Weilacher]

Yury G. Kudryashov said:

I'm going to add

class HasCountableSeparatingOn (α : Type _) (p : Set α → Prop) (t : Set α) : Prop where
  protected out : ∃ S : Set (Set α), S.Countable ∧ (∀ s ∈ S, p s) ∧
    t.Pairwise fun x y ↦ ∃ s ∈ S, Xor' (x ∈ s) (y ∈ s)

with instances for IsOpen, IsClosed, and MeasurableSet.

Awesome, thanks!

[Yury G. Kudryashov]

!4#5218

[Felix Weilacher]

Should Topology.CountableSeparatingOn be moved into perhaps MeasureTheory.Constructions.BorelSpace.Basic? I assume the former file is a thing only because of the port?

[Yury G. Kudryashov]

But it doesn't need measure theory.

[Yury G. Kudryashov]

IMHO, it doesn't hurt to have an extra file.