Integral of a constant

Stream: general

[Koundinya Vajjha]

I am stuck on the following goal for a test lemma:

α : Type u,
_inst_1 : measurable_space α,
D : probability_measure bool,
h : true
⊢ measure.integral (D.to_measure) (λ (a : bool), 1) = 1

Where I have extended the measure structure with the extra field that the measure of univ is 1. Is there a lemma which says I can rewrite the LHS as the measure of the whole set?

[Kevin Buzzard]

I can't help you, but it's wonderful to see that people are now trying to do differentiation and integration. Very little has happened in this area since 2017, until recently, when things seem to be slowly taking off. An attainable (in my opinion) goal is to have Lean's maths library knowing essentially all of a pure mathematics degree course within the next few years, and this stuff is absolutely essential.

[Mario Carneiro]

There doesn't seem to be much about measure.integral yet. Also it's generally presumed that the measure of univ is infinite, so there isn't much about stuff like integrable constant functions. Presumably that's part of the focus of your probability_measure work. measure.integral is defined in terms of lintegral, which has the theorem simple_func.lintegral_eq_integral. Show that the constant function is a simple function; it follows that the integral of a is a * measure univ = a for a probability measure.

[Koundinya Vajjha]

apply simple_func.lintegral_eq_integral is giving me a deterministic timeout. I probably shouldn't have done this, but are there any general reasons behind an apply giving deterministic timeouts?

[Kevin Buzzard]

Can you post a complete working example?

[Kevin Buzzard]

It might be trying to prove that two types are defeq when they're not, it might be user error, it might be that two types are defeq but it's very hard to prove, it might be fixable by changing the timeout parameter (but the point of the -T50000 thread is that we'd rather be changing it the other way ;-) )

[Koundinya Vajjha]

Here a complete working example:

import measure_theory.giry_monad

open set measure_theory measurable_space

infixl `>>=ₐ` :55 := measure_theory.measure.bind
local notation `do` binders `←ₐ` m `;` t:(scoped p, m >>=ₐ p) := t
local notation `ret` := measure_theory.measure.dirac

variable [measurable_space ℕ]

structure probability_measure (α : Type*) [measurable_space α] extends measure_theory.measure α :=
(is_one : measure_of univ = 1)

noncomputable def double(m: probability_measure ℕ) : measure ℕ :=
do x ←ₐ m.to_measure;
ret (2 * x)

def even := {x | ∃ k, x = 2 * k}

lemma test:
∀ m: probability_measure ℕ, ∀ m': measure ℕ,
m' = double(m) → m'(even) = 1 :=
begin
  intros,
  unfold even,
  unfold double at a,
  rewrite a,
  clear a,
  rewrite measure.bind_apply,

end

I'm afraid I don't know if this is even provable with the current technology...

[Mario Carneiro]

This is provable, but it looks like one of those things I don't want to prove. As in, I challenge the premise that this theorem matters. It reminds me of Kevin's M1F problems

[Koundinya Vajjha]

Let's just say it matters very much to me.

[Mario Carneiro]

Step back. What do you want to say?

[Mario Carneiro]

maybe this isn't the easiest way to formalize whatever the real goal is

[Koundinya Vajjha]

Basically I want to reason about the measure which is returned by the do x <- D; return(f(x) part of the Giry monad.

[Mario Carneiro]

first of all, bind return is map

[Mario Carneiro]

This generalizes in a few ways. The double function doesn't matter, replace it with an arbitrary function A -> B

[Mario Carneiro]

the measure takes values in the image of the function

[Koundinya Vajjha]

Yes. Well maybe this particular example is too hard.

[Mario Carneiro]

Examples are always harder than general theorems

[Mario Carneiro]

they add additional irrelevant stuff

[Koundinya Vajjha]

Basically I want to reason about the measure which is returned by the do x <- D; return(f(x) part of the Giry monad.

In particular, I want to characterize the measure zero sets of this measure.

[Mario Carneiro]

It's not hard to prove your theorem using measure.map_apply once you have the monad laws

[Koundinya Vajjha]

Okay this is the most general I can make it

lemma test [measurable_space α][measurable_space β] (D : measure α) (p : α → β) (A : set β) [hs : is_measurable A] :
(measure_theory.measure.bind D (λ x, measure_theory.measure.dirac $ p x)) A = D {x | p x ∈ A} := sorry

[Mario Carneiro]

the thing on the right is D.map p A

[Mario Carneiro]

so this is the monad law

[Koundinya Vajjha]

That worked. (Btw it's failing to apply the coe_fn coercion. I need to explicitly say (D.map p).measure_of A.

[Mario Carneiro]

you can use (D.map p : function type) A

[Koundinya Vajjha]

Still stuck on essentially the same goal as the first case. :(

⊢measure.integral D (λ (a : α), ⨆ (h : p a ∈ A), 1) = ⇑D (p ⁻¹' A)

If I understand you correctly, there surely isn't a purely abstract proof using just the monad laws, is there? You have to use the Giry monad bind and return somewhere to prove this right?

[Mario Carneiro]

there should be an abstract proof

[Mario Carneiro]

using lemmas about Giry bind and return

[Mario Carneiro]

which are the same as the usual monad laws

[Koundinya Vajjha]

Sorry I just can't see how that can be..

[Koundinya Vajjha]

Can you sketch a proof?

[Mario Carneiro]

@Koundinya Vajjha The current dirac_bind is not one of the monad laws, it's too weak. The real monad law says that m >>= pure o f = f <$> m, and dirac_bind is the special case when f = id. So we can take inspiration from this and try to generalize the proof of dirac_bind with a function and deduce dirac_bind as a consequence:

lemma dirac_bind_comp {m : measure α} {f : α → β} (hf : measurable f) :
  bind m (λ x, dirac $ f x) = map f m :=
measure.ext $ assume s hs, begin
  rw [bind_apply hs (measurable_dirac.comp hf), map_apply hf hs],
  conv {to_lhs, congr, skip, funext, rw dirac_apply _ hs},
  transitivity, apply lintegral_supr_const,
  exact hf _ hs, rw one_mul, refl
end

lemma dirac_bind {m : measure α} : bind m dirac = m :=
(dirac_bind_comp measurable_id).trans map_id

[Koundinya Vajjha]

Thanks a lot Mario!!

[Kevin Buzzard]

So this is an absolutely serious statement. I went to a 24 lecture course on measure theory as an undergraduate and we learnt about sigma algebras and Borel measures and Lebesgue measure and the Borel Cantelli lemma and all that stuff which mathematicians think of as standard, but for absolute sure there were no monads and certainly no monad law. Is this just some statement that is mathematically very straightforward but turns out to be some sort of universal statement for measures which would have been presented to us as an "obvious fact" or something?

[Kevin Buzzard]

All this measure theory chat is completely passing me by. When people start doing MSc level stuff that's fine, that's what I'd expect, but I had still expected to be following what was going on at this stage.

[Andrew Ashworth]

If there's one thing type theorists love, it's categories. The original paper by Giry is here A Categorical Approach to Probability Theory.

[Andrew Ashworth]

I'm also a little confused by Giry monads, but also very interested in concrete probability theory. I suppose I'll sit down and wrestle with the terminology once the library is a little more complete...

[Kevin Buzzard]

But on the other hand we had a colloquium by Hugo Duminil-Copin at Imperial last week and I went out to dinner with him afterwards and asked him if he'd heard of the Giry monad and he said no. He's a regular mathematician though, not a type theorist. There's something funny going on. Type theorists might like it but probabilists don't use it, so my guess is that it is probably a beautiful way of saying something relatively straightforward to a mathematician; I suspect it's just the observation that one can use the language of monads to precisely encapsulate some standard phenomenon in measure theory, so it doesn't buy the mathematician anything in practice, but it makes part of the theory much more pleasant to formalise. I remember when I learnt that a morphism of sheaves was a natural transformation of functors -- I just thought "cool" but it didn't mean I understood morphisms of sheaves any better, it just meant that I was suddenly better at remembering the precise list of axioms for a morphism of sheaves in some sense.

[Koundinya Vajjha]

I've never come across the Giry monad myself until I got interested in it thanks to Johannes' work. The fundamental fact which everyone glosses over which makes this thing work is that the space of all measures on a set is also a measurable space. (Take the weak* topology and the borel sigma algebra wrt to that and you have a measurable space).

IMO, the Giry monad will pop up sooner or later when you ask a mathematician how to rigorously formalize the statement "sample a point from a distribution D". Indeed that was my motivation in discovering it as well.

[Koundinya Vajjha]

We make these sort of statements all the time, but never (until now) have thought of what the best way to formalize these things would be in a proof assistant.

[Koundinya Vajjha]

Part of the appeal of the Giry monad is then to "sample a point from a distribution D", you can say do x <- D, return (x). It's really quite beautiful.

[Kevin Buzzard]

Seeing that as beautiful is something which a certain kind of person does -- and perhaps the probabilist I talked to was not that kind of person. Thanks for the explanation! I read some of the pdf link. It's a cute thing.

[Mario Carneiro]

The really powerful thing about the Giry monad is it allows you to do operations on random variables without a massive amount of notation overloading to make sense of those x * cos Y expressions

[Mario Carneiro]

I'm sure no mathematician or statistician would even think of calling this a monad, because ad hoc notation overloading is just what they do, but they never had to prove anything formally about those expressions

[Mario Carneiro]

I suspect it's just the observation that one can use the language of monads to precisely encapsulate some standard phenomenon in measure theory, so it doesn't buy the mathematician anything in practice, but it makes part of the theory much more pleasant to formalise.

^ this