generate_from_le

Stream: new members

[Iocta]

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]

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]

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]

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]

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

[Hanting Zhang]

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]

How can I see that?

[Hanting Zhang]

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.

[Iocta]

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

[Hanting Zhang]

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

[Hanting Zhang]

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]

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]

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

[Iocta]

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]

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]

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

[Johan Commelin]

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

[Iocta]

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

[Johan Commelin]

What does your goal look like?

[Johan Commelin]

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

[Iocta]

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

[Iocta]

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

[Johan Commelin]

@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

[Iocta]

I see, thanks

[Iocta]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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