Definition of simple functions and its integral

Stream: new members

[Joe]

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]

Typically, writing definitions is not enough...

[Johan Commelin]

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

[Johan Commelin]

@Joe do you have some goal in mind?

[Joe]

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]

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

[Joe]

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]

Probably I'll use a similar approach.

[Joe]

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

[Kevin Buzzard]

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]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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]

I’ll try to work out the basic lemmas.

[Joe]

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]

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

[Joe]

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

[Joe]

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

[Johan Commelin]

The coercion already exists.

[Johan Commelin]

Maybe you can just remove it from your code

[Johan Commelin]

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

[Joe]

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

[Joe]

But it is an error it seems :

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

[Johan Commelin]

Aah.... sorry

[Reid Barton]

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]

That of course only works if it's nnreal

[Johan Commelin]

You can't coerce infinity to a real

[Joe]

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]

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

[Sebastien Gouezel]

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