split_ifs

Stream: new members

[Iocta]

How can I resolve this goal?

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 data.real.basic
import data.complex.exponential
import measure_theory.probability_mass_function
import set_theory.cardinal_ordinal

noncomputable theory

universe u
variables {α β : Type u}


def expectation (pr : pmf α) (f : α → real) : real :=
∑' a : α, pr a * f a



def real_of_bool (b: bool) : real := if b = true then 1 else 0


def bernoulli_expectation {p : nnreal} (h : p ≤ 1) : expectation (pmf.bernoulli p h) real_of_bool = p :=
begin
unfold expectation,
unfold pmf.bernoulli,
-- p: nnreal
-- h: p ≤ 1
-- ⊢ (∑' (a : bool), ↑(⇑(pmf.of_fintype (λ (b : bool), cond b p (1 - p)) _) a) * real_of_bool a) = ↑p
unfold tsum,
split_ifs,
-- 2 goals
-- p: nnreal
-- h: p ≤ 1
-- h_1: summable (λ (a : bool), ↑(⇑(pmf.of_fintype (λ (b : bool), cond b p (1 - p)) _) a) * real_of_bool a)
-- ⊢ classical.some h_1 = ↑p
-- p: nnreal
-- h: p ≤ 1
-- h_1: ¬summable (λ (a : bool), ↑(⇑(pmf.of_fintype (λ (b : bool), cond b p (1 - p)) _) a) * real_of_bool a)
-- ⊢ 0 = ↑p
end

[Kenny Lau]

you would benefit from my advice "stop unfolding!"

[Kenny Lau]

(it does not apply to expectation or pmf.bernoulli because there are no theorems for them)

[Iocta]

I used unfold tsum because I couldn't see what else to do :-)

[Kenny Lau]

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 data.real.basic
import data.complex.exponential
import measure_theory.probability_mass_function
import set_theory.cardinal_ordinal

noncomputable theory

universe u
variables {α β : Type u}

-- we prefer unicode
def expectation (pr : pmf α) (f : α → ℝ) : ℝ :=
∑' a : α, pr a * f a

-- use `cond`
def real_of_bool (b : bool) : ℝ :=
cond b 1 0

def bernoulli_expectation {p : nnreal} (h : p ≤ 1) :
  expectation (pmf.bernoulli p h) real_of_bool = p :=
begin
  unfold expectation pmf.bernoulli real_of_bool pmf.of_fintype, -- unfold things without API
  rw [tsum_fintype, fintype.sum_bool],
  change (p * 1 + (1 - p : nnreal) * 0 : ℝ) = p,
  rw [mul_one, mul_zero, add_zero]
end

[Kenny Lau]

@Iocta ask yourself: how can I remove the noise to reveal the essence of the next step? Then you would know that taking the tsum of a fintype should be the same as the sum over the fintype

[Iocta]

What made you think to go straight to the fintype api?

[Iocta]

(instead of sum-related stuff, or bool stuff, or pmf stuff or measure stuff)

[Kenny Lau]

I don't really know how to answer that question

[Kenny Lau]

perhaps @Johan Commelin could help

[Johan Commelin]

Let me read the question (-;

[Kenny Lau]

I mean, "my intuition told me so" is neither helpful nor valid: intuition just means something you can't explain

[Kenny Lau]

@Johan Commelin what's the first thing that comes to mind when you see the goal (∑' (a : bool), ↑(⇑⟨λ (b : bool), cond b p (1 - p), _⟩ a) * cond a 1 0) = ↑p?

[Kenny Lau]

p : nnreal,
h : p ≤ 1
⊢ (∑' (a : bool), ↑(⇑⟨λ (b : bool), cond b p (1 - p), _⟩ a) * cond a 1 0) = ↑p

[Johan Commelin]

That tsum is aweful

[Kenny Lau]

see we have the same intuition

[Johan Commelin]

But yes, turning that into a finset.sum is a great start

[Kenny Lau]

but how can you explain it?

[Kenny Lau]

it's like Magnus Carlsen explaining his move because it "felt intuitive"

[Kenny Lau]

sure, it works for him, but it doesn't explain anything

[Johan Commelin]

Well, it's an infinite sum, which means you have to care about convergence etc...

[Johan Commelin]

So if you sum over a finite type, then certainly you don't want to care about that

[Kenny Lau]

the way it works for me, I see the infinite sum, I think to myself, oh that's "just" a finite sum

[Kenny Lau]

so why not rewrite it as a finite sum

[Kenny Lau]

my intuition tells me that tsum is something I know nothing about and sum is something I know more about

[Kenny Lau]

so it's I guess the same mentality as "unfolding definitions"

[Kenny Lau]

but not using unfold

[Kenny Lau]

because mathematical definition is not the same as Lean definition

[Kenny Lau]

in Lean one object has one definition (Kevin would call this implementation)

[Kenny Lau]

in math one object can have 37 definitions

[Kenny Lau]

using the appropriate API to me feels like choosing the right definition to unfold

[Kenny Lau]

@Iocta I hope this is more helpful than "well my intuition told me so"

[Iocta]

Yes, it is. Similar to replacing ite with cond

[Kenny Lau]

oh that one

[Kenny Lau]

if is for Prop

[Kenny Lau]

no need to convert it to Prop if there is a version for bool

[Iocta]

switching to a less powerful tool without losing info

[Kenny Lau]

it isn't less powerful

[Iocta]

well, possibly-infinite -> finite, arbitrary prop -> bool

[Kenny Lau]

fair enough

[Iocta]

What is this error about?

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 data.real.basic
import data.complex.exponential
import measure_theory.probability_mass_function
import set_theory.cardinal_ordinal

noncomputable theory

universe u
variables {α β : Type u}


def expectation (pr : pmf α) (f : α → ℝ) : ℝ :=
∑' a : α, pr a * f a


def binomial_pmf {p: nnreal} (h: p ≤ 1) (n : ℕ) : pmf ℕ :=
⟨ λ k, (nat.choose n k) * p ^ k * (1 - p) ^ (n - k) , sorry ⟩


lemma mul_choose (n k : ℕ) : k * (n.choose k) = n * ((n - 1).choose (k - 1)) := sorry

theorem binomial_expectation {p : nnreal} (h: p ≤ 1) (n : ℕ) :
expectation (binomial_pmf h n) coe = n * p :=
begin
unfold expectation binomial_pmf pmf.of_fintype,
suffices : (∑'(k : ℕ), ↑(n.choose k) * p ^ k * (1 - p) ^ (n - k) * k) = ↑n * p,
{
--p: nnreal
--h: p ≤ 1
--n: ℕ
--this: (∑' (k : ℕ), ↑(n.choose k) * p ^ k * (1 - p) ^ (n - k) * ↑k) = ↑n * p
--⊢ (∑' (a : ℕ), ↑(⇑⟨λ (k : ℕ), ↑(n.choose k) * p ^ k * (1 - p) ^ (n - k), _⟩ a) * ↑a) = ↑n * ↑p
    sorry,
},
calc (∑'(k : ℕ), ↑(n.choose k) * p ^ k * (1 - p) ^ (n - k) * k) = ∑' k ∈ (finset.range n), (n.choose k) * p ^ k * (1 - p) ^ (n - k) * k: sorry
... = ∑' k ∈ (finset.range n), k * (n.choose k) * p ^ k * (1 - p) ^ (n - k) : sorry
... = ∑' k ∈ (finset.range n), n * ((n - 1).choose (k - 1)) * p ^ k * (1 - p) ^ (n - k) : sorry
... = n * (∑' k ∈ (finset.range n), ((n - 1).choose (k - 1)) * p ^ k * (1 - p) ^ (n - k)) : sorry
... = n * p * (∑' k ∈ (finset.range n) \ {0}, ((n - 1).choose (k - 1)) * p ^ (k -1) * (1 - p) ^ (n - k)) : sorry
... = n * p * (∑' j ∈ (finset.range (n - 1)), ((n - 1).choose j) * p ^ j * (1 - p) ^ (n - 1 - j)) : sorry
-- type mismatch at application
--   ∑' (H : j ∈ finset.range (n - 1)), ↑((n - 1).choose j) * p ^ j * (1 - p) ^ (n - 1 - j)
-- term
--   λ (H : j ∈ finset.range (n - 1)), ↑((n - 1).choose j) * p ^ j * (1 - p) ^ (n - 1 - j)
-- has type
--   j ∈ finset.range (n - 1) → nnreal : Type
-- but is expected to have type
--   ?m_1 → nnreal : Type ?
-- state:
... = n * p : sorry
end

[Iocta]

Also, how do I fill that first sorry (the suffices one)?

[Iocta]

... of course maybe my suffices statement is wrong :-)

[Kevin Buzzard]

I don't know much about probability, but your mul_choose is definitely wrong -- if ever you use natural subtraction you can be pretty sure that something is wrong, because natural subtraction is a pathological function.

[Iocta]

@Kevin Buzzard Do you think I should try to reformulate binomial_pmf to not mention n - k?

[Kevin Buzzard]

n-k is fine if you know k<=n. But you don't know this in mul_choose

[Kevin Buzzard]

I mean, you don't know k>=1 so you'll be in trouble with k-1 if k=0

[Iocta]

So do I want to just add an (h: k >= 1) or try to build the >=1 into the terms some other way?

[Iocta]

lemma mul_choose (w b: ℕ) (h: w + b ≥ 1): w * ((w + b).choose w) = (w + b) * (((w + b - 1).choose (w - 1)) := sorry

getting rid of n doesn't seem to help

[Iocta]

(still need the hypothesis)

[Iocta]

lemma mul_choose (w_minus_1 b: ℕ): (w_minus_1 + 1) * ((w_minus_1 + 1 + b).choose (w_minus_1 + 1)) = (w_minus_1 + b) * (((w_minus_1 + b ).choose w_minus_1) := sorry

¯\_(ツ)_/¯

[Kevin Buzzard]

All I'm saying was that your lemma as it stood was false because k=0 gave counterexamples. What you should do instead is entirely up to you but for sure you can't use a false lemma.

[Kevin Buzzard]

And the reason I took one look at it and suspected it might be false was that it used unsafe natural subtraction, subtracting one from things which hadn't been assumed to be >= 1.

[Iocta]

Sure that makes sense

[Kevin Buzzard]

I think your error is because you're just not using the ∑' syntax correctly. I've never used ∑' before but you seem to have ∑' (k : nat) and ∑' k \in (some finset) which doesn't bode well. What is the syntax of ∑'?

[Iocta]

I've used it above in the expectation definition ∑' a : α, pr a * f a and I agree that's different from here with the \in.

[Iocta]

So what I mean is (∑ j in (finset.range (n - 1)), _

[Iocta]

or so I thought from here

* `∑ x in s, f x` is notation for `finset.sum s f` (assuming `β` is an `add_comm_monoid`)

but

variable (k: nat)
#eval (∑ k in ((finset.range 5) \ {0}), k)

doesn't even parse

[Dan Stanescu]

This works for me and the result is 10:

#eval (∑ k in ((finset.range 5) \ {0}), k) -- 10

[Dan Stanescu]

Do you have the correct imports?

[Iocta]

Which imports do you have?

[Kyle Miller]

Make sure you have

open_locale big_operators

to include the notation.

[Dan Stanescu]

I have all of these in a file for a different purpose, but you probably don't need the first two:

import data.polynomial
import data.real.basic
import algebra.big_operators

open_locale big_operators

[Iocta]

Ah, that's the trick

[Iocta]

What's the notation for (α × β) but with countable elements? Is that def myprod (t : ℕ → Type u) : Π (n: nat), t n := _?