Zulip Chat Archive

Stream: new members

Topic: measurable_space


view this post on Zulip Iocta (Aug 13 2020 at 21:40):

What is going on here?

import analysis.normed_space.indicator_function
import measure_theory.set_integral
import analysis.specific_limits
import data.real.basic
import data.nat.basic
import algebra.geom_sum


open set filter topological_space measure_theory

section e2_7_1


@[derive decidable_eq]
inductive letter : Type
| a : letter
| b : letter
| c : letter
| d : letter

namespace letter



instance fintype: fintype letter :=
{elems := {a, b, c, d}, complete := λ x, by cases x; simp}


def f1 : set (set letter) := {{}, {a, b}, {c, d}, {a,b,c,d}}


-- from mathlib:
-- /-- A measurable space is a space equipped with a σ-algebra. -/
-- structure measurable_space (α : Type u) :=
-- (is_measurable : set α → Prop)
-- (is_measurable_empty : is_measurable ∅)
-- (is_measurable_compl : ∀s, is_measurable s → is_measurable sᶜ)
-- (is_measurable_Union : ∀f:ℕ → set α, (∀i, is_measurable (f i)) → is_measurable (⋃i, f i))



example : measurable_space f1 :=
begin
    split,
    {  exact rfl, },
    {
        intros s h,
-- s: set ↥f1
-- h: ∅ = s
-- ⊢ ∅ = sᶜ
    },
    { sorry },
    { sorry }
end

end letter


end e2_7_1

view this post on Zulip Iocta (Aug 13 2020 at 21:43):

Is it asking me to show that the complement of {} in {{}, {a, b}, {c, d}, {a,b,c,d}} is {}? I don't think that's true.

view this post on Zulip Reid Barton (Aug 13 2020 at 21:43):

You have gone wrong starting with measurable_space f1

view this post on Zulip Iocta (Aug 13 2020 at 21:44):

Oh. What do I mean?

view this post on Zulip Reid Barton (Aug 13 2020 at 21:45):

Also, I would recommend using fsplit rather than split--that will present the subgoals in the order you expect

view this post on Zulip Reid Barton (Aug 13 2020 at 21:47):

Try using fsplit instead of split, and then pay close attention to what Lean is asking for

view this post on Zulip Reid Barton (Aug 13 2020 at 21:47):

And look at the definition of measurable_space again.

view this post on Zulip Iocta (Aug 13 2020 at 21:54):

well I can finish the proof but as you said, I'm pretty sure this is not what I meant :-D

example : measurable_space f1 :=
begin
    fsplit,
    {
        exact (λs, true),
    },
    {
        exact trivial,
    },
    {
        intros a b,
        trivial,
        },
    {
        intros a b,
        trivial,
     },
end

view this post on Zulip Iocta (Aug 13 2020 at 23:25):

So maybe what I mean is example : measurable_space letter :=, but then the first step is ⊢ set letter -> Prop, and I can start by saying

intro s, have s_finite: finite s, exact finite.of_fintype s,

which leaves ⊢ Prop and I'd say something involving finset.is_measurable....?

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 23:25):

If you have ⊢ Prop you're doing something very wrong, although you could solve it using Fermat's Last Theorem

view this post on Zulip Iocta (Aug 13 2020 at 23:26):

haha okay

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 23:26):

Did you look at the type of measurable_space yet? I have never used it but my impression is that if it's data then you shouldn't be anywhere near a begin/end block

view this post on Zulip Iocta (Aug 13 2020 at 23:26):

yeah I quoted it in the first paste

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 23:26):

You make structures in Lean with the { foo := bar, baz := moo } constructor usually

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 23:27):

Oh Ok great thanks: then you should write example : measurable_space f1 := _ and then click on the light bulb and then click on the last but one option about fields of a structure and then go ahead and fill those in

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 23:28):

this is assuming you want to put a measurable space structure on f1

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 23:28):

which to be frank looks highly unlikely

view this post on Zulip Iocta (Aug 13 2020 at 23:32):

I think what I'm trying to say is f1 has {}, is closed under complement, and countable union/intersection

view this post on Zulip Iocta (Aug 13 2020 at 23:33):

which is at least similar to the generated

example : measurable_space XXXX := {
  is_measurable := _,
  is_measurable_empty := _,
  is_measurable_compl := _,
  is_measurable_Union := _ }

for some XXXX

view this post on Zulip Iocta (Aug 13 2020 at 23:35):

but you both say I don't mean measurable_space f1, so I'm not sure what I do mean

view this post on Zulip Iocta (Aug 13 2020 at 23:38):

maybe i mean

example : measurable_space letter := {
  is_measurable := (λ s, s  f1),
  is_measurable_empty := _,
  is_measurable_compl := _,
  is_measurable_Union := _ }

i'll try that

view this post on Zulip Iocta (Aug 14 2020 at 00:28):

⊢ ∅ ∈ f1 woulda thought rfl would work, but no dice

view this post on Zulip Iocta (Aug 14 2020 at 00:40):

Since def f1 : set (set letter) := {{}, {a, b}, {c, d}, {a,b,c,d}}, shouldn't it follow immediately that {} \in f1?

view this post on Zulip Alex J. Best (Aug 14 2020 at 00:41):

Well just because its obvious to you do doesn't mean its trivial!

view this post on Zulip Alex J. Best (Aug 14 2020 at 00:42):

The notation {{}, {a,b}, {c,d}, {a,b,c,d}} means something. Try adding set_option pp.notation false above your example to turn notation off, and you'll see it is really a sequence of elements inserted into a singleton set.

view this post on Zulip Alex J. Best (Aug 14 2020 at 00:43):

So probably there is a sequence of lemmas that do it, or maybe a tactic like finish.

view this post on Zulip Alex J. Best (Aug 14 2020 at 00:47):

First thing is to rw f1 though if you didn't already.

view this post on Zulip Alex J. Best (Aug 14 2020 at 00:48):

In this case it is in fact a single lemma after you've done that

view this post on Zulip Iocta (Aug 14 2020 at 00:52):

Ok that works.


Last updated: May 10 2021 at 00:31 UTC