Setting up appropriate definitions for Lusin-Novikov

Stream: maths

[Connor Gordon]

I am currently attempting to formalize a proof of the Lusin-Novikov theorem in descriptive set theory, namely the proof in the following paper: Lusin-Novikov.pdf

So far I've set up the following for the spaces X and Y, and the function f between them.

variable {α : Type*} [tα : TopologicalSpace α] [pα : PolishSpace α]
variable {β : Type*} [tβ : TopologicalSpace β] [pβ : PolishSpace β]
variable {f : α → β} (fcont : Continuous f)

I'm new to topology in Lean, so I have a few questions regarding how to set up the appropriate definitions.

1. While defining the notion of a partial section (or even a Borel partial section) is pretty straightforward, I'm not really sure how I might define the sigma ideal generated by such partial sections. Is there any machinery in Lean already to do this? I was thinking a subtype of Set α would make sense, but I'm not really sure how to encode the sigma ideal condition into such a subtype.
2. Similarly, I'm not sure the best way to define ℙ. Again a subtype of Set Set α would make sense, and perhaps it wouldn't be too bad to encode the collection being disjoint and the sets being closed, but is there a better way to do it?
3. At some point I need to define what the paper calls (U)^2, the product of U with itself minus its diagonal. I could do this as directly as possible via def sq_minus_diag (U : Set α) := {x : α × α | x.1 ∈ U ∧ x.2 ∈ U ∧ x.1 ≠ x.2}, but is there a better option?

[Pedro Sánchez Terraf]

The first hint is that for finite sets you should use docs#Finset.

[Pedro Sánchez Terraf]

@Felix Weilacher has been formalizing DST recently, perhaps he is interested. I was, also, but I had to stop for a while.

[Connor Gordon]

Is this how subtypes work, syntactically? I came up with these for now (with the definition of I being a placeholder until I figure out how to generate a sigma ideal).

/- To be replaced with actual definition once I have it -/
def I := {C : Set α // ∀ x ∈ C, ∀ y ∈ C, x ≠ y → f x ≠ f y}
def P := {F : Finset (Set α) // ∀ C₁ ∈ F, ∀ C₂ ∈ F,
  C₁ ∩ C₂ = ∅ ∧ ∀ C ∈ F, IsClosed C}

However, when I attempt to define what it means for a family to be null using this type, I get an error.

def IsNull (F : P) := F=F

typeclass instance problem is stuck, it is often due to metavariables
  TopologicalSpace ?m.1010

I'm assuming I have somehow screwed up the definition of a subtype, but I don't know how it works well enough to see what I did wrong.

[Ruben Van de Velde]

Is a subtype of a topological space always a topological space?

[Connor Gordon]

I think so? A subtype should correspond to some subset of the original space, which we can equip with the subspace topology.

[Connor Gordon]

In the meantime, I've tried to write a statement for the first observation on the second page of the paper, and I'm getting a few errors. Here's what I wrote

theorem obs1 {γ : Type*} [MetricSpace γ] [SeparableSpace γ] {U : Set γ} (Ucl := IsClosed U) {ε : ℝ} (εpos : ε > 0) :
  ∃ V : ℕ → Set γ, ∃ W : ℕ → Set γ, sq_minus_diag U = ⋃ n : ℕ, ((V n) × (W n)) ∧
  ∀ n : ℕ, IsClosed (V n) ∧ IsClosed (W n) ∧ Metric.diam (V n) ≤ ε ∧
  Metric.diam (W n) ≤ ε := by sorry

The first thing it doesn't like is the [SeparableSpace γ], for which I'm getting the following error message:

invalid binder annotation, type is not a class instance
  ?m.1226
use the command `set_option checkBinderAnnotations false` to disable the check

It also doesn't like the sq_minus_diag U = ⋃ n : ℕ, ((V n) × (W n)), for which I'm getting the following error message:

type mismatch
  ↑(V n) × ↑(W n)
has type
  Type u_3 : Type (u_3 + 1)
but is expected to have type
  Set ?m.1493 : Type ?u.1491

Any ideas what I'm doing wrong here?

(Also would this sort of discussion be better suited for #lean4? I'm not sure what the correct feed is for this.)

[Felix Weilacher]

I also have not been working on lean much lately, so some of my library knowledge may be out of date.

Connor Gordon said:

While defining the notion of a partial section (or even a Borel partial section) is pretty straightforward, I'm not really sure how I might define the sigma ideal generated by such partial sections. Is there any machinery in Lean already to do this? I was thinking a subtype of Set α would make sense, but I'm not really sure how to encode the sigma ideal condition into such a subtype.

One quirk of mathlib is there is a lot of infrastructure set up for filters that is not there for ideals. Often, even if the ideal is a bit more intuitive to think about, it's better to just work with the dual filter. For generating a sigma filter, you can use docs#Filter.countableGenerate

[Felix Weilacher]

Connor Gordon said:

At some point I need to define what the paper calls (U)^2, the product of U with itself minus its diagonal. I could do this as directly as possible via def sq_minus_diag (U : Set α) := {x : α × α | x.1 ∈ U ∧ x.2 ∈ U ∧ x.1 ≠ x.2}, but is there a better option?

Maybe U ×ˢ U \ (diagonal α)

[Felix Weilacher]

Connor Gordon said:

Is this how subtypes work, syntactically? I came up with these for now (with the definition of I being a placeholder until I figure out how to generate a sigma ideal).

/- To be replaced with actual definition once I have it -/
def I := {C : Set α // ∀ x ∈ C, ∀ y ∈ C, x ≠ y → f x ≠ f y}
def P := {F : Finset (Set α) // ∀ C₁ ∈ F, ∀ C₂ ∈ F,
  C₁ ∩ C₂ = ∅ ∧ ∀ C ∈ F, IsClosed C}

Why do you want I and P to be subtypes? It is probably better to just define sets (or ideals/filters) here.

[Felix Weilacher]

Connor Gordon said:

def IsNull (F : P) := F=F


typeclass instance problem is stuck, it is often due to metavariables
  TopologicalSpace ?m.1010

In paper mathematics, people often say that they are making a definition only for certain types of objects, even when the definition is valid for a much broader class of objects, because the general definition is not very interesting and/or well behaved without some extra assumptions about the objects.

In lean/mathlib, it is usually best to avoid this. For example, here, "null" makes sense for arbitrary elements of Finset (Set α).

[Felix Weilacher]

I can't tell what is causing your error message without seeing the whole code, but having this be a predicate on Finset (Set α) might help and is the right decision anyways.

[Felix Weilacher]

Connor Gordon said:

It also doesn't like the sq_minus_diag U = ⋃ n : ℕ, ((V n) × (W n)), for which I'm getting the following error message:

type mismatch
  ↑(V n) × ↑(W n)
has type
  Type u_3 : Type (u_3 + 1)
but is expected to have type
  Set ?m.1493 : Type ?u.1491

I'm pretty sure it's that you need to use Set.prod, written ×ˢ. Right now it is taking the subtypes induced by V n and W n and taking the product of those types.

[Felix Weilacher]

Another word of warning: Metric.diam will return 0 for sets with infinite diameter. When I've done things similar to this, I've usually found docs#EMetric.diam to be better to use.

[Connor Gordon]

Thanks for all the tips! After taking a break to formalize the two "observations" in the paper, I'm back to trying to get these definitions working. Towards using the dual filter idea, I attempted to define the set of complements of Borel partial sections as follows:

def BorelPartialSection (A : Set α) : Prop := MeasurableSet A ∧ ∀ x ∈ A, ∀ y ∈ A, x ≠ y → f x ≠ f y
def I₀ := {A : Set α | BorelPartialSection Aᶜ}

However, when I do this, I get the error message

invalid occurrence of universe level 'u_3' at 'I₀', it does not occur at the declaration type, nor it is explicit universe level provided by the user, occurring at expression
  BorelPartialSection.{u_3, u_1} (compl.{u_1} A)
at declaration body
  fun {α : Type u_1} [MeasurableSpace α] => {A : Set α | BorelPartialSection Aᶜ}

I'm assuming this is a classic instance of me not knowing how set builder notation works in Lean, but could I get some help defining what I actually want this to be?

[Ruben Van de Velde]

I think I've only seen that if there's another error elsewhere, though I'm not sure what it would be here. Maybe try giving I0 an explicit type?

[Yaël Dillies]

BorelPartialSection has an extra f argument, right? You should provide it in the set builder notation

[Yaël Dillies]

It would be easier for me to check whether my hunch is correct if you gave us a mwe though

[Yaël Dillies]

#mwe

[Connor Gordon]

f is declared as a global variable. Where should it be in the set builder notation?
MWE.lean

[Yaël Dillies]

There's no such thing as a "global variable" in Lean 4 (it was a thing in Lean 3, and it was pretty buggy)

[Yaël Dillies]

Here's something that should work:

import Mathlib.Topology.MetricSpace.Polish
import Mathlib.MeasureTheory.Constructions.Polish

variable {α : Type*} [tα : TopologicalSpace α] [mα : MeasurableSpace α]
  [pα : PolishSpace α]
variable {β : Type*} [tβ : TopologicalSpace β] [mβ : MeasurableSpace β]
  [pβ : PolishSpace β]
variable {f : α → β} (fcont : Continuous f)

def BorelPartialSection (f : α → β) (A : Set α) : Prop :=
  MeasurableSet A ∧ A.InjOn f

def I₀ (f : α → β) : Set (Set α) := {A : Set α | BorelPartialSection f Aᶜ}

[Yaël Dillies]

I took the freedom to use docs#Set.InjOn since it will make your life easier down the line

[Connor Gordon]

That worked, thanks so much! I went ahead and did the rest of the relevant definitions as well, as shown here:

variable {α : Type*} [tα : TopologicalSpace α] [mα : MeasurableSpace α]
  [pα : PolishSpace α]
variable {β : Type*} [tβ : TopologicalSpace β] [mβ : MeasurableSpace β]
  [pβ : PolishSpace β]
variable {f : α → β} (fcont : Continuous f)
variable {F : Finset (Set α)} (Fdisj : ∀ C₁ ∈ F, ∀ C₂ ∈ F, C₁ ∩ C₂ = ∅)
  (Fclosed : ∀ C ∈ F, IsClosed C)

def BorelPartialSection (f : α → β) (A : Set α) : Prop :=
  MeasurableSet A ∧ A.InjOn f
def IDual₀ (f : α → β) : Set (Set α) := {A : Set α | BorelPartialSection f Aᶜ}
def IDual (f : α → β) : Filter α := countableGenerate (IDual₀ f)
def I (f : α → β) : Set (Set α) := {A : Set α | Aᶜ ∈ (IDual f).sets}
def FBorelCover (B : Set α → Set β) (G : Finset (Set α)) :=
  ⋃ C ∈ G, B C = Set.univ ∧ ∀ C ∈ G, MeasurableSet (B C)
def BorelCover (B : ℕ → Set β) :=
  ⋃ n : ℕ, B n = Set.univ ∧ ∀ n : ℕ, MeasurableSet (B n)
def IsNull (f : α → β) (G : Finset (Set α)) : Prop :=
  ∃ B : Set α → Set β, FBorelCover B G ∧ ∀ C ∈ G, C ∩ f ⁻¹' (B C) ∈ I f
def sq_minus_diag (U : Set α) := {x : α × α | x.1 ∈ U ∧ x.2 ∈ U ∧ x.1 ≠ x.2}

(If you think I could improve any of these definitions, please let me know.)

I'm now attempting to formulate the statements of Lemmas 1 and 2 in the paper, and I'm running into a few issues. The first one I'm going for is Lemma 2, for which I want to write something like

lemma lem2 {A : ℕ → Set β} (ABC : BorelCover A)
  (hA : ∀ n : ℕ, IsNull f {C ∩ f⁻¹' (A n) | C ∈ F}) : IsNull f F := sorry

Lean is not liking the {C ∩ f⁻¹' (A n) | C ∈ F}, as it wants a Finset α but is getting a Set α. Is there a way for me to write this set as a finset?

For Lemma 1, this is somewhat silly, but I'm not actually sure how to write the doubleton set {V n, W n} as a Finset α rather than a Set α. How would I do this?

[Connor Gordon]

I'm also trying to prove a convenience lemma that members of a non-null family of sets are nonempty. I've started the proof below, where the key idea is that if we did have an empty set, then we could pick our Borel cover to assign all of Y to the empty set and have everything else be empty.

lemma aux2 (Fnonnull : ¬IsNull f F) : ∀ C ∈ F, C ≠ ∅ := by
  intro C hC hcont
  have : IsNull f F := by
    rw[IsNull]
    set B : Set α → Set β := fun C => if C = ∅ then Set.univ else ∅ with B_def
    sorry
  sorry

However, this is raising the error

failed to synthesize instance
  Decidable (C = ∅)

Is there any way to get around this issue?

[Matt Diamond]

re: decidability, you can open Classical in the file to make all Props decidable (assuming you don't care about constructivity/computability)

[Matt Diamond]

for your lemma 1 question, Lean should be able to create a Finset literal if it knows what the expected type is... for example, ({1, 2} : Finset ℕ) type-checks perfectly well

[Kevin Buzzard]

Just use the classical tactic at the beginning of the proof, that's much better than opening it for all the file

[Connor Gordon]

The classical tactic worked, thanks!

I'm still having trouble on the two lemmas, though. For the first, I've written the following:

lemma lem1 {V W : ℕ → Set α} (Udecomp : sq_minus_diag U = ⋃ n : ℕ, V n ×ˢ W n)
  (VWnull : ∀ n : ℕ, IsNull f (F ∪ ({V n, W n} : Finset (Set α)))) :
    IsNull f (F ∪ {U}) := by sorry

The second line is giving me these errors:

failed to synthesize instance
  Insert (Set α) (Finset (Set α))

failed to synthesize instance
  Union (Finset (Set α))

And the third is giving me this:

failed to synthesize instance
  Union (Finset (Set α))

For the second, I've written

lemma lem2 {A : ℕ → Set β} (ABC : BorelCover A)
  (hA : ∀ n : ℕ, IsNull f {C ∩ f⁻¹' (A n) | C ∈ F}) : IsNull f F := sorry

But am getting the error message

application type mismatch
  IsNull f {x | ∃ C, C ∈ F ∧ C ∩ f ⁻¹' A n = x}
argument
  {x | ∃ C, C ∈ F ∧ C ∩ f ⁻¹' A n = x}
has type
  Set (Set α) : Type u_1
but is expected to have type
  Finset (Set α) : Type u_1

Any ideas how to fix these?

[Ruben Van de Velde]

Not enough code for us to see the error for ourselves

[Connor Gordon]

Apologies, here's a MWE

import Mathlib.Topology.MetricSpace.Polish
import Mathlib.MeasureTheory.Constructions.Polish
import Mathlib.Topology.MetricSpace.CantorScheme
import Mathlib.Topology.Bases


-- Set variables:
variable {α : Type*} [tα : TopologicalSpace α] [mα : MeasurableSpace α]
  [pα : PolishSpace α]
variable {β : Type*} [tβ : TopologicalSpace β] [mβ : MeasurableSpace β]
  [pβ : PolishSpace β]
variable {f : α → β} (fcont : Continuous f)
variable {F : Finset (Set α)} (Fdisj : ∀ C₁ ∈ F, ∀ C₂ ∈ F, C₁ ∩ C₂ = ∅)
  (Fclosed : ∀ C ∈ F, IsClosed C)

open Filter

-- Important definitions:
def BorelPartialSection (f : α → β) (A : Set α) : Prop :=
  MeasurableSet A ∧ A.InjOn f
def IDual₀ (f : α → β) : Set (Set α) := {A : Set α | BorelPartialSection f Aᶜ}
def IDual (f : α → β) : Filter α := countableGenerate (IDual₀ f)
def I (f : α → β) : Set (Set α) := {A : Set α | Aᶜ ∈ (IDual f).sets}
def FBorelCover (B : Set α → Set β) (G : Finset (Set α)) :=
  ⋃ C ∈ G, B C = Set.univ ∧ ∀ C ∈ G, MeasurableSet (B C)
def BorelCover (B : ℕ → Set β) :=
  ⋃ n : ℕ, B n = Set.univ ∧ ∀ n : ℕ, MeasurableSet (B n)
def IsNull (f : α → β) (G : Finset (Set α)) : Prop :=
  ∃ B : Set α → Set β, FBorelCover B G ∧ ∀ C ∈ G, C ∩ f ⁻¹' (B C) ∈ I f
def sq_minus_diag (U : Set α) := {x : α × α | x.1 ∈ U ∧ x.2 ∈ U ∧ x.1 ≠ x.2}

lemma lem1 {V W : ℕ → Set α} (Udecomp : sq_minus_diag U = ⋃ n : ℕ, V n ×ˢ W n)
  (VWnull : ∀ n : ℕ, IsNull f (F ∪ ({V n, W n} : Finset (Set α)))) :
    IsNull f (F ∪ {U}) := by sorry

lemma lem2 {A : ℕ → Set β} (ABC : BorelCover A)
  (hA : ∀ n : ℕ, IsNull f {C ∩ f⁻¹' (A n) | C ∈ F}) : IsNull f F := sorry

[Ruben Van de Velde]

lemma lem1 [DecidableEq (Set α)] {V W : ℕ → Set α} (Udecomp : sq_minus_diag U = ⋃ n : ℕ, V n ×ˢ W n)
  (VWnull : ∀ n : ℕ, IsNull f (F ∪ ({V n, W n} : Finset (Set α)))) :
    IsNull f (F ∪ {U}) := by sorry

For technical reasons, we need to be able to tell whether V n = W n in a decidable way

[Ruben Van de Velde]

For lem2, that set builder notation only works for Set, not Finset

[Ruben Van de Velde]

Alternative:

open Classical in
lemma lem2 {A : ℕ → Set β} (ABC : BorelCover A)
  (hA : ∀ n : ℕ, IsNull f (F.image fun C => C ∩ f⁻¹' (A n))) : IsNull f F := sorry

[Connor Gordon]

That works, thank you!

In the meantime, I've been trying to prove that I is closed under countable unions, as we would expect of a sigma ideal. The only issue is that I need Lean to recognize IDual as a CountableInterFilter, which it should be by definition of countableGenerate in docs#Filter.countableGenerate, but I'm not sure how to actually get Lean to realize it.

Also, for the proof of Lemma 2, part of the proof is extracting relevant Borel covers based on the fact that each of the families are null. In particular, I need a Borel cover for each n : ℕ. I suppose I could do something like

lemma lem2 {A : ℕ → Set β} (ABC : BorelCover A)
  (hA : ∀ n : ℕ, IsNull f (F.image fun C => C ∩ f⁻¹' (A n))) : IsNull f F := by
    rw[IsNull]
    simp only [IsNull._eq_1, Finset.mem_image, forall_exists_index,
      and_imp, forall_apply_eq_imp_iff₂] at hA
    set B : ℕ → Set α → Set β := fun n => choose (hA n) with B_def
    sorry

but this seems absolutely awful to work with. Is there something better I can do?

[Connor Gordon]

I've been working on the proof of Lemma 1 (after the simplifying reductions have been made) in in MWE.lean, so in particular I've defined the set B U as written in the paper and am currently trying to show that the resulting cover is indeed a Borel cover. I have shown it's a cover, and all that remains is to show that B U, which is defined to be Y minus the union of the other B Cs for all C in F. I know that Y and all of the B Cs are Borel, so I would like to apply MeasurableSet.iInter to finish, but it's not recognizing that the intersection in question is actually finite. Any ideas how I could address this?

[Felix Weilacher]

is F a Finset? Maybe docs#Finset.measurableSet_biInter

[Connor Gordon]

Yep, that worked!

[Matt Diamond]

Did you figure out the CountableInterFilter instance issue or are you still looking for a solution to that?

[Connor Gordon]

I am still looking for a solution to that as well as advice for the picking Borel covers for lemma 2 part, I've just been working on some other stuff in the meantime.

[Connor Gordon]

Actually never mind on the CountableInterFilter one, I just needed to unfold the definition of Idual and it figured it out!

[Matt Diamond]

That works! I was just going to suggest marking the definition as @[reducible] but I wasn't sure if that would cause other problems

[Connor Gordon]

I've been continuing to work on Lemma 2 in MWE.lean. I've now managed to reduce the problem to proving

have Bcover : ∀ n : ℕ, FBorelCover (B n) F ∧
      ∀ (C : Set α), C ∈ F → C ∩ f ⁻¹' A n ∩ f ⁻¹' (B n) (C) ∈ I f

This should follow pretty quickly from the definitions of B and B', but getting anything out of Classical.choose can be a hassle. Does anyone have any idea how I could do this or how to better define B and B' to avoid this issue?

[Connor Gordon]

Never mind, aesop saved the day! (As a stylistic note, what are the guidelines behind using aesop or simp in proofs? Should I always use aesop? or simp? and put the replacements, or is it sometimes fine to leave them as-is?)

[Ruben Van de Velde]

At least for simp, it's fine, as long as it proves the (sub)goal. We don't like proofs that do simp; some more work that depends on the exact goal that simp left

[Connor Gordon]

I just finished the proof of Lemma 1 after the reductions at the beginning, so now it's time to actually implement those reductions! Getting to the single cover by taking unions seems simple enough, so I'm mainly wondering how to do the disjointifying part. I found Docs#Disjointed, but this seems to be collections of set indexed by the naturals, where I would want a collection of sets indexed by a Finset. Does there exist infrastructure to do this already in Mathlib, or should I attempt to do that myself (if it's the latter, is there a way to get an ordering on a Finset?)

[Connor Gordon]

Alright, I have implemented the taking unions step, barring some difficulties in proving that the unions do what I want. I now have a Borel cover for each natural number such that all of them agree on the sets indexed by F. I would like to disjointify them in some coherent way such that the disjointified versions also agree on the sets indexed by F. Any ideas on how to do this?

[Connor Gordon]

After some more thought, I think I know what I would like to do for the structure of the disjointifying, I just need some help on one step. I would like to place a linear ordering on F, perhaps by using `Finset.toList, and then define the Borel cover via the same method as is done is the Disjointed file. Is there a canonical way to put an ordering on a Finset in a way that's usable? I might also need to induct on it to prove the sets are Borel, so if that's possible that would be fantastic.

[Felix Weilacher]

I don't understand why you want to disjointify in this proof

[Connor Gordon]

You know, now that you mention it, you're right. I never stopped to think whether that partition statement was necessary. All I needed was that the sets for V n and W n were disjoint from the sets for all the Cs, and that's much easier to work with (and I just finished doing it). Thank you for the sanity check!