## Stream: new members

### Topic: How to show a set is an σ-algebra

#### Peter Hansen (Jul 18 2022 at 22:27):

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 (Jul 18 2022 at 22:45):

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 (Jul 19 2022 at 02:00): just wanted to note that writing definitions in tactic mode is generally discouraged (or so I've heard) #### Junyan Xu (Jul 19 2022 at 02:09): 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 (Jul 19 2022 at 02:13): 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 (Jul 19 2022 at 02:17): 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 (Jul 19 2022 at 02:19): does Lean just take your word for it when you type a definition? #### Yaël Dillies (Jul 19 2022 at 02:20): (500 : fin 4) = 0 because it loops around. #### Matt Diamond (Jul 19 2022 at 02:21): oh huh, it just does 500 mod 4? #### Matt Diamond (Jul 19 2022 at 02:21): I guess that makes sense #### Kyle Miller (Jul 19 2022 at 02:26): 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 (Jul 19 2022 at 02:26): gotcha... good to know! #### Kyle Miller (Jul 19 2022 at 02:27): If you want to pull back the curtain, you can try set_option pp.numerals false #### Kyle Miller (Jul 19 2022 at 02:27): #check 37 /- bit1 (bit0 (bit1 (bit0 (bit0 has_one.one)))) : ℕ -/  #### Peter Hansen (Jul 19 2022 at 02:37): 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 (Jul 19 2022 at 03:09): feel free to share what you have so far (if you want to) #### Kevin Buzzard (Jul 19 2022 at 03:11): 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 (Jul 19 2022 at 03:24): 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 (Jul 19 2022 at 03:32): 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 (Jul 19 2022 at 03:34): @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 (Jul 19 2022 at 03:40): ah, I forgot about ext... very nice #### Junyan Xu (Jul 19 2022 at 04:06): 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 (Jul 19 2022 at 04:18): I'm curious about why there's a ∨ false there #### Junyan Xu (Jul 19 2022 at 04:34): docs#list.mem is an inductive definition with base case list.mem a list.nil = false for the empty list. #### Matt Diamond (Jul 19 2022 at 04:35): ah, that makes sense #### Junyan Xu (Jul 19 2022 at 04:51): 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 (Jul 19 2022 at 07:02):

That change set _ is a bad idea

#### Eric Wieser (Jul 19 2022 at 07:03):

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

#### Junyan Xu (Jul 19 2022 at 07:36):

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 (Jul 19 2022 at 07:38): That change set _ is a bad idea Yes, change seems to introduce an id, but it doesn't seem to matter much ... #### Eric Wieser (Jul 19 2022 at 09:23): measurable_set' := ({{0,1}, {2,3}, {0,1,2,3}, ∅} : set _) is still the wrong spelling #### Eric Wieser (Jul 19 2022 at 09:23): Use measurable_set' := (∈ {{0,1}, {2,3}, {0,1,2,3}, ∅}), #### Eric Wieser (Jul 19 2022 at 09:25): 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 (Jul 19 2022 at 10:27): 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 (Jul 19 2022 at 11:04): 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 (Jul 19 2022 at 15:44): 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 (Jul 19 2022 at 15:44): 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 (Jul 19 2022 at 22:53):

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 (Jul 19 2022 at 23:37):

Looks like it: #15538

#### Junyan Xu (Jul 20 2022 at 00:41):

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

Last updated: Dec 20 2023 at 11:08 UTC