# Zulip Chat Archive

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

aha, docs#measure_theory.measure.with_density

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

Here's another bad instance:

```
@[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

#### Iocta (Aug 11 2020 at 04:50):

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
```

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

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,
refine eq.trans _ add_to_one,
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
refine eq.trans _ add_to_one,
simp [add_assoc],
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

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

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

What's it talking about?

```
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
-- ⊢ add_comm_monoid Prop
```

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

oh

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

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