# Zulip Chat Archive

## 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