Zulip Chat Archive

Stream: new members

Topic: type mismatch error


view this post on Zulip Iocta (Aug 20 2020 at 19:57):

  1. I can see what it's saying in the first error but I don't know how to fix it.
  2. I don't understand the second error
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
import measure_theory.probability_mass_function
import set_theory.cardinal_ordinal


universe u
variables α β : Type u



noncomputable def marginalize1 (f : pmf (α × β)) : pmf β:=
(λb, ∑' a : α, f (a, b))

-- type mismatch, term
--   λ (b : β), ∑' (a : α), ⇑f (a, b)
-- has type
--   β → nnreal
-- but is expected to have type
--   pmf β


noncomputable def marginalize2 (f : pmf (α × β)) : pmf α :=
(λa, ∑' b : β, f (a, b))


def independent (f : pmf (α × β)) : Prop :=
 a: α,  b : β, f (a, b) = (marginalize1 f b) * (marginalize2 f a)

-- type mismatch at application
--   marginalize1 f
-- term
--   f
-- has type
--   pmf (α × β) : Type u
-- but is expected to have type
--   Type ? : Type (?+1)

view this post on Zulip Alex J. Best (Aug 20 2020 at 20:02):

The type pmf α is { f : α → nnreal // has_sum f 1 } , so to construct a term you need a pair α → nnreal and a proof that the sum is 1, you can write this as a pair with langle rangle.

view this post on Zulip Iocta (Aug 20 2020 at 20:04):

Ok that makes sense

view this post on Zulip Iocta (Aug 20 2020 at 20:17):

Does that also explain the second error (how)?

view this post on Zulip Iocta (Aug 20 2020 at 20:19):

ie

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
import measure_theory.probability_mass_function
import set_theory.cardinal_ordinal


universe u
variables α β : Type u



noncomputable def marginalize1 (f : pmf (α × β)) : pmf β:=

   (λb, ∑' a : α, f (a, b)),
   begin
    unfold pmf at f,
    cases f,
    sorry,
   end


#check nhds


noncomputable def marginalize2 (f : pmf (α × β)) : pmf α :=
 (λa, ∑' b : β, f (a, b)), sorry 


def independent (f : pmf (α × β)) : Prop :=
 a: α,  b : β, f (a, b) = (marginalize1 f b) * (marginalize2 f a)


-- type mismatch at application
--   marginalize1 f
-- term
--   f
-- has type
--   pmf (α × β) : Type u
-- but is expected to have type
--   Type ? : Type (?+1)

view this post on Zulip Alex J. Best (Aug 20 2020 at 20:19):

Did you get the first ones working? I'm not running lean right now so I can't check unfortunately, you might have to add f.val in some places too.

view this post on Zulip Alex J. Best (Aug 20 2020 at 20:31):

Oh this is because marginalize1 takes alpha and beta as explicit arguments (try #check marginalize1 to see them).

view this post on Zulip Alex J. Best (Aug 20 2020 at 20:31):

So you can change your variables line to variables {α β : Type u} to make them implicit.

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

easy fix :-)


Last updated: May 14 2021 at 21:11 UTC