integrable_on

Stream: new members

[Iocta]

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]

Do we have a measure.comap?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

aha, docs#measure_theory.measure.with_density

[Mario Carneiro]

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]

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]

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]

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

[Mario Carneiro]

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]

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]

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

[Iocta]

ok

[Reid Barton]

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]

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]

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]

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

[Reid Barton]

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

[Iocta]

That helps

[Iocta]

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

[Alex J. Best]

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

[Iocta]

failed to find a derive handler for 'fintype'

[Alex J. Best]

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]

Ah

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

[Reid Barton]

Is it actually noncomputable?

[Iocta]

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

[Reid Barton]

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

[Iocta]

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]

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

[Kenny Lau]

(this is rfl)

[Mario Carneiro]

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

kenny beat me to the punchline

[Iocta]

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

[Kenny Lau]

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

[Kenny Lau]

it has type finset X

[Kenny Lau]

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

[Mario Carneiro]

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

[Iocta]

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

[Iocta]

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]

because real numbers are not computable

[Mario Carneiro]

if you use rat it should be computable

[Iocta]

I see

[Mario Carneiro]

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

[Mario Carneiro]

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

[Iocta]

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]

oh

[Iocta]

parens

[Kenny Lau]

I think that's stupid

[Kenny Lau]

we need to fix the precedence levels

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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