Zulip Chat Archive

Stream: new members

Topic: Definition of simple functions and its integral


view this post on Zulip Joe (May 13 2019 at 14:05):

Hi everyone,
here is a definition for integral over simple functions,
a definition for simple functions as a subtype of integrable functions,
and a definition for its integral.

Do these look okay?

variables  {γ : Type*}  [normed_space ℝ γ] [second_countable_topology γ] [topological_add_group γ]

def integral' (f : measure_theory.simple_func α γ) : γ :=
  f.range.sum (λ (x : γ), (ennreal.to_real (volume (f ⁻¹' {x}))) • x)

section
variables (α γ)
def simple_func : Type* :=
  { f : α →ᵢ γ // ∃ (s : measure_theory.simple_func α γ), (ae_eq_fun.mk s s.measurable) = f.val}
end

local infixr ` →ₛ `:25 := simple_func

def integral_over_simple_func (f : α →ₛ γ) : γ := integral' (classical.some f.2)

view this post on Zulip Johan Commelin (May 13 2019 at 15:37):

Typically, writing definitions is not enough...

view this post on Zulip Johan Commelin (May 13 2019 at 15:37):

You have to prove some basic lemmas to connect your definition with the real world

view this post on Zulip Johan Commelin (May 13 2019 at 15:38):

@Joe do you have some goal in mind?

view this post on Zulip Joe (May 13 2019 at 16:36):

Yeah, I think then I will prove simple functions are dense in integrable functions. And then define the integral on integrable functions.

lemma simple_func_dense_embedding : dense_embedding (subtype.val : (α →ₛ γ) → (α →ᵢ γ)) := sorry
def integral (f : α →ᵢ γ) : γ := dense_embedding.extend simple_func_dense_embedding integral_over_simple_func f

view this post on Zulip Koundinya Vajjha (May 13 2019 at 16:39):

@Joe did you have a look at https://github.com/leanprover-community/mathlib/blob/ffa6d6992c4de076154fdefad79c2488bcb48bbd/src/measure_theory/integration.lean?

view this post on Zulip Joe (May 13 2019 at 16:42):

I know. We already have an integral on α → ennreal, but it seems that we want to define the Bochner integral and integrate on Banach space.

view this post on Zulip Joe (May 13 2019 at 16:44):

Probably I'll use a similar approach.

view this post on Zulip Joe (May 13 2019 at 16:52):

I feel definitions are more important than proofs. So I want to be more careful with them.

view this post on Zulip Kevin Buzzard (May 13 2019 at 17:12):

I know how you feel. If you give a bad proof, who cares? Someone can come along and give a better proof and nothing really changes. But with a bad definition you have type class issues or something that's impossible to work with or something

view this post on Zulip Johan Commelin (May 13 2019 at 17:25):

@Joe Certainly. But the way to demonstrate that your definitions are really good is by proving theorems that use them

view this post on Zulip Johan Commelin (May 13 2019 at 17:27):

Can you prove that the integral of a constant function over a compact set has the expected value? That is a first baby-step to validating that your definition is usable.

view this post on Zulip Johan Commelin (May 13 2019 at 17:28):

You will want to prove how integration interacts with addition, subtraction, etc...

view this post on Zulip Johan Commelin (May 13 2019 at 17:28):

You also need to show how it interacts with existing notions of integration that are in the library

view this post on Zulip Johan Commelin (May 13 2019 at 17:28):

All of this is of course a lot of work. And you don't have to do this alone. But you will have to put in some effort.

view this post on Zulip Joe (May 13 2019 at 17:40):

Yes, this is exactly how I feel. If I give a bad definition then in the future all proofs depending on the definition may need to be reworked.

view this post on Zulip Joe (May 13 2019 at 17:40):

I’ll try to work out the basic lemmas.

view this post on Zulip Joe (May 13 2019 at 17:43):

I do have doubts about the definitions. I don’t like the ‘ennneal.to_real’ there. And I use ‘classical.some’. I don’t like that either.

view this post on Zulip Johan Commelin (May 13 2019 at 17:44):

The ennreal.to_real can be done using a coercion. And in fact that is the better way to do it.

view this post on Zulip Joe (May 13 2019 at 17:52):

I think it is ennreal.of_real that can be done using a coercion?

view this post on Zulip Joe (May 13 2019 at 17:53):

Or you mean I first define a coercion from ennreal to real?

view this post on Zulip Johan Commelin (May 13 2019 at 17:55):

The coercion already exists.

view this post on Zulip Johan Commelin (May 13 2019 at 17:55):

Maybe you can just remove it from your code

view this post on Zulip Johan Commelin (May 13 2019 at 17:55):

If that doesn't work, wrap its argument in (_ : \real)

view this post on Zulip Joe (May 13 2019 at 17:56):

You mean like this (volume (f ⁻¹' {x})) : ℝ)

view this post on Zulip Joe (May 13 2019 at 17:57):

But it is an error it seems :

invalid type ascription, term has type
ennreal
but is expected to have type

view this post on Zulip Johan Commelin (May 13 2019 at 17:57):

Aah.... sorry

view this post on Zulip Reid Barton (May 13 2019 at 17:57):

In order to deal with the classical.some you'll want to prove a lemma that says that you can evaluate the integral of a simple_func using any choice of measure_theory.simple_func, which amounts to proving that two measure_theory.simple_funcs with the same underlying function have the same integral

view this post on Zulip Johan Commelin (May 13 2019 at 17:57):

That of course only works if it's nnreal

view this post on Zulip Johan Commelin (May 13 2019 at 17:58):

You can't coerce infinity to a real

view this post on Zulip Joe (May 13 2019 at 18:01):

Yes. Cannot coerce infinity to a real. It is possible for a set to have infinite measure, but since here we are dealing with a simple function, set with infinite measure will be mapped to zero, so it doesn't matter.

view this post on Zulip Joe (May 13 2019 at 18:02):

@Reid Barton Yeah, so that is how I can eliminate the exists.

view this post on Zulip Sebastien Gouezel (May 13 2019 at 18:39):

Probably a good reference is http://isabelle.in.tum.de/dist/library/HOL/HOL-Analysis/Bochner_Integration.html


Last updated: May 08 2021 at 10:12 UTC