# Zulip Chat Archive

## Stream: new members

### Topic: Definition of simple functions and its integral

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

#### Johan Commelin (May 13 2019 at 15:37):

Typically, writing definitions is not enough...

#### Johan Commelin (May 13 2019 at 15:37):

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

#### Johan Commelin (May 13 2019 at 15:38):

@Joe do you have some goal in mind?

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

#### 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?

#### 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.

#### Joe (May 13 2019 at 16:44):

Probably I'll use a similar approach.

#### Joe (May 13 2019 at 16:52):

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

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

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

#### 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.

#### Johan Commelin (May 13 2019 at 17:28):

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

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

#### 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.

#### 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.

#### Joe (May 13 2019 at 17:40):

I’ll try to work out the basic lemmas.

#### 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.

#### 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.

#### Joe (May 13 2019 at 17:52):

I think it is `ennreal.of_real`

that can be done using a coercion?

#### Joe (May 13 2019 at 17:53):

Or you mean I first define a coercion from `ennreal`

to `real`

?

#### Johan Commelin (May 13 2019 at 17:55):

The coercion already exists.

#### Johan Commelin (May 13 2019 at 17:55):

Maybe you can just remove it from your code

#### Johan Commelin (May 13 2019 at 17:55):

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

#### Joe (May 13 2019 at 17:56):

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

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

ℝ

#### Johan Commelin (May 13 2019 at 17:57):

Aah.... sorry

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

s with the same underlying function have the same integral

#### Johan Commelin (May 13 2019 at 17:57):

That of course only works if it's `nnreal`

#### Johan Commelin (May 13 2019 at 17:58):

You can't coerce infinity to a real

#### 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.

#### Joe (May 13 2019 at 18:02):

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

.

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