feat(measure_theory/bochner_integration): linearity of the Bochner In…

…tegral (leanprover-community#1745)

* Linearity of the Bochner Integral

* prove integral_neg and integral_smul with less assumptions; make integral irreducible

* remove simp tag

* create simp set for integral

* Add simp_attr.integral to nolint

* Make it possible to unfold the definition of `integral`

and other things.

* Update nolints.txt

* Make it possible to unfold l1.integral

* Update bochner_integration.lean

* Update bochner_integration.lean

scripts/nolints.txt

@@ -2671,6 +2671,7 @@ side
 side.other
 side.to_string
 simp_attr.functor_norm
+simp_attr.integral_simps
 simp_attr.monad_norm
 simp_attr.parity_simps
 simp_attr.push_cast

src/analysis/normed_space/operator_norm.lean

@@ -363,7 +363,7 @@ end
 
 section uniformly_extend
 
-variables [complete_space F] {e : E →L[𝕜] G} (h_dense : dense_range e)
+variables [complete_space F] (e : E →L[𝕜] G) (h_dense : dense_range e)
 
 section
 variables (h_e : uniform_inducing e)
@@ -393,7 +393,7 @@ have eq : _ := uniformly_extend_of_ind h_e h_dense f.uniform_continuous,
   cont := cont
 }
 
-@[simp] lemma extend_zero : extend (0 : E →L[𝕜] F) h_dense h_e = 0 :=
+@[simp] lemma extend_zero : extend (0 : E →L[𝕜] F) e h_dense h_e = 0 :=
 begin
   apply ext,
   refine is_closed_property h_dense (is_closed_eq _ _) _,
@@ -407,7 +407,7 @@ end
 section
 variables {N : ℝ} (h_e : ∀x, ∥x∥ ≤ N * ∥e x∥)
 
-local notation `ψ` := f.extend h_dense (uniform_embedding_of_bound _ _ h_e).to_uniform_inducing
+local notation `ψ` := f.extend e h_dense (uniform_embedding_of_bound _ _ h_e).to_uniform_inducing
 
 /-- If a dense embedding `e : E →L[𝕜] G` expands the norm by a constant factor `N⁻¹`, then the norm
     of the extension of `f` along `e` is bounded by `N * ∥f∥`. -/

src/measure_theory/ae_eq_fun.lean

@@ -349,11 +349,11 @@ variables {γ : Type*} [topological_space γ]
           [add_comm_monoid γ] [semimodule 𝕜 γ] [topological_semimodule 𝕜 γ]
 
 protected def smul : 𝕜 → (α →ₘ γ) → (α →ₘ γ) :=
-λ c f, comp (has_scalar.smul c) (measurable_smul measurable_id) f
+λ c f, comp (has_scalar.smul c) (measurable_smul _ measurable_id) f
 
 instance : has_scalar 𝕜 (α →ₘ γ) := ⟨ae_eq_fun.smul⟩
 
-@[simp] lemma smul_mk (c : 𝕜) (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 : 𝕜) (f : α →ₘ γ) : ∀ₘ a, (c • f).to_fun a = c • f.to_fun a :=

src/measure_theory/bochner_integration.lean

@@ -620,20 +620,20 @@ protected lemma uniform_embedding : uniform_embedding (coe : (α →₁ₛ β) 
 uniform_embedding_comap subtype.val_injective
 
 protected lemma uniform_inducing : uniform_inducing (coe : (α →₁ₛ β) → (α →₁ β)) :=
-l1.simple_func.uniform_embedding.to_uniform_inducing
+simple_func.uniform_embedding.to_uniform_inducing
 
 protected lemma dense_embedding : dense_embedding (coe : (α →₁ₛ β) → (α →₁ β)) :=
-l1.simple_func.uniform_embedding.dense_embedding $
+simple_func.uniform_embedding.dense_embedding $
 λ f, mem_closure_iff_nhds.2 $ λ t ht,
 let ⟨ε,ε0, hε⟩ := metric.mem_nhds_iff.1 ht in
 let ⟨s, h⟩ := exists_simple_func_near f ε0 in
 ne_empty_iff_exists_mem.2 ⟨_, hε (metric.mem_ball'.2 h), s, rfl⟩
 
 protected lemma dense_inducing : dense_inducing (coe : (α →₁ₛ β) → (α →₁ β)) :=
-l1.simple_func.dense_embedding.to_dense_inducing
+simple_func.dense_embedding.to_dense_inducing
 
-protected lemma closure_range : closure (range (coe : (α →₁ₛ β) → (α →₁ β))) = univ :=
-l1.simple_func.dense_embedding.to_dense_inducing.closure_range
+protected lemma dense_range : dense_range (coe : (α →₁ₛ β) → (α →₁ β)) :=
+simple_func.dense_inducing.dense
 
 variables (𝕜 : Type*) [normed_field 𝕜] [normed_space 𝕜 β]
 
@@ -654,7 +654,7 @@ section simple_func_integral
 
 variables [normed_space ℝ β]
 
-/-- Bochner integration over simple functions in l1 space. -/
+/-- The Bochner integral over simple functions in l1 space. -/
 def integral (f : α →₁ₛ β) : β := simple_func.bintegral (f.to_simple_func)
 
 lemma integral_eq_lintegral {f : α →₁ₛ ℝ} (h_pos : ∀ₘ a, 0 ≤ f.to_simple_func a) :
@@ -689,7 +689,7 @@ begin
   exact f.to_simple_func.norm_bintegral_le_bintegral_norm f.integrable
 end
 
-/-- Bochner integration over simple functions in l1 space as a continuous linear map. -/
+/-- The Bochner integral over simple functions in l1 space as a continuous linear map. -/
 def integral_clm : (α →₁ₛ β) →L[ℝ] β :=
 linear_map.with_bound ⟨integral, integral_add, integral_smul⟩
   ⟨1, (λf, le_trans (norm_integral_le_norm _) $ by rw one_mul)⟩
@@ -711,6 +711,144 @@ end simple_func_integral
 
 end simple_func
 
+open simple_func
+
+variables [normed_space ℝ β] [normed_space ℝ γ] [complete_space β]
+
+local notation `to_l1` := coe_to_l1 α β ℝ
+local attribute [instance] simple_func.normed_group simple_func.normed_space
+
+open continuous_linear_map
+
+/-- The Bochner integral in l1 space as a continuous linear map. -/
+def integral_clm : (α →₁ β) →L[ℝ] β :=
+  integral_clm.extend to_l1 simple_func.dense_range simple_func.uniform_inducing
+
+/-- The Bochner integral in l1 space -/
+def integral (f : α →₁ β) : β := (integral_clm).to_fun f
+
+lemma integral_eq (f : α →₁ β) : integral f = (integral_clm).to_fun f := rfl
+
+variables (α β)
+@[simp] lemma integral_zero : integral (0 : α →₁ β) = 0 :=
+map_zero integral_clm
+variables {α β}
+
+lemma integral_add (f g : α →₁ β) : integral (f + g) = integral f + integral g :=
+map_add integral_clm f g
+
+lemma integral_neg (f : α →₁ β) : integral (-f) = - integral f :=
+map_neg integral_clm f
+
+lemma integral_sub (f g : α →₁ β) : integral (f - g) = integral f - integral g :=
+map_sub integral_clm f g
+
+lemma integral_smul (r : ℝ) (f : α →₁ β) : integral (r • f) = r • integral f :=
+map_smul r integral_clm f
+
 end l1
 
+variables [normed_group β] [second_countable_topology β] [normed_space ℝ β] [complete_space β]
+          [normed_group γ] [second_countable_topology γ] [normed_space ℝ γ] [complete_space γ]
+
+/-- The Bochner integral -/
+def integral (f : α → β) : β :=
+if hf : measurable f ∧ integrable f
+then (l1.of_fun f hf.1 hf.2).integral
+else 0
+
+section properties
+
+open continuous_linear_map measure_theory.simple_func
+
+variables {f g : α → β}
+
+lemma integral_eq (f : α → β) : integral f =
+  if hf : measurable f ∧ integrable f then (l1.of_fun f hf.1 hf.2).integral else 0 := rfl
+
+lemma integral_eq_zero_of_non_measurable (h : ¬ measurable f) : integral f = 0 :=
+by { rw [integral, dif_neg], rw not_and_distrib, exact or.inl h }
+
+lemma integral_eq_zero_of_non_integrable (h : ¬ integrable f) : integral f = 0 :=
+by { rw [integral, dif_neg], rw not_and_distrib, exact or.inr h }
+
+variables (α β)
+@[simp] lemma integral_zero : integral (0 : α → β) = 0 :=
+begin
+  simp only [integral], rw dif_pos,
+  { apply l1.integral_zero },
+  { exact ⟨(measurable_const : measurable (λb:α, (0:β))), integrable_zero⟩ }
+end
+variables {α β}
+
+lemma integral_add (hfm : measurable f) (hfi : integrable f) (hgm : measurable g)
+  (hgi : integrable g) : integral (f + g) = integral f + integral g :=
+begin
+  simp only [integral], repeat { rw dif_pos },
+  { rw ← l1.integral_add, refl },
+  { exact ⟨hgm, hgi⟩ },
+  { exact ⟨hfm, hfi⟩ },
+  { exact ⟨measurable_add hfm hgm, integrable_add hfm hgm hfi hgi⟩ }
+end
+
+lemma integral_neg (f : α → β) : integral (-f) = - integral f :=
+begin
+  simp only [integral],
+  by_cases hfm : measurable f, by_cases hfi : integrable f,
+  { repeat { rw dif_pos },
+    { rw ← l1.integral_neg, refl },
+    { exact ⟨hfm, hfi⟩ },
+    { exact ⟨measurable_neg hfm, integrable_neg hfi⟩ } },
+  { repeat { rw dif_neg },
+    { rw neg_zero },
+    { rw not_and_distrib, exact or.inr hfi },
+    { rw not_and_distrib, rw integrable_neg_iff, exact or.inr hfi } },
+  { repeat { rw dif_neg },
+    { rw neg_zero },
+    { rw not_and_distrib, exact or.inl hfm },
+    { rw not_and_distrib, rw measurable_neg_iff, exact or.inl hfm } }
+end
+
+lemma integral_sub (hfm : measurable f) (hfi : integrable f) (hgm : measurable g)
+  (hgi : integrable g) : integral (f - g) = integral f - integral g :=
+begin
+  simp only [integral], repeat {rw dif_pos},
+  { rw ← l1.integral_sub, refl },
+  { exact ⟨hgm, hgi⟩ },
+  { exact ⟨hfm, hfi⟩ },
+  { exact ⟨measurable_sub hfm hgm, integrable_sub hfm hgm hfi hgi⟩ }
+end
+
+lemma integral_smul (r : ℝ) (f : α → β) : integral (λx, r • (f x)) = r • integral f :=
+begin
+  by_cases r0 : r = 0,
+  { have : (λx, r • (f x)) = 0, { funext, rw [r0, zero_smul, pi.zero_apply] },
+    rw [this, r0, zero_smul], apply integral_zero },
+  simp only [integral],
+  by_cases hfm : measurable f, by_cases hfi : integrable f,
+  { rw dif_pos, rw dif_pos,
+    { rw ← l1.integral_smul, refl  },
+    { exact ⟨hfm, hfi⟩ },
+    { exact ⟨measurable_smul _ hfm, integrable_smul _ hfi⟩ } },
+  { repeat { rw dif_neg },
+    { rw smul_zero },
+    { rw not_and_distrib, exact or.inr hfi },
+    { rw not_and_distrib,
+      have : (λx, r • (f x)) = r • f, { funext, simp only [pi.smul_apply] },
+      rw [this, integrable_smul_iff r0], exact or.inr hfi } },
+  { repeat { rw dif_neg },
+    { rw smul_zero },
+    { rw not_and_distrib, exact or.inl hfm },
+    { rw not_and_distrib, rw [measurable_smul_iff r0], exact or.inl hfm, apply_instance } },
+end
+
+end properties
+
+run_cmd mk_simp_attr `integral_simps
+
+attribute [integral_simps] integral_neg integral_smul l1.integral_add l1.integral_sub
+  l1.integral_smul l1.integral_neg
+
+attribute [irreducible] integral l1.integral
+
 end measure_theory

src/measure_theory/borel_space.lean

@@ -209,6 +209,19 @@ lemma measurable_neg
   (hf : measurable f) : measurable (λa, - f a) :=
 (measurable_of_continuous continuous_neg').comp hf
 
+lemma measurable_neg_iff
+  [add_group α] [topological_add_group α] [measurable_space β] (f : β → α) :
+  measurable (-f) ↔ measurable f :=
+iff.intro
+begin
+  assume h,
+  have := measurable_neg h,
+  convert this,
+  funext,
+  simp only [pi.neg_apply, _root_.neg_neg]
+end
+$ measurable_neg
+
 lemma measurable_sub
   [add_group α] [topological_add_group α] [second_countable_topology α] [measurable_space β]
   {f : β → α} {g : β → α} : measurable f → measurable g → measurable (λa, f a - g a) :=
@@ -506,8 +519,23 @@ lemma measurable_smul {α : Type*} {β : Type*} {γ : Type*}
   [semiring α] [topological_space α]
   [topological_space β] [add_comm_monoid β]
   [semimodule α β] [topological_semimodule α β] [measurable_space γ]
-  {c : α} {g : γ → β} (hg : measurable g) : measurable (λ x, c • g x) :=
-measurable.comp (measurable_of_continuous (continuous_smul continuous_const continuous_id)) hg
+  (c : α) {f : γ → β} (hf : measurable f) : measurable (λ x, c • f x) :=
+measurable.comp (measurable_of_continuous (continuous_smul continuous_const continuous_id)) hf
+
+lemma measurable_smul_iff {α : Type*} {β : Type*} {γ : Type*}
+  [division_ring α] [topological_space α]
+  [topological_space β] [add_comm_monoid β]
+  [semimodule α β] [topological_semimodule α β] [measurable_space γ]
+  {c : α} (hc : c ≠ 0) (f : γ → β) : measurable (λ x, c • f x) ↔ measurable f :=
+iff.intro
+begin
+  assume h,
+  have eq : (λ (x : γ), c⁻¹ • (λ (x : γ), c • f x) x) = f,
+  { funext, rw [smul_smul, inv_mul_cancel hc, one_smul] },
+  have := measurable_smul c⁻¹ h,
+  rwa eq at this
+end
+$ measurable_smul c
 
 lemma measurable_dist' {α : Type*} [metric_space α] [second_countable_topology α] :
   measurable (λp:α×α, dist p.1 p.2) :=

src/measure_theory/l1_space.lean

@@ -142,6 +142,15 @@ lemma integrable_neg {f : α → β} : integrable f → integrable (-f) :=
 assume hfi, calc _ = _ : lintegral_nnnorm_neg
                  ... < ⊤ : hfi
 
+lemma integrable_neg_iff (f : α → β) : integrable (-f) ↔ integrable f :=
+begin
+  split,
+  { assume h,
+    have := integrable_neg h,
+    rwa _root_.neg_neg at this },
+  exact integrable_neg
+end
+
 lemma integrable_sub {f g : α → β} (hf : measurable f) (hg : measurable g) :
   integrable f → integrable g → integrable (f - g) :=
 λ hfi hgi,
@@ -175,6 +184,15 @@ begin
     end
 end
 
+lemma integrable_smul_iff {c : 𝕜} (hc : c ≠ 0) (f : α → β) : integrable (c • f) ↔ integrable f :=
+begin
+  split,
+  { assume h,
+    have := integrable_smul c⁻¹ h,
+    rwa [smul_smul, inv_mul_cancel hc, one_smul] at this },
+  exact integrable_smul _
+end
+
 end normed_space
 
 variables [second_countable_topology β]
@@ -331,7 +349,7 @@ rfl
 variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β]
 
 lemma of_fun_smul (f : α → β) (hfm hfi) (k : 𝕜) :
-  of_fun (k • f) (measurable_smul hfm) (integrable_smul _ hfi) = k • of_fun f hfm hfi := rfl
+  of_fun (k • f) (measurable_smul _ hfm) (integrable_smul _ hfi) = k • of_fun f hfm hfi := rfl
 
 end of_fun