Skip to content

Commit

Permalink
feat(measure_theory/bochner_integration): bochner integral of simple …
Browse files Browse the repository at this point in the history 
…functions (#1676)

* Bochner integral of simple functions

* Update bochner_integration.lean

* Change notation for simple functions in L1 space; Fill in blanks in `calc` proofs

* Better definitions of operations on integrable simple functions

* Update src/measure_theory/bochner_integration.lean

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* Update src/measure_theory/bochner_integration.lean

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* Update src/measure_theory/bochner_integration.lean

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* Update src/measure_theory/bochner_integration.lean

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* Update src/measure_theory/bochner_integration.lean

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* Update src/measure_theory/bochner_integration.lean

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>

* Several fixes - listed below

* K -> \bbk
* remove indentation after `calc`
* use local instances
* one tactic per line
* add `elim_cast` attributes
* remove definitions from nolints.txt
* use `linear_map.with_bound` to get continuity

* Update documentation and comments

* Fix things

* norm_triangle_sum -> norm_sum_le
* fix documentations and comments (The Bochner integral)

* Fix typos and grammatical errors

* Update src/measure_theory/ae_eq_fun.lean

Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>
  • Loading branch information
@sgouezel @mergify
2 people authored and mergify[bot] committed Nov 25, 2019
1 parent 6af35ec commit 242159f
Show file tree
Hide file tree
Showing 5 changed files with 808 additions and 167 deletions.
4 changes: 0 additions & 4 deletions scripts/nolints.txt
View file
Expand Up @@ -1697,14 +1697,10 @@ measure_theory.ae_eq_fun.integrable
measure_theory.ae_eq_fun.neg
measure_theory.ae_eq_fun.smul
measure_theory.integrable
measure_theory.integral
measure_theory.l1.integral
measure_theory.l1.simple_func
measure_theory.l1.simple_func.exists_simple_func_near
measure_theory.l1.simple_func.integral
measure_theory.l1.simple_func.mk
measure_theory.l1.simple_func.to_simple_func
measure_theory.l1.smul
measure_theory.lintegral_eq_nnreal
measure_theory.measure
measure_theory.measure.integral
Expand Down
11 changes: 11 additions & 0 deletions src/linear_algebra/basic.lean
View file
Expand Up @@ -67,6 +67,17 @@ lemma smul_sum {α : Type u} {M : Type v} {R : Type w}
a • (s.sum f) = s.sum (λc, a • f c) :=
(finset.sum_hom ((•) a)).symm

lemma smul_sum' {α : Type u} {M : Type v} {R : Type w}
[ring R] [add_comm_group M] [module R M]
{s : finset α} {f : α → R} {x : M} :
(s.sum f) • x = s.sum (λa, (f a) • x) :=
begin
-- TODO : where should I put this instance?
haveI : is_add_monoid_hom (λ (r : R), r • x) :=
{ map_add := λ a b, add_smul _ _ _, map_zero := zero_smul _ _ },
exact (finset.sum_hom (λ (r : R), r • x)).symm
end

end finset

namespace finsupp
Expand Down
42 changes: 23 additions & 19 deletions src/measure_theory/ae_eq_fun.lean
View file
Expand Up @@ -271,7 +271,7 @@ comp₂ (+) (measurable_add (measurable_fst measurable_id) (measurable_snd meas
instance : has_add (α →ₘ γ) := ⟨ae_eq_fun.add⟩

@[simp] lemma mk_add_mk (f g : α → γ) (hf hg) :
(mk f hf) + (mk g hg) = mk (λa, (f a) + (g a)) (measurable_add hf hg) := rfl
(mk f hf) + (mk g hg) = mk (f + g) (measurable_add hf hg) := rfl

lemma add_to_fun (f g : α →ₘ γ) : ∀ₘ a, (f + g).to_fun a = f.to_fun a + g.to_fun a :=
comp₂_to_fun _ _ _ _
Expand Down Expand Up @@ -344,24 +344,24 @@ end add_comm_group

section semimodule

variables {K : Type*} [semiring K] [topological_space K]
variables {𝕜 : Type*} [semiring 𝕜] [topological_space 𝕜]
variables {γ : Type*} [topological_space γ]
[add_comm_monoid γ] [semimodule K γ] [topological_semimodule K γ]
[add_comm_monoid γ] [semimodule 𝕜 γ] [topological_semimodule 𝕜 γ]

protected def smul : K → (α →ₘ γ) → (α →ₘ γ) :=
protected def smul : 𝕜 → (α →ₘ γ) → (α →ₘ γ) :=
λ c f, comp (has_scalar.smul c) (measurable_smul measurable_id) f

instance : has_scalar K (α →ₘ γ) := ⟨ae_eq_fun.smul⟩
instance : has_scalar 𝕜 (α →ₘ γ) := ⟨ae_eq_fun.smul⟩

@[simp] lemma smul_mk (c : K) (f : α → γ) (hf) : c • (mk f hf) = mk (c • f) (measurable_smul hf) :=
@[simp] lemma smul_mk (c : 𝕜) (f : α → γ) (hf) : c • (mk f hf) = mk (c • f) (measurable_smul hf) :=
rfl

lemma smul_to_fun (c : K) (f : α →ₘ γ) : ∀ₘ a, (c • f).to_fun a = c • f.to_fun a :=
lemma smul_to_fun (c : 𝕜) (f : α →ₘ γ) : ∀ₘ a, (c • f).to_fun a = c • f.to_fun a :=
comp_to_fun _ _ _

variables [second_countable_topology γ] [topological_add_monoid γ]

instance : semimodule K (α →ₘ γ) :=
instance : semimodule 𝕜 (α →ₘ γ) :=
{ one_smul := by { rintros ⟨f, hf⟩, simp only [quot_mk_eq_mk, smul_mk, one_smul] },
mul_smul :=
by { rintros x y ⟨f, hf⟩, simp only [quot_mk_eq_mk, smul_mk, mul_action.mul_smul x y f], refl },
Expand All @@ -377,27 +377,29 @@ instance : semimodule K (α →ₘ γ) :=
exact add_smul x y f
end,
zero_smul :=
by { rintro ⟨f, hf⟩, simp only [quot_mk_eq_mk, smul_mk, zero_def], congr, exact zero_smul K f }}
by { rintro ⟨f, hf⟩, simp only [quot_mk_eq_mk, smul_mk, zero_def], congr, exact zero_smul 𝕜 f }}

instance : mul_action 𝕜 (α →ₘ γ) := by apply_instance

end semimodule

section module

variables {K : Type*} [ring K] [topological_space K]
variables {𝕜 : Type*} [ring 𝕜] [topological_space 𝕜]
variables {γ : Type*} [topological_space γ] [second_countable_topology γ] [add_comm_group γ]
[topological_add_group γ] [module K γ] [topological_semimodule K γ]
[topological_add_group γ] [module 𝕜 γ] [topological_semimodule 𝕜 γ]

instance : module K (α →ₘ γ) := { .. ae_eq_fun.semimodule }
instance : module 𝕜 (α →ₘ γ) := { .. ae_eq_fun.semimodule }

end module

section vector_space

variables {K : Type*} [discrete_field K] [topological_space K]
variables {𝕜 : Type*} [discrete_field 𝕜] [topological_space 𝕜]
variables {γ : Type*} [topological_space γ] [second_countable_topology γ] [add_comm_group γ]
[topological_add_group γ] [vector_space K γ] [topological_semimodule K γ]
[topological_add_group γ] [vector_space 𝕜 γ] [topological_semimodule 𝕜 γ]

instance : vector_space K (α →ₘ γ) := { .. ae_eq_fun.semimodule }
instance : vector_space 𝕜 (α →ₘ γ) := { .. ae_eq_fun.semimodule }

end vector_space

Expand Down Expand Up @@ -426,7 +428,7 @@ begin
end

lemma eintegral_add : ∀(f g : α →ₘ ennreal), eintegral (f + g) = eintegral f + eintegral g :=
by rintros ⟨f⟩ ⟨g⟩; simp only [quot_mk_eq_mk, mk_add_mk, eintegral_mk, lintegral_add f.2 g.2]
by { rintros ⟨f⟩ ⟨g⟩, simp only [quot_mk_eq_mk, mk_add_mk, eintegral_mk], exact lintegral_add f.2 g.2 }

lemma eintegral_le_eintegral {f g : α →ₘ ennreal} (h : f ≤ g) : eintegral f ≤ eintegral g :=
begin
Expand All @@ -449,6 +451,8 @@ comp₂_to_fun _ _ _ _
lemma comp_edist_self : ∀ (f : α →ₘ γ), comp_edist f f = 0 :=
by rintro ⟨f⟩; refine quotient.sound _; simp only [edist_self]

/-- Almost everywhere equal functions form an `emetric_space`, with the emetric defined as
`edist f g = ∫⁻ a, edist (f a) (g a)`. -/
instance : emetric_space (α →ₘ γ) :=
{ edist := λf g, eintegral (comp_edist f g),
edist_self := assume f, (eintegral_eq_zero_iff _).2 (comp_edist_self _),
Expand Down Expand Up @@ -517,10 +521,10 @@ section normed_space

set_option class.instance_max_depth 100

variables {K : Type*} [normed_field K]
variables {γ : Type*} [normed_group γ] [second_countable_topology γ] [normed_space K γ]
variables {𝕜 : Type*} [normed_field 𝕜]
variables {γ : Type*} [normed_group γ] [second_countable_topology γ] [normed_space 𝕜 γ]

lemma edist_smul (x : K) : ∀ f : α →ₘ γ, edist (x • f) 0 = (ennreal.of_real ∥x∥) * edist f 0 :=
lemma edist_smul (x : 𝕜) : ∀ f : α →ₘ γ, edist (x • f) 0 = (ennreal.of_real ∥x∥) * edist f 0 :=
begin
rintros ⟨f, hf⟩, simp only [zero_def, edist_mk_mk', quot_mk_eq_mk, smul_mk],
exact calc
Expand Down

0 comments on commit 242159f

Please sign in to comment.