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: Dec 20 2023 at 11:08 UTC