## Stream: new members

### Topic: type mismatch error

#### 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)


#### 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.

#### Iocta (Aug 20 2020 at 20:04):

Ok that makes sense

#### Iocta (Aug 20 2020 at 20:17):

Does that also explain the second error (how)?

#### 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)


#### 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.

#### 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).

#### Alex J. Best (Aug 20 2020 at 20:31):

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

#### Iocta (Aug 20 2020 at 20:32):

easy fix :-)

Last updated: May 14 2021 at 21:11 UTC