letter

Stream: new members

[Kevin Buzzard]

@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]

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]

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]

suggest or library_search might help here

[Iocta]

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]

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]

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

[Chris Wong]

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]

And these are arbitrary possibly infinite unions

[Scott Morrison]

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]

Then do a case bash

[Scott Morrison]

(possibly with fin_cases)

[Iocta]

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]

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]

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

[Iocta]

heh yeah that's what I meant

[Iocta]

[edited it to avoid confusion]

[Chris Wong]

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

[Iocta]

oh that sounds true

[Iocta]

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]

set X is implemented as X \r Prop

[Iocta]

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]

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

[Kenny Lau]

so hr is really saying r \in s

[Kenny Lau]

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

[Kenny Lau]

σ := (λx, x ∈ s)

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Iocta]

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

[Kenny Lau]

not just for a specific a and b

[Iocta]

yeah exactly

[Kenny Lau]

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

[Iocta]

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

[Kenny Lau]

you're bracketing wrong

[Iocta]

okay I'll start over

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Iocta]

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]

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

[Chris Wong]

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

[Chris Wong]

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]

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]

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]

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

[Kevin Buzzard]

import tactic

variable (α : Type)

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

[Kenny Lau]

because it isn't a 0th order logic goal

[Iocta]

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]

h.univ_mem

[Kenny Lau]

again I think that isn't what you meant

[Kenny Lau]

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

[Kenny Lau]

the underlying set of h is h.\sigma

[Iocta]

Like this I guess

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

[Kenny Lau]

yes that's right

[Iocta]

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]

Oh maybe this

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

[Iocta]

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]

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]

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

[Iocta]

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

[Kenny Lau]

@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]

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]

Yes, thank you.

[Iocta]

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]

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

[Mario Carneiro]

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]

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]

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]

Those haves are a little awkward, can I avoid?

[Ruben Van de Velde]

    {
      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]

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

[Kyle Miller]

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]

That's much prettier!

[Ruben Van de Velde]

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]

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]

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

[Iocta]

Cool, thanks :-)

[Iocta]

just learned about rw at \entails too

[Kyle Miller]

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.