## Stream: new members

### Topic: integrable_on

#### Iocta (Aug 11 2020 at 00:00):

I saw there's some new material in mathlib about measure. Can I use this to say like "f(x)=1/(b-a) is integrable on [a,b] and integrates to 1 so it's a probability measure"?

#### Mario Carneiro (Aug 11 2020 at 00:03):

Do we have a measure.comap?

#### Mario Carneiro (Aug 11 2020 at 00:04):

To define a measure from a function we need some kind of integral based measure

#### Mario Carneiro (Aug 11 2020 at 00:04):

that's before even getting to the question of turning that into a probability measure

#### Mario Carneiro (Aug 11 2020 at 00:09):

so you just make that into a probability measure, using with_density_apply and prove that the integral of f over [a,b] is 1

#### Iocta (Aug 11 2020 at 03:44):

I don't think I understand

import measure_theory.bochner_integration
import analysis.normed_space.indicator_function
import measure_theory.set_integral
import analysis.specific_limits
import data.real.basic

open set filter topological_space measure_theory
open_locale classical topological_space interval

def uniform (x : real) : real := 1

def unit_interval : set real := Icc 0 1

lemma unit_interval_measurable : is_measurable unit_interval :=
is_measurable_Icc

set_option trace.class_instances

#check with_density_apply ↑uniform unit_interval_measurable

-- lemma with_density_apply (f : α → ennreal) {s : set α} (hs : is_measurable s) ...

-- maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')

-- invalid Boolean option value, 'true' or 'false' expected


#### Mario Carneiro (Aug 11 2020 at 04:05):

Well, there are a lot of weird things in that trace. I was wondering what a to_string (ℝ →. ℝ) had to do with the original goal of has_lift_t (ℝ → ℝ) (ℝ → ennreal), and found this

@[instance]
protected meta def widget.html.to_string_coe :
Π {α β : Type} [_inst_1 : has_to_string β], has_coe β (widget.html α) :=


#### Mario Carneiro (Aug 11 2020 at 04:06):

Looking at an instance trace is like looking under the couch while cleaning

#### Mario Carneiro (Aug 11 2020 at 04:21):

@[instance]
protected def lift_fn_range : Π {a : Sort ua} {b₁ : Sort ub₁} {b₂ : Sort ub₂} [_inst_1 : has_lift_t b₁ b₂],
has_lift (a → b₁) (a → b₂) :=


The fact that this goes from lift_t to lift means that it can be pumped by instances that expect that a lift_t allows the output to be more complicated than the input:

protected def filter.germ.has_lift_t : Π {α : Type u_1} {β : Type u_2} {l : filter α}, has_lift_t β (l.germ β) :=


Together this means that has_lift (A -> B) (A -> l.germ B) so a search for has_lift_t (A -> B) ?C diverges:

has_lift_t (A -> B) ?C <- has_lift_t (A -> ?l.germ B) ?C <-has_lift_t (A -> ?l.germ (?l.germ B)) ?C <- ...


#### Mario Carneiro (Aug 11 2020 at 04:22):

Anyway, the short answer to your question @Iocta is that there is no coercion from real to ennreal so ↑uniform doesn't work. Make it a function real -> ennreal instead

#### Mario Carneiro (Aug 11 2020 at 04:26):

Oh wow, lift_fn_range is in core, and has been there since the dawn of time

ok

#### Reid Barton (Aug 11 2020 at 10:00):

Iocta said:

I don't think I understand

set_option trace.class_instances

-- invalid Boolean option value, 'true' or 'false' expected


You're missing true at the end of that line.

#### Iocta (Aug 11 2020 at 19:55):

Having various issues:

import measure_theory.probability_mass_function
import analysis.normed_space.indicator_function
import measure_theory.set_integral
import analysis.specific_limits
import data.real.basic

open set filter topological_space measure_theory
open_locale classical topological_space interval

inductive letter : Type
| a : letter
| b : letter
| c : letter

namespace letter

instance fintype: fintype letter :=
begin
-- ⊢ fintype letter
sorry,
end

def f_letter : letter → nnreal
| a := 0.5
| b := 0.3
| c := 1 - (f_letter a) - (f_letter b)
-- equation compiler failed to generate bytecode for 'f_letter._main'
-- nested exception message:
-- code generation failed, VM does not have code for 'classical.choice'

def letter_pmf : pmf letter :=
pmf.of_fintype f_letter
begin
simp,
-- ⊢ finset.univ.sum f_letter = 1
sorry,
end,

end letter


#### Reid Barton (Aug 11 2020 at 19:57):

The f_letter errors look like one or more bugs, but in any case it needs noncomputable (or just add noncomputable theory near the top somewhere)

#### Reid Barton (Aug 11 2020 at 19:58):

I think the definition of f_letter was wrong for two different reasons, and Lean got confused as a result.

#### Reid Barton (Aug 11 2020 at 19:58):

noncomputable def f_letter : letter → nnreal
| a := 0.5
| b := 0.3
| c := 0.2


That helps

#### Iocta (Aug 11 2020 at 20:13):

is there a trick to filling these? instance fintype: fintype letter := sorry

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

Does @[derive fintype] on the line before inductive letter work?

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

failed to find a derive handler for 'fintype'

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

Oh yeah there was a thread about this. If you search for enumerated types are fintypes in zulip you should find a thread with that name with an example of this

#### Iocta (Aug 11 2020 at 20:28):

Ah

noncomputable instance fintype: fintype letter :=
{elems := {a, b, c}, complete := λ x, by cases x; simp}


#### Reid Barton (Aug 11 2020 at 20:30):

Is it actually noncomputable?

#### Iocta (Aug 11 2020 at 20:31):

I'm just believing what it tells me definition 'fintype' is noncomputable, it depends on 'classical.prop_decidable'

#### Reid Barton (Aug 11 2020 at 20:33):

I see. I think you should add @[derive decidable_eq] before inductive letter (on the other hand, maybe you don't care).

#### Iocta (Aug 11 2020 at 21:26):

Can I fill the sorry?

import measure_theory.probability_mass_function
import analysis.normed_space.indicator_function
import measure_theory.set_integral
import analysis.specific_limits
import data.real.basic

open set filter topological_space measure_theory
open_locale classical topological_space interval

@[derive decidable_eq]
inductive letter : Type
| a : letter
| b : letter
| c : letter

namespace letter

instance fintype: fintype letter :=
{elems := {a, b, c}, complete := λ x, by cases x; simp}

noncomputable def letter_f : letter → nnreal
| a := 0.5
| b := 0.3
| c := 0.2

lemma add_to_one : letter_f a + letter_f b + letter_f c = 1 :=
begin
simp [letter_f] at *,
ring,
ext1,
norm_num,
end

noncomputable def letter_pmf : pmf letter :=
pmf.of_fintype letter_f
begin
simp,
unfold finset.univ,
-- ⊢ (fintype.elems letter).sum letter_f = a.letter_f + b.letter_f + c.letter_f
sorry,
end

end letter


#### Kenny Lau (Aug 11 2020 at 21:29):

prove an auxiliary lemma (finset.univ : finset letter) = {a, b, c}

#### Kenny Lau (Aug 11 2020 at 21:29):

(this is rfl)

#### Mario Carneiro (Aug 11 2020 at 21:31):

@[simp] theorem letter_univ : (finset.univ : finset letter) = {a, b, c} := rfl

noncomputable def letter_pmf : pmf letter :=
pmf.of_fintype letter_f
begin
end


#### Mario Carneiro (Aug 11 2020 at 21:31):

kenny beat me to the punchline

#### Iocta (Aug 11 2020 at 21:40):

How to interpret  (finset.univ : finset letter)  ?

#### Kenny Lau (Aug 11 2020 at 21:42):

finset.univ implicitly takes a type X and an instance of fintype X

#### Kenny Lau (Aug 11 2020 at 21:42):

it has type finset X

#### Kenny Lau (Aug 11 2020 at 21:42):

it is formed by simply extracting the finset.elems in the instance of fintype X

#### Mario Carneiro (Aug 11 2020 at 21:43):

You can also write @finset.univ letter _ if you prefer

#### Iocta (Aug 11 2020 at 23:32):

What is the significance of noncomputable here? is it related to why #eval letter_f a doesn't work?

#### Iocta (Aug 11 2020 at 23:42):

IOW, why do I need to make

noncomputable def letter_f : letter → nnreal
| a := 0.5
| b := 0.3
| c := 0.2


noncomputable?

#### Mario Carneiro (Aug 11 2020 at 23:43):

because real numbers are not computable

#### Mario Carneiro (Aug 11 2020 at 23:44):

if you use rat it should be computable

I see

#### Mario Carneiro (Aug 11 2020 at 23:45):

anyway I don't think this is a big issue if you are just doing measure theory

#### Mario Carneiro (Aug 11 2020 at 23:45):

you can still prove e.g. letter_f a = 0.5 by rfl

#### Iocta (Aug 12 2020 at 04:18):

noncomputable def binomial_mass (n: ℕ) (p: nnreal) (hp: p ≤ 1) (k: ℕ) : nnreal :=
(nat.choose n k) * p ^ k * (1 - p) ^ (n - k)

lemma add_to_one (n : nat) (p : nnreal) (hp: p ≤ 1) : ∑'k , binomial_mass n p hp k = 1 :=
sorry
-- failed to synthesize type class instance for
-- n : ℕ,
-- p : nnreal,
-- hp : p ≤ 1


oh

parens

#### Kenny Lau (Aug 12 2020 at 06:35):

I think that's stupid

#### Kenny Lau (Aug 12 2020 at 06:35):

we need to fix the precedence levels

#### Yury G. Kudryashov (Aug 12 2020 at 07:19):

I'd use measure.restrict instead of measure.with_density.

#### Yury G. Kudryashov (Aug 12 2020 at 07:19):

We already have measure.restrict_apply, and I'll add a shortcut measure.restrict_apply soon.

Last updated: May 08 2021 at 04:14 UTC