## Stream: new members

### Topic: generate_from_le

#### Iocta (Mar 09 2021 at 20:08):

I'm trying to understand the basics of generate_from_le. I don't get what's happening in this step. First of all, what doesm.measurable_set' t say, in English?

lemma generate_from_le' {s : set (set Ω)} {m : measurable_space Ω}
(h :  t  s, m.measurable_set' t) : generate_from s  m :=
assume t, _
-- don't know how to synthesize placeholder
-- context:
-- Ω : Type,
-- _inst_1 : measurable_space Ω,
-- s : set (set Ω),
-- m : measurable_space Ω,
-- h : ∀ (t : set Ω), t ∈ s → m.measurable_set' t,
-- t : set Ω
-- ⊢ (generate_from s).measurable_set' t ≤ m.measurable_set' t

lemma generate_from_le' {s : set (set Ω)} {m : measurable_space Ω}
(h :  t  s, m.measurable_set' t) : generate_from s  m :=
assume t ht, _
-- don't know how to synthesize placeholder
-- context:
-- Ω : Type,
-- _inst_1 : measurable_space Ω,
-- s : set (set Ω),
-- m : measurable_space Ω,
-- h : ∀ (t : set Ω), t ∈ s → m.measurable_set' t,
-- t : set Ω,
-- ht : (generate_from s).measurable_set' t
-- ⊢ m.measurable_set' t

#### Iocta (Mar 09 2021 at 20:12):

First of all, what doesm.measurable_set' t say, in English? I think it means m is a sigma algebra and m.measurable_set' t is its set.

#### Iocta (Mar 09 2021 at 20:15):

But then how does adding an argument take "please show the sigma algebra generate_from s's set t is a subset of the sigma algebra m's set -- the same t" to "please show m is a sigma algebra with set t" (if that's what's happening)?

#### Hanting Zhang (Mar 09 2021 at 20:21):

The type of t is set \Omega. m.measurable_set' t means that t is a measurable subset of the space m. generate_from_le is saying that if s is a collection of measurable subsets of m, then the sigma algebra generated by s is less than or equal to the sigma algebra on m.

#### Iocta (Mar 09 2021 at 20:26):

How does adding the ht argument transform the "less than or equal" goal into the m.measurable_set' t goal?

#### Hanting Zhang (Mar 09 2021 at 20:35):

Proving that (generate_from s).measurable_set' t ≤ m.measurable_set' t is defeq to proving that (generate_from s).measurable_set' t implies m.measurable_set' t

#### Iocta (Mar 09 2021 at 20:36):

How can I see that?

#### Hanting Zhang (Mar 09 2021 at 20:38):

I think what lean is doing is that its treating m.measurable_set' t as a collection of sets of \Omega, i.e. it has type set (set \Omega). Then lean looks at the \le symbol and tries to find an instance of a partial order on sets, which exists. Then lean realizes that you're trying to prove that the thing on the left is a subset of the thing on the right.

#### Hanting Zhang (Mar 09 2021 at 20:39):

And proving that a \subset b unfolds to x \in a implies x in b.

#### Hanting Zhang (Mar 09 2021 at 20:40):

Well yes, but that's not what you want I think. You're trying to find the partial order that defines what m₁.measurable_set' ≤ m₂.measurable_set' means.

#### Hanting Zhang (Mar 09 2021 at 20:43):

Nevermind, what I've said is inaccurate. I think the gist of what I said is probably the right idea, but it might not be a partial order on sets. It should be directly related to lattices?

#### Hanting Zhang (Mar 09 2021 at 20:45):

You could try going into tactic mode and doing unfold (\le) instead of intro ht and see if it unfolds to a implication

#### Iocta (Mar 09 2021 at 20:48):

set_option pp.notation false

lemma generate_from_le' {s : set (set Ω)} {m : measurable_space Ω}
(h :  t  s, m.measurable_set' t) : generate_from s  m :=
begin
intros t,
unfold has_le.le,
unfold preorder.le,
unfold partial_order.le,
unfold semilattice_inf.le,
unfold lattice.le,
unfold linear_order.le,
unfold partial_order.le,
unfold order_bot.le,
unfold bounded_lattice.le,
unfold bounded_distrib_lattice.le,
end
-- 1 goal
-- Ω: Type
-- _inst_1: measurable_space Ω
-- s: set (set Ω)
-- m: measurable_space Ω
-- h: ∀ (t : set Ω), has_mem.mem t s → m.measurable_set' t
-- t: set Ω
-- ⊢ (generate_from s).measurable_set' t → m.measurable_set' t

#### Iocta (Mar 10 2021 at 04:06):

What is the tactic version of this?

lemma generate_from_le {s : set (set α)} {m : measurable_space α}
(h :  t  s, m.measurable_set' t) : generate_from s  m :=
assume t (ht : generate_measurable s t), ht.rec_on h
(measurable_set_empty m)
(assume s _ hs, measurable_set_compl m s hs)
(assume f _ hf, measurable_set_Union m f hf)

I have

lemma generate_from_le' {s : set (set Ω)} {m : measurable_space Ω}
(h :  t  s, m.measurable_set' t) : generate_from s  m :=
begin
intros r hr,
cases hr with ha hb t ht he hf ,
{    exact h r hb,  },
{ apply measurable_set_empty, },
{
apply measurable_set_compl _ _ _,
sorry,
},
{
sorry,
}
end

#### Johan Commelin (Mar 10 2021 at 04:08):

@Iocta you can just fill in the remaining arguments, right?

#### Johan Commelin (Mar 10 2021 at 04:08):

Or otherwise, use assumption, if you want lean to figure them out for you

#### Iocta (Mar 10 2021 at 04:15):

Replacing sorry with assumption doesn't satisfy lean, maybe I don't understand what you mean.

#### Johan Commelin (Mar 10 2021 at 04:20):

What does your goal look like?

#### Johan Commelin (Mar 10 2021 at 04:21):

If you give me something that I can copy-paste into an empty lean file, I can take a look [see #mwe]

#### Iocta (Mar 10 2021 at 04:23):

import measure_theory.measure_space
import measure_theory.measurable_space

open measure_theory measure_theory.measure_space classical set

noncomputable theory

variable Ω   : Type
variable [measurable_space Ω]

open measurable_space

lemma generate_from_le' {s : set (set Ω)} {m : measurable_space Ω}
(h :  t  s, m.measurable_set' t) : generate_from s  m :=
begin
intros r hr,
cases hr with ha hb t ht he hf ,
{    exact h r hb,  },
{ apply measurable_set_empty, },
{
apply measurable_set_compl _ _ _,
sorry,
},
{
sorry,
},
end

#### Johan Commelin (Mar 10 2021 at 04:34):

@Iocta the problem was that cases is too crude of a tactic for this job. induction works better:

lemma generate_from_le' {s : set (set Ω)} {m : measurable_space Ω}
(h :  t  s, m.measurable_set' t) : generate_from s  m :=
begin
intros t ht,
induction ht with u hu x hx y hy z hz,
{ exact h u hu, },
{ apply measurable_set_empty, },
{ apply measurable_set_compl _ _ _,
assumption, },
{ apply measurable_set_Union,
assumption, },
end

I see, thanks

#### Iocta (Mar 10 2021 at 20:24):

In measurable_space.lean we have

variable [measurable_space α] -- at top level
m : measurable_space α -- in a lemma

what is the difference between these two uses of measurable_space?

#### Kevin Buzzard (Mar 11 2021 at 07:42):

You'd use concrete instances when you are reasoning about the collection of all measurable space structures on a type, and type class inference if you just want to fix one measurable space structure once and for all and then do some measure theory.

#### Iocta (Mar 11 2021 at 08:01):

What does it mean that they're both used on the same variable α in that file?

#### Mario Carneiro (Mar 11 2021 at 08:22):

I don't think they are both in scope at the same time

#### Mario Carneiro (Mar 11 2021 at 08:23):

the [measurable_space A] is in a section that ends before the lemma you see

Last updated: May 06 2021 at 22:13 UTC