Zulip Chat Archive

Stream: new members

Topic: letter


Kevin Buzzard (Aug 14 2020 at 08:39):

@Iocta rfl doesn't mean "it's obvious", it means "equality is reflexive" ie it proves X=X. Your goal is something like true or P or Q or R

Iocta (Aug 14 2020 at 08:48):

Got most of the way through it. How to fill the sorry?

    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}

    @[simp]
    lemma univ_letter : @finset.univ letter letter.fintype = {a, b, c, d} := rfl






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

    example : measurable_space letter := {
    is_measurable := (λ s, s  f1),
    is_measurable_empty := by {
        rw f1,
        rw mem_insert_iff,
        left,
        simp only [eq_self_iff_true],
    },
    is_measurable_compl := by {
        intros s h,
        cases h,
        {
            rw f1,
            simp,
            right,
            right,
            right,
            simp *,
            ext1,
            split,
            {
                intro h,
                unfold univ at *,
                simp * at *,
                cases h,
                cases x; finish,
            },
            intro h,
            finish,
        },
        {
            rw f1,
            simp * at *,
            cases h,
            {
              right,
              right,
              left,
              simp * at *,
                ext1,
                split,
                {
                    intro h',
                    simp * at *,
                    cases x; finish,
                },
                {
                    intro h',
                    cases x; finish,
                },
            },
            cases h,
            {
                right,
                left,
                ext1,
                split,
                { intro h', simp * at h', cases x; finish,   },
                { intro h',
                    cases x; finish,
                },
            },
            {
                left,
                ext1,
                split,
                {
                    intro h',
                    cases x; finish,
                },
                {
                    intro h',
                    cases x; finish,
                }
            },

        },
    },
    is_measurable_Union := by {
        intros s h,
        simp * at *,
        rw f1 at *,
        /-
s : ℕ → set letter,
h : ∀ (i : ℕ), s i ∈ {∅, {a, b}, {c, d}, {a, b, c, d}}
⊢ Union s ∈ {∅, {a, b}, {c, d}, {a, b, c, d}}
-/

        sorry,


    }

    }

    end letter


    end e2_7_1

Iocta (Aug 14 2020 at 08:53):

I'm never sure when I need to be thinking about how to do the math vs knowing about tactics/lemmas in mathlib. I guess this will come with experience.

Chris Wong (Aug 14 2020 at 08:55):

suggest or library_search might help here

Iocta (Aug 14 2020 at 08:57):

Those don't give me anything; for some reason my computer seems to be struggling with this example, maybe they timed out sooner than they shouldve

Scott Morrison (Aug 14 2020 at 09:12):

What would your maths argument be? Maybe write it out here in gory detail. A possible hint would be to look at the fin_cases tactic, but you'll need to do some preparatory work before it's useful.

Kevin Buzzard (Aug 14 2020 at 09:38):

Yeah I echo Scott's comment. You might think this is "obvious" -- but what is the actual proof?

Chris Wong (Aug 14 2020 at 09:40):

Ooh, I see. So I guess we have to iterate over every possible union, and check that it's valid? That would explain why it isn't just a library_search away.

Kevin Buzzard (Aug 14 2020 at 09:59):

And these are arbitrary possibly infinite unions

Scott Morrison (Aug 14 2020 at 10:18):

Since each s i lives in some finite set, you might make an argument about the image of s (which is some set of sets of letters).

Scott Morrison (Aug 14 2020 at 10:18):

Then do a case bash

Scott Morrison (Aug 14 2020 at 10:18):

(possibly with fin_cases)

Iocta (Aug 15 2020 at 02:47):

I think this is in the direction described, but dunno how to fill it.

 example :  (f :   set letter), ( (i : ), f i  f1)  ( (i : ), f i)  f1 :=
 begin
    intros f h,
    rw f1 at *,
    let im_f : (set (set letter)) := {q : set letter |  i : , q = f i},
    let sets : set (set letter) :=  {, {a, b}, {c, d}, {a, b, c, d}},
    have imf2sets:  (s: set letter), s  im_f  s  sets,
    {
        intros s hs,
        simp at hs,
        cases hs with i hi,
        specialize h i,
        rw hi,
        exact h,
    },
    suffices: ( (i : ), f i)  sets, { exact this, },
    have uclosed_imf: ( (i : ), f i)  im_f,
    {
        sorry,

    },
    exact imf2sets ( (i : ), f i) uclosed_imf,

Iocta (Aug 15 2020 at 05:47):

structure alg (Ω : Type u) :=
(σ : set (set Ω))
(univ_mem : set.univ  σ)
(closed_complements :  s  σ, s  σ)
(closed_finite_unions :   f :   set Ω,  n : , ( i : , (f i)  σ)  ( i  n, f i)  σ)

this restricts the last line of measurable_space to only finite unions. Is that the right expression for closed finite unions?

Chris Wong (Aug 15 2020 at 05:56):

Your closed_countable_unions seems to be about finite unions, not countable ones?

Iocta (Aug 15 2020 at 05:56):

heh yeah that's what I meant

Iocta (Aug 15 2020 at 05:58):

[edited it to avoid confusion]

Chris Wong (Aug 15 2020 at 06:00):

If you only care about finite unions, then I think the statement can be simplified to union (small u) of two sets

Iocta (Aug 15 2020 at 06:04):

oh that sounds true

Iocta (Aug 15 2020 at 08:11):

How to interpret the definition of hr?

universe u

variable {α : Type u}

structure algebra' (Ω : Type u) :=
(σ : set (set Ω))
(univ_mem : set.univ  σ)
(closed_complements :  s  σ, s  σ)
(closed_finite_unions (a b  σ ): a  b  σ)

example (s : set (set α )) (a b: set α) (ha: a  s) (hb : b  s) (h: a  b  s) : algebra' α := {
  σ := (λx, x  s),
  univ_mem := by {
    sorry,
  },
  closed_complements := by {
    intros r hr,
-- α: Type u
-- s: set (set α)
-- ab: set α
-- ha: a ∈ s
-- hb: b ∈ s
-- h: a ∩ bᶜ ∈ s
-- r: set α
-- hr: r ∈ λ (x : set α), x ∈ s
-- ⊢ rᶜ ∈ λ (x : set α), x ∈ s

  },
  closed_finite_unions := _ }

Kenny Lau (Aug 15 2020 at 08:12):

set X is implemented as X \r Prop

Iocta (Aug 15 2020 at 08:12):

is that "proof that r is in the set of functions from sets x of alpha to proof that x is in s"?

Kenny Lau (Aug 15 2020 at 08:12):

so \lambda x : x \in s is really { x | x \in s }

Kenny Lau (Aug 15 2020 at 08:12):

so hr is really saying r \in s

Kenny Lau (Aug 15 2020 at 08:13):

that's what happens if you use the X \r Prop implementation to write \sigma

Kenny Lau (Aug 15 2020 at 08:13):

σ := (λx, x ∈ s)

Kenny Lau (Aug 15 2020 at 08:13):

instead of σ := { x | x ∈ s }

Kenny Lau (Aug 15 2020 at 08:14):

I don't think your hypothesis is saying what you want it to say either

Kenny Lau (Aug 15 2020 at 08:14):

you want to say that for all a b \in s we have a \cap b\^c \in s

Iocta (Aug 15 2020 at 08:14):

I have a feeling there's something wrong with the quantifiers

Kenny Lau (Aug 15 2020 at 08:14):

not just for a specific a and b

Iocta (Aug 15 2020 at 08:14):

yeah exactly

Kenny Lau (Aug 15 2020 at 08:15):

and instead of σ := { x | x ∈ s } you should just write σ := s

Iocta (Aug 15 2020 at 08:15):

but I thought I could always put hypotheses on the left of the : instead of \foralling them

Kenny Lau (Aug 15 2020 at 08:15):

you're bracketing wrong

Iocta (Aug 15 2020 at 08:15):

okay I'll start over

Kenny Lau (Aug 15 2020 at 08:16):

\forall a, a = a is the same as (a) : a = a

Kenny Lau (Aug 15 2020 at 08:16):

but (\forall a, a = a) \to b is not the same as (a) (h : a = a) : b

Kenny Lau (Aug 15 2020 at 08:16):

that's what it means that forall can be replaced with colon

Iocta (Aug 15 2020 at 09:48):

This seems to work. I have some questions about improvements. Can I use closed_complements in closed_finite_unions? Currently I'm proving the same thing twice. Or can I pull it into an internal lemma to be used in both places?

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
import tactic.fin_cases
import data.set.basic


open set filter topological_space measure_theory

universe u

variable {α : Type u}

structure algebra' (Ω : Type u) :=
(σ : set (set Ω))
(univ_mem : set.univ  σ)
(closed_complements :  s  σ, s  σ)
(closed_finite_unions (a b  σ ): a  b  σ)


@[simp]
lemma compl_iff {x y : set α } : x = y   x = y  :=
begin
    split,
    {
        intro h,
        finish,
    },
    {
        intro h,
        ext1,
        split; { intro h', finish },
    }
end

lemma compl_inter_compl_eq_union (x y : set α ): (x  y) = x  y :=
begin
 have: (x  y) = (x  y), {     simp only [compl_union], },
 rw  @compl_iff α (x  y) (x  y) ,
 exact this,
end





example  (s: set (set α )) (hs: set.univ  s) (h:  a b  s, a  b  s) : algebra' α := {
  σ := s,
  univ_mem := hs,
  closed_complements := by {
      intros z hz,
      specialize h set.univ z hs hz,
      rw univ_inter at h,
      exact h,
  },
  closed_finite_unions := by {
    have cc:  x  s, x  s, {
        intros z hz,
        specialize h set.univ z hs hz,
        rw univ_inter at h,
        exact h,
    },
    intros x y hx hy,
    have hxc: x  s, { apply cc x hx,  },
    have hyc: y  s, { apply cc y hy},
    have: x  y  s, { specialize h x y hxc hy , exact h},
    have hc: (x  y)  s, { apply cc (x  y )  this},
    have : (x  y) = x  y, { apply compl_inter_compl_eq_union  },
    simp * at *,
  }
}

Iocta (Aug 15 2020 at 10:00):

Also, there's gotta be an easier way to do those De Morgan-like lemmas, right?

Chris Wong (Aug 15 2020 at 12:08):

lemma compl_inter_compl (x y : set α) : (x  y) = x  y :=
by simp only [compl_inter, compl_compl]

Chris Wong (Aug 15 2020 at 13:14):

example (s : set (set α)) (hs : set.univ  s) (h :  a b  s, a  b  s) : algebra' α :=
have closed_complements :  z  s, z  s :=
begin
  intros z hz,
  specialize h set.univ z hs hz,
  rw univ_inter z at h,
  exact h,
end,
{ σ := s,
  univ_mem := hs,
  closed_complements := closed_complements,
  closed_finite_unions :=
  begin
    intros a b ha hb,
    have hab : a  b  s := h _ _ (closed_complements _ ha) hb,
    rw  compl_union at hab,
    rw  compl_compl (a  b),
    apply closed_complements,
    exact hab,
  end }

Chris Wong (Aug 15 2020 at 13:35):

I'm using have to share the closed_complements proof – I haven't worked with structures much yet so I don't know if there's a better way

Kenny Lau (Aug 15 2020 at 17:16):

Iocta said:

Also, there's gotta be an easier way to do those De Morgan-like lemmas, right?

the canonical way to solve any 0th order logic (i.e. propositional logic) goal is finish

Iocta (Aug 15 2020 at 18:11):

Why doesn't lemma compl_inter_compl_eq_union' (x y : set α ): (xᶜ ∩ yᶜ)ᶜ = x ∪ y := by finish work?

Kevin Buzzard (Aug 15 2020 at 18:15):

import tactic

variable (α : Type)

example (x y : set α ): (x  y) = x  y :=
begin
  ext,
  finish
end

Kenny Lau (Aug 15 2020 at 18:25):

because it isn't a 0th order logic goal

Iocta (Aug 15 2020 at 21:53):

universe u

variable {α : Type u}
variables (s: set (set α)) (hs: set.univ  s)


structure algebra' (Ω : Type u) :=
(σ : set (set Ω))
(univ_mem : set.univ  σ)
(closed_complements :  s  σ, s  σ)
(closed_finite_unions (a b  σ ): a  b  σ)


example (h : algebra' α) : set.univ  s :=
begin
    sorry,
end

How do I use the univ_mem from the structure definition?

Kenny Lau (Aug 15 2020 at 21:56):

h.univ_mem

Kenny Lau (Aug 15 2020 at 21:56):

again I think that isn't what you meant

Kenny Lau (Aug 15 2020 at 21:57):

h is some algebra structure on \alpha that has nothing to do with s

Kenny Lau (Aug 15 2020 at 21:57):

the underlying set of h is h.\sigma

Iocta (Aug 15 2020 at 22:08):

Like this I guess

example (a : algebra' α) : set.univ  a.σ := a.univ_mem

Kenny Lau (Aug 15 2020 at 22:12):

yes that's right

Iocta (Aug 15 2020 at 22:25):

I don't totally get it. What do I mean here?

structure semialgebra (Ω : Type u) :=
(σ : set (set Ω))
(univ_mem : set.univ  σ)
(empty_mem : {}  σ )
(semi_closed_complements :  s  σ,   f :   set Ω,  n : , ( i : , (f i)  σ)  ( i  n, f i) = s)

example (a: algebra' α) : semialgebra a.σ := {
  σ := _,
  univ_mem := _,
  empty_mem := _,
  semi_closed_complements := _ }

Iocta (Aug 15 2020 at 22:34):

Oh maybe this

example (a: algebra' α) : semialgebra α := {
  σ := a.σ,
  univ_mem := a.univ_mem,
  empty_mem := _,
  semi_closed_complements := _ }

Iocta (Aug 16 2020 at 05:29):

How can I use algebra'.univ_mem to fill this?

example (all_algebras: n : , algebra' (ss n)  ) : algebra' α  :=
{
  σ := Union ss,
  univ_mem := by {
    simp only [mem_Union],
    specialize all_algebras 0,
    let ss0 := (ss 0),
    have: univ  ss0,
    {
-- α: Type u
-- ss: ℕ → set (set α)
-- all_algebras: algebra' ↥(ss 0)
-- ss0: set (set α) := ss 0
-- ⊢ univ ∈ ss0
    }


  },
  closed_complements := _,
  closed_finite_unions := _
}

Iocta (Aug 16 2020 at 05:45):

there's a sequence of set (set alpha), each of which contains univ. So I should be able to pick the first one, show it has univ, and then unioning it with the others should still have univ.

Iocta (Aug 16 2020 at 05:45):

but I'm stuck at showing the first one has univ

Iocta (Aug 16 2020 at 05:49):

I figured it'd be algebra'.univ_mem or something like that but no dice

Kenny Lau (Aug 16 2020 at 10:02):

@Iocta algebra' (ss n) means an algebra structure on ss n (coerced to a type), not an algebra structure on \alpha whose underlying set is ss n

Kenny Lau (Aug 16 2020 at 10:06):

this should be what you mean:

import data.set.lattice

universe u

variable {α : Type u}

structure algebra' (Ω : Type u) :=
(σ : set (set Ω))
(univ_mem : set.univ  σ)
(closed_complements :  s  σ, s  σ)
(closed_finite_unions (a b  σ ): a  b  σ)

variables (ss :   algebra' α) (ss_increasing:  n : , (ss n).σ  (ss (n + 1)).σ)

example : algebra' α :=
{ σ :=  n, (ss n).σ,
  univ_mem := set.mem_Union.2 0, (ss 0).univ_mem,
  closed_complements := _,
  closed_finite_unions := _ }

Iocta (Aug 17 2020 at 00:23):

Yes, thank you.

Iocta (Aug 18 2020 at 06:59):

I guess it's complaining that a <= might not be decidable? What is the normal way to handle this?

universe u

variable {α : Type u}


structure algebra' (Ω : Type u) :=
(σ : set (set Ω))
(univ_mem : set.univ  σ)
(closed_complements :  s  σ, s  σ)
(closed_finite_unions (a b  σ ): a  b  σ)

variables (ss :   algebra' α) (ss_subset_of_ss_succ:  n : , (ss n).σ  (ss (n + 1)).σ)

include ss_subset_of_ss_succ

lemma ss_increasing (n m : ) (h: n  m) : (ss n).σ  (ss m).σ :=
begin
    intros s hs,
    induction h ,
    {        exact hs,    },
    {
        specialize ss_subset_of_ss_succ h_b,
        apply ss_subset_of_ss_succ,
        exact h_ih,
    },
end


example : algebra' α :=
{ σ :=  n, (ss n).σ,
  univ_mem := set.mem_Union.2 0, (ss 0).univ_mem,
  closed_complements := by {
    intros s hs,
    have exists_ssn:  n : , s  (ss n).σ,
    {
        let sn:= {n :  | s  (ss n).σ  },
        simp at hs,
        cases hs with n hn,
        use n,
        exact hn,
    },
    cases exists_ssn with n hn,
    norm_num,
    use n,
    exact (ss n).closed_complements s hn,
 },
  closed_finite_unions := by {
    intros a b ha hb,
    simp * at *,
    cases ha with na hna,
    cases hb with nb hnb,
    let nab := max na nb,
    have na_subset: (ss na).σ  (ss nab).σ, {
        apply ss_increasing,
        apply le_max_left,
-- invalid apply tactic, failed to unify
--   ∀ (n : ℕ), (ss n).σ ⊆ (ss (n + 1)).σ
-- with
--   ∀ [_inst_1 : decidable_linear_order ?m_1] (a b : ?m_1), a ≤ max a b
    },
    have nb_subset: (ss nb).σ  (ss nab).σ, {
        apply ss_increasing,
        apply le_max_right,
    },
    use nab,
    apply (ss nab).closed_finite_unions a b (na_subset hna) (nb_subset hnb),
  }
}

Mario Carneiro (Aug 18 2020 at 07:01):

the error says you applied something that looks different than what lean wants

Mario Carneiro (Aug 18 2020 at 07:02):

I don't think it's a decidability problem, it's just a completely different theorem. ss has no definition in your problem, it's just a variable

Mario Carneiro (Aug 18 2020 at 07:04):

it looks like when you did apply ss_increasing, the first subgoal you got is (ss_subset_of_ss_succ: ∀ n : ℕ, (ss n).σ ⊆ (ss (n + 1)).σ), which should be a variable in your context

Iocta (Aug 18 2020 at 07:28):

Alright this works

universe u

variable {α : Type u}


structure algebra' (Ω : Type u) :=
(σ : set (set Ω))
(univ_mem : set.univ  σ)
(closed_complements :  s  σ, s  σ)
(closed_finite_unions (a b  σ ): a  b  σ)

variables (ss :   algebra' α) (ss_subset_of_ss_succ:  n : , (ss n).σ  (ss (n + 1)).σ)

include ss_subset_of_ss_succ

lemma ss_increasing {n m : } (h: n  m) : (ss n).σ  (ss m).σ :=
begin
    intros s hs,
    induction h ,
    {        exact hs,    },
    {
        specialize ss_subset_of_ss_succ h_b,
        apply ss_subset_of_ss_succ,
        exact h_ih,
    },
end


example : algebra' α :=
{ σ :=  n, (ss n).σ,
  univ_mem := set.mem_Union.2 0, (ss 0).univ_mem,
  closed_complements := by {
    intros s hs,
    have exists_ssn:  n : , s  (ss n).σ,
    {
        let sn:= {n :  | s  (ss n).σ  },
        simp at hs,
        cases hs with n hn,
        use n,
        exact hn,
    },
    cases exists_ssn with n hn,
    norm_num,
    use n,
    exact (ss n).closed_complements s hn,
 },
  closed_finite_unions := by {
    intros a b ha hb,
    simp * at *,
    cases ha with na hna,
    cases hb with nb hnb,
    use (max na nb),
    apply (ss (max na nb)).closed_finite_unions a b,
    {
    have: (ss na).σ  (ss (max na nb)).σ,
    {
        apply ss_increasing,
        intro n,
        apply ss_subset_of_ss_succ,
        apply le_max_left,
    },
    apply this hna,
    },
    {
        have: (ss nb).σ  (ss (max na nb)).σ,
        {
            apply ss_increasing,
            intro n,
            apply ss_subset_of_ss_succ,
            apply le_max_right,
        },
        apply this hnb,
    },
  }
}

Iocta (Aug 18 2020 at 07:28):

Those haves are a little awkward, can I avoid?

Ruben Van de Velde (Aug 18 2020 at 07:37):

    {
      apply set.mem_of_mem_of_subset hna,
      apply ss_increasing,
      intro n,
      apply ss_subset_of_ss_succ,
      apply le_max_left,
    },
    {
      apply set.mem_of_mem_of_subset hnb,
      apply ss_increasing,
      intro n,
      apply ss_subset_of_ss_succ,
      apply le_max_right,
    },

Iocta (Aug 18 2020 at 07:40):

nice. Did you happen to know that one or was there a trick to figuring it out?

Kyle Miller (Aug 18 2020 at 07:40):

Looks like I did the same transformation as @Ruben Van de Velde there, but there are some other simplifications, too, elsewhere:

import data.set

universe u

variable {α : Type u}


structure algebra' (Ω : Type u) :=
(σ : set (set Ω))
(univ_mem : set.univ  σ)
(closed_complements :  s  σ, s  σ)
(closed_finite_unions (a b  σ ): a  b  σ)

variables (ss :   algebra' α) (ss_subset_of_ss_succ:  n : , (ss n).σ  (ss (n + 1)).σ)

include ss_subset_of_ss_succ

lemma ss_increasing {n m : } (h: n  m) : (ss n).σ  (ss m).σ :=
begin
    intros s hs,
    induction h ,
    { exact hs, },
    { exact ss_subset_of_ss_succ h_b h_ih, }
end


example : algebra' α :=
{ σ :=  n, (ss n).σ,
  univ_mem := set.mem_Union.2 0, (ss 0).univ_mem,
  closed_complements := by {
    intros s hs,
    rw set.mem_Union at hs,
    cases hs with n hn,
    norm_num,
    use n,
    exact (ss n).closed_complements s hn,
 },
  closed_finite_unions := by {
    intros a b ha hb,
    rw set.mem_Union at ha hb ,
    cases ha with na hna,
    cases hb with nb hnb,
    use (max na nb),
    apply (ss (max na nb)).closed_finite_unions a b,
    { apply set.mem_of_mem_of_subset hna,
      apply ss_increasing,
      intro n,
      apply ss_subset_of_ss_succ,
      apply le_max_left, },
    { apply set.mem_of_mem_of_subset hnb,
      apply ss_increasing,
      intro n,
      apply ss_subset_of_ss_succ,
      apply le_max_right, },
  }
}

Iocta (Aug 18 2020 at 07:42):

That's much prettier!

Ruben Van de Velde (Aug 18 2020 at 07:43):

I first tried apply (_ : (ss nb).σ ⊆ (ss (max na nb)).σ) hna, but that didn't look great either, so I scrolled through https://leanprover-community.github.io/mathlib_docs/data/set/basic.html and there it was :)

Kyle Miller (Aug 18 2020 at 07:43):

Iocta said:

nice. Did you happen to know that one or was there a trick to figuring it out?

Usually you're not supposed to take advantage of the way things are defined, so I looked for the lemma that takes x ∈ s and s ⊆ t to get x ∈ t figuring it must exist for that reason. I guessed it was in data.set.basic, and found it with a quick search for . You could also use library_search to find this kind of theorem. The trick then is that applying mem_of_mem_of_subset hna replaces the goal with the subset relation you want to prove.

Kyle Miller (Aug 18 2020 at 07:45):

And don't forget about squeeze_simp to figure out what your simp is doing. This is where set.mem_Union came from.

Iocta (Aug 18 2020 at 07:48):

Cool, thanks :-)

Iocta (Aug 18 2020 at 07:48):

just learned about rw at \entails too

Kyle Miller (Aug 18 2020 at 07:51):

One thing I'm confused about is that set.mem_of_mem_of_subset is marked with the @[trans] attribute, but you can't use the transitivity tactic in its place. I'm not sure how this is supposed to work.


Last updated: Dec 20 2023 at 11:08 UTC