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


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

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