How to show a set is an σ-algebra

Stream: new members

[Peter Hansen]

How do I show that Σ = { ∅, {0, 1}, {2, 3}, {0, 1, 2, 3} } is a σ-algebra on X = {0, 1, 2, 3} in Lean?

I think it is done by defining a relevant object of the measurable_space-structure:

structure measurable_space (α : Type*) :=
(measurable_set' : set α → Prop)
(measurable_set_empty : measurable_set' ∅)
(measurable_set_compl : ∀ s, measurable_set' s → measurable_set' sᶜ)
(measurable_set_Union : ∀ f : ℕ → set α, (∀ i, measurable_set' (f i)) → measurable_set' (⋃ i, f i))

First I need to choose the right (α : Type*). I think the type should correspond to the set X = {0, 1, 2, 3}. I have a vague understanding of subtypes. Do I simply use {n : ℕ // n < 4}?

Next I need to specify measurable_set', which has type set α → Prop. I think I can define it as

import tactic
import measure_theory.measurable_space_def

def mysig : measurable_space (fin 4) :=
begin
fconstructor,
intro N,
exact N = {0, 1} ∨ N = {2, 3} ∨ N = {0, 1, 2, 3} ∨ N = ∅,
simp,
sorry,
sorry,
end

With this approach, I run into problems when trying to show closure under complementation.

[Junyan Xu]

fin 4 is defined to be {n : ℕ // n < 4}, so I think you are using the right thing.
The following includes a proof of empty and compl (fin_cases is sorta slow though), and Union seems to require some additional lemma(s):

def mysig : measurable_space (fin 4) :=
begin
  fconstructor,
  { change set _, exact {{0,1}, {2,3}, {0,1,2,3}, ∅} },
  { exact or.inr (or.inr $ or.inr rfl) /- or `right, right, right, exact rfl` -/ },
  { rintro _ (rfl|rfl|rfl|rfl|⟨⟩),
    { right, left, ext, split; fin_cases x; dec_trivial },
    { left, ext, split; fin_cases x; dec_trivial },
    { right, right, right, ext, split; fin_cases x; dec_trivial },
    { right, right, left, ext, split; fin_cases x; dec_trivial }, },
  sorry,
end

[Matt Diamond]

just wanted to note that writing definitions in tactic mode is generally discouraged (or so I've heard)

[Junyan Xu]

Matt Diamond said:

just wanted to note that writing definitions in tactic mode is generally discouraged (or so I've heard)

I agree; even though we're only using tactics that are safe for the data fields (e.g. constructor, intro, exact, change, dsimp, apply, refine), it would be nicer to write { measurable_set' := ... , measurable_set_empty := ..., ... } so that it's evident which field you are working on.

[Violeta Hernández]

Matt Diamond said:

just wanted to note that writing definitions in tactic mode is generally discouraged (or so I've heard)

The idea is that most tactics are meant for propositions, and might do very complicated or unpredictable things in order to reach their results, which is bad when you're trying to define a concrete object. There are a few you can safely use - I'd like to add by_cases to the aforementioned list, and rw if you really know what you're doing.

[Matt Diamond]

btw, I must be missing something about how Lean works because def mySet : set (fin 4) := {1, 2, 500} seems to typecheck just fine

[Matt Diamond]

does Lean just take your word for it when you type a definition?

[Yaël Dillies]

(500 : fin 4) = 0 because it loops around.

[Matt Diamond]

oh huh, it just does 500 mod 4?

[Matt Diamond]

I guess that makes sense

[Kyle Miller]

That's sort of a side-effect to how numerals are implemented. Under the hood, they're all expressions made from docs#bit0, docs#bit1, docs#has_zero.zero and docs#has_one.one, so you're forced to allow every natural number.

[Matt Diamond]

gotcha... good to know!

[Kyle Miller]

If you want to pull back the curtain, you can try set_option pp.numerals false

[Kyle Miller]

#check 37
/-
bit1 (bit0 (bit1 (bit0 (bit0 has_one.one)))) : ℕ
-/

[Peter Hansen]

Thanks for the help and for confirming that I was somewhat on the right track :) Using fin_cases worked nicely for showing closure under complementation. I'm still trying to show closure under countable unions. I thought that since this was such a simple example it would be easy to formalize. Not the case for me at least.

[Matt Diamond]

feel free to share what you have so far (if you want to)

[Kevin Buzzard]

General theorems are much easier to formalise than examples in Lean 3, because Lean 3 is not a "computer"; it is not designed to compute. Lean 4 should be much better in this regard.

[Matt Diamond]

now I'm curious if there's an easy way to prove a statement like ↑(finset.fin_range 4) = {0, 1, 2, 3}

[Kyle Miller]

It might be nice to have a tactic (maybe a norm_num plugin?) that reduces basic set expressions, normalizing set literals like {2, 4, 4, 1, 3} -> {1, 2, 3, 4} and using that to efficiently compute unions, intersections, and set differences.

[Kyle Miller]

@Matt Diamond For this small example, at least this works:

example : ↑(finset.fin_range 4) = ({0, 1, 2, 3} : set (fin 4)) :=
begin
  ext x, fin_cases x; simp,
end

[Matt Diamond]

ah, I forgot about ext... very nice

[Junyan Xu]

Actually these are almost defeq:

example : (finset.fin_range 4 : set (fin 4)) = {i | i = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3 ∨ false} := rfl
/- comes from `list.mem` -/
example : ({0, 1, 2, 3} : set (fin 4)) = {i | i = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3} := rfl
/- comes from `set.has_insert` and `set.has_singleton` -/

Should we make them agree (for example, by redefining docs#set.has_singleton)?

[Matt Diamond]

I'm curious about why there's a ∨ false there

[Junyan Xu]

docs#list.mem is an inductive definition with base case list.mem a list.nil = false for the empty list.

[Matt Diamond]

ah, that makes sense

[Junyan Xu]

Using a lemma, I was able to reduce it to a finite problem (16 cases); then the same solution for complement works, but it takes like 1 minute on my machine:

import tactic
import measure_theory.measurable_space_def

lemma Sup_mem_of_sup_mem {α} [complete_lattice α] (m : multiset α) (p : α → Prop)
  (h : ∀ s ∈ m.powerset, p (multiset.sup s))
  (f : ℕ → α) (hf : ∀ i, f i ∈ m) : p (⨆ i, f i) :=
begin
  classical,
  have hff : (set.range f).finite,
  { apply m.to_finset.finite_to_set.subset,
    rintro _ ⟨i, rfl⟩, rw [finset.mem_coe, multiset.mem_to_finset], exact hf i },
  change p (Sup _),
  rw [← hff.coe_to_finset, ← finset.sup_id_eq_Sup, finset.sup_def, multiset.map_id],
  apply h,
  rw [multiset.mem_powerset, finset.val_le_iff_val_subset],
  intros a ha, obtain ⟨i, rfl⟩ := hff.mem_to_finset.1 ha, exact hf i,
end

set_option class.instance_max_depth 100

open or
def mysig : measurable_space (fin 4) :=
begin
  fconstructor,
  { change set _, exact {{0,1}, {2,3}, {0,1,2,3}, ∅} },
  { exact inr (inr $ inr rfl) /- or `right, right, right, exact rfl` -/ },
  { rintro _ (rfl|rfl|rfl|rfl|⟨⟩),
    { right, left, ext, split; fin_cases x; dec_trivial },
    { left, ext, split; fin_cases x; dec_trivial },
    { right, right, right, ext, split; fin_cases x; dec_trivial },
    { right, right, left, ext, split; fin_cases x; dec_trivial } },
  { intros f hf, apply Sup_mem_of_sup_mem,
    swap 3, { exact {{0,1}, {2,3}, {0,1,2,3}, ∅} },
    swap 2, { intro i, obtain h|h|h|h := hf i,
      exacts [inl h, inr $ inl h, inr $ inr $ inl h, inr $ inr $ inr $ inl h] },
    { intros s x, fin_cases x; dsimp [multiset.sup],
      work_on_goal 1 { right, right, right },
      work_on_goal 2 { left },
      work_on_goal 3 { right, left },
      work_on_goal 4 { right, right, left },
      work_on_goal 5 { right, right, left },
      work_on_goal 6 { right, right, left },
      work_on_goal 7 { right, right, left },
      work_on_goal 8 { right, right, left },
      work_on_goal 9 { right, right, right },
      work_on_goal 10 { left },
      work_on_goal 11 { right, left },
      work_on_goal 12 { right, right, left },
      work_on_goal 13 { right, right, left },
      work_on_goal 14 { right, right, left },
      work_on_goal 15 { right, right, left },
      work_on_goal 16 { right, right, left },
      all_goals { ext, split; fin_cases x; dec_trivial } } },
end

[Eric Wieser]

That change set _ is a bad idea

[Eric Wieser]

Use refine (∈ (_ : set _)) there instead ( or better, combine that with the next line

[Junyan Xu]

Using finset computability/decidability, I'm able to make it faster and more automated:

import tactic
import measure_theory.measurable_space_def

lemma Sup_mem_of_sup_mem {α} [complete_lattice α] (m : multiset α) (p : α → Prop)
  (h : ∀ s ∈ m.powerset, p (multiset.sup s))
  (f : ℕ → α) (hf : ∀ i, f i ∈ m) : p (⨆ i, f i) :=
begin
  classical,
  have hff : (set.range f).finite,
  { apply m.to_finset.finite_to_set.subset,
    rintro _ ⟨i, rfl⟩, rw [finset.mem_coe, multiset.mem_to_finset], exact hf i },
  change p (Sup _),
  rw [← hff.coe_to_finset, ← finset.sup_id_eq_Sup, finset.sup_def, multiset.map_id],
  apply h,
  rw [multiset.mem_powerset, finset.val_le_iff_val_subset],
  intros a ha, obtain ⟨i, rfl⟩ := hff.mem_to_finset.1 ha, exact hf i,
end

local notation `f4` := finset (fin 4)
open or

lemma mysig_aux :
  ({{0,1}, {2,3}, {0,1,2,3}, ∅} : set $ set $ fin 4) =
  {↑({0,1}:f4), ↑({2,3}:f4), ↑({0,1,2,3}:f4), ↑(∅:f4)} :=
by { congr; ext; exact (or_false _).symm }

set_option profiler true
/- elaboration of mysig took 20.8s -/
def mysig : measurable_space (fin 4) :=
{ measurable_set' := ({{0,1}, {2,3}, {0,1,2,3}, ∅} : set _),
  measurable_set_empty := inr (inr $ inr rfl),
  measurable_set_compl := begin
    rw [mysig_aux],
    rintro _ (h|h|h|h),
    work_on_goal 4 { rw set.mem_singleton_iff at h },
    all_goals { subst h, rw ← finset.coe_compl,
      dsimp [set.has_insert, -finset.coe_empty],
      change _ = _ ∨ _, simp only [finset.coe_inj], dec_trivial },
  end,
  measurable_set_Union := λ f hf, begin
    rw mysig_aux at hf ⊢,
    fapply Sup_mem_of_sup_mem,
    { exact {↑({0,1}:f4), ↑({2,3}:f4), ↑({0,1,2,3}:f4), ↑(∅:f4)} },
    { rintro s (h|h|h|h|h|h|h|h|h|h|h|h|h|h|h|h|⟨⟨⟩⟩),
      all_goals { subst h, dsimp [multiset.sup, set.has_insert, ← finset.coe_empty],
        change _ = _ ∨ _, simp only [← finset.coe_union, finset.coe_inj], dec_trivial } },
    { intro i, obtain h|h|h|h := hf i,
      exacts [inl h, inr $ inl h, inr $ inr $ inl h, inr $ inr $ inr $ inl h] },
  end }

[Junyan Xu]

That change set _ is a bad idea

Yes, change seems to introduce an id, but it doesn't seem to matter much ...

[Eric Wieser]

measurable_set' := ({{0,1}, {2,3}, {0,1,2,3}, ∅} : set _) is still the wrong spelling

[Eric Wieser]

Use measurable_set' := (∈ {{0,1}, {2,3}, {0,1,2,3}, ∅}),

[Eric Wieser]

The right way to convert from a -> Prop to set is set_of p aka {x | p x}, and the right way to convert in the order direction is (∈ s). If you do it any other way, you'll find that you have to unfold stuff because no lemmas expect you to do things that way

[Yaël Dillies]

Matt Diamond said:

now I'm curious if there's an easy way to prove a statement like ↑(finset.fin_range 4) = {0, 1, 2, 3}

People, please stop using docs#finset.fin_range. Use docs#finset.univ instead.

[Anne Baanen]

Kyle Miller said:

It might be nice to have a tactic (maybe a norm_num plugin?) that reduces basic set expressions, normalizing set literals like {2, 4, 4, 1, 3} -> {1, 2, 3, 4} and using that to efficiently compute unions, intersections, and set differences.

We basically already have this as part of docs#tactic.norm_num.eval_big_operators. The problem with finsets is that you need some way to decide that ({1, 2, 3, 4} : finset (fin 4)) = {1, 2, 3}. But if you can hook up a norm_num front-end to docs#tactic.norm_num.eval_finset it should work.

[Junyan Xu]

Use measurable_set' := (∈ {{0,1}, {2,3}, {0,1,2,3}, ∅}),

Using (∈ ) allow to eliminate change _ = _ ∨ _ , but I also have to modify the statement of Sup_mem_of_sup_mem to use set α instead of α → Prop, otherwise fapply Sup_mem_of_sup_mem fails to unify.

[Junyan Xu]

import tactic
import measure_theory.measurable_space_def

lemma Sup_mem_of_sup_mem {α} [complete_lattice α] (m : multiset α) (p : set α)
  (h : ∀ s ∈ m.powerset, multiset.sup s ∈ p)
  (f : ℕ → α) (hf : ∀ i, f i ∈ m) : (⨆ i, f i) ∈ p :=
begin
  classical,
  have hff : (set.range f).finite,
  { apply m.to_finset.finite_to_set.subset,
    rintro _ ⟨i, rfl⟩, rw [finset.mem_coe, multiset.mem_to_finset], exact hf i },
  change p (Sup _),
  rw [← hff.coe_to_finset, ← finset.sup_id_eq_Sup, finset.sup_def, multiset.map_id],
  apply h,
  rw [multiset.mem_powerset, finset.val_le_iff_val_subset],
  intros a ha, obtain ⟨i, rfl⟩ := hff.mem_to_finset.1 ha, exact hf i,
end

local notation `f4` := finset (fin 4)

lemma mysig_aux :
  ({{0,1}, {2,3}, {0,1,2,3}, ∅} : set $ set $ fin 4) =
  {↑({0,1}:f4), ↑({2,3}:f4), ↑({0,1,2,3}:f4), ↑(∅:f4)} :=
by congr; { ext, exact (or_false _).symm }

open or
set_option profiler true
/- elaboration of mysig took 20.2s -/
def mysig : measurable_space (fin 4) :=
{ measurable_set' := (∈ ({{0,1}, {2,3}, {0,1,2,3}, ∅} : set $ set $ fin 4)),
  measurable_set_empty := inr (inr $ inr rfl),
  measurable_set_compl := begin
    rw [mysig_aux],
    rintro _ (h|h|h|h),
    work_on_goal 4 { rw set.mem_singleton_iff at h },
    all_goals { subst h, rw ← finset.coe_compl,
      dsimp [set.has_insert, -finset.coe_empty],
      simp only [finset.coe_inj], dec_trivial },
  end,
  measurable_set_Union := λ f hf, begin
    rw mysig_aux at hf ⊢,
    fapply Sup_mem_of_sup_mem,
    { exact {↑({0,1}:f4), ↑({2,3}:f4), ↑({0,1,2,3}:f4), ↑(∅:f4)} },
    { rintro s (h|h|h|h|h|h|h|h|h|h|h|h|h|h|h|h|⟨⟨⟩⟩),
      all_goals { subst h, dsimp [multiset.sup, set.has_insert, ← finset.coe_empty],
        simp only [← finset.coe_union, finset.coe_inj], dec_trivial } },
    { intro i, obtain h|h|h|h := hf i,
      exacts [inl h, inr $ inl h, inr $ inr $ inl h, inr $ inr $ inr $ inl h] },
  end }

[Violeta Hernández]

Yaël Dillies said:

People, please stop using docs#finset.fin_range. Use docs#finset.univ instead.

Is this something that can be easily refactored out?

[Yaël Dillies]

Looks like it: #15538

[Junyan Xu]

With more lemmas (some basic ones are missing in mathlib), Lean can do the computation in less than 5 seconds: https://gist.github.com/alreadydone/ba98aa4e04b5f0067960284ef03b4442