Zulip Chat Archive

Stream: new members

Topic: generate_from_le


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Iocta (Mar 09 2021 at 20:36):

How can I see that?

view this post on Zulip 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.

view this post on Zulip Iocta (Mar 09 2021 at 20:39):

is https://github.com/leanprover-community/mathlib/blob/16ef29135dfe41fba018ef7005909c279bee45f5/src/measure_theory/measurable_space.lean#L278 relevant?

view this post on Zulip Hanting Zhang (Mar 09 2021 at 20:39):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 10 2021 at 04:08):

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

view this post on Zulip Johan Commelin (Mar 10 2021 at 04:08):

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

view this post on Zulip Iocta (Mar 10 2021 at 04:15):

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

view this post on Zulip Johan Commelin (Mar 10 2021 at 04:20):

What does your goal look like?

view this post on Zulip 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]

view this post on Zulip 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

view this post on Zulip Iocta (Mar 10 2021 at 04:23):

the term version is https://github.com/leanprover-community/mathlib/blob/16ef29135dfe41fba018ef7005909c279bee45f5/src/measure_theory/measurable_space.lean#L302

view this post on Zulip 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

view this post on Zulip Iocta (Mar 10 2021 at 05:04):

I see, thanks

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Iocta (Mar 11 2021 at 08:01):

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

view this post on Zulip Mario Carneiro (Mar 11 2021 at 08:22):

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

view this post on Zulip 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