refactor(measure_theory/simple_func_dense): generalize L1.simple_func.dense_embedding to Lp (#8209)

This PR generalizes all the more abstract results about approximation by simple functions, from L1 to Lp (`p ≠ ∞`).  Notably, this includes 
* the definition `Lp.simple_func`, the `add_subgroup` of `Lp` of classes containing a simple representative
* the coercion `Lp.simple_func.coe_to_Lp` from this subgroup to `Lp`, as a continuous linear map
* `Lp.simple_func.dense_embedding`, this subgroup is dense in `Lp`
* `mem_ℒp.induction`, to prove a predicate holds for `mem_ℒp` functions it suffices to prove that it behaves appropriately on `mem_ℒp` simple functions

Many lemmas get renamed from `L1.simple_func.*` to `Lp.simple_func.*`, and have hypotheses or conclusions changed from `integrable` to `mem_ℒp`.

I take the opportunity to streamline the construction by deleting some instances which typeclass inference can find, and some lemmas which are re-statements of more general results about `add_subgroup`s in normed groups.  In my opinion, this extra material obscures the structure of the construction.  Here is a list of the definitions deleted:
- `instance : has_coe (α →₁ₛ[μ] E) (α →₁[μ] E)`
- `instance : has_coe_to_fun (α →₁ₛ[μ] E)`
- `instance : inhabited (α →₁ₛ[μ] E)`
- `protected def normed_group : normed_group (α →₁ₛ[μ] E)`

and lemmas deleted (in the `L1.simple_func` namespace unless specified):
- `simple_func.tendsto_approx_on_univ_L1`
- `eq`
- `eq_iff`
- `eq_iff'`
- `coe_zero`
- `coe_add`
- `coe_neg`
- `coe_sub`
- `edist_eq`
- `dist_eq`
- `norm_eq`
- `lintegral_edist_to_simple_func_lt_top`
- `dist_to_simple_func`

Author: hrmacbeth

src/group_theory/subgroup.lean

@@ -313,6 +313,7 @@ instance has_div : has_div H := ⟨λ a b, ⟨a / b, H.div_mem a.2 b.2⟩⟩
 @[simp, norm_cast, to_additive] lemma coe_mul (x y : H) : (↑(x * y) : G) = ↑x * ↑y := rfl
 @[simp, norm_cast, to_additive] lemma coe_one : ((1 : H) : G) = 1 := rfl
 @[simp, norm_cast, to_additive] lemma coe_inv (x : H) : ↑(x⁻¹ : H) = (x⁻¹ : G) := rfl
+@[simp, norm_cast, to_additive] lemma coe_div (x y : H) : (↑(x / y) : G) = ↑x / ↑y := rfl
 @[simp, norm_cast, to_additive] lemma coe_mk (x : G) (hx : x ∈ H) : ((⟨x, hx⟩ : H) : G) = x := rfl
 
 attribute [norm_cast] add_subgroup.coe_add add_subgroup.coe_zero

src/measure_theory/bochner_integration.lean

@@ -140,6 +140,8 @@ noncomputable theory
 open_locale classical topological_space big_operators nnreal ennreal measure_theory
 open set filter topological_space ennreal emetric
 
+local attribute [instance] fact_one_le_one_ennreal
+
 namespace measure_theory
 
 variables {α E F 𝕜 : Type*} [measurable_space α]
@@ -370,7 +372,7 @@ end simple_func
 
 namespace L1
 
-open ae_eq_fun
+open ae_eq_fun Lp.simple_func Lp
 
 variables
   [normed_group E] [second_countable_topology E] [measurable_space E] [borel_space E]
@@ -384,7 +386,7 @@ namespace simple_func
 lemma norm_eq_integral (f : α →₁ₛ[μ] E) : ∥f∥ = ((to_simple_func f).map norm).integral μ :=
 begin
   rw [norm_to_simple_func, simple_func.integral_eq_lintegral],
-  { simp only [simple_func.map_apply, of_real_norm_eq_coe_nnnorm] },
+  { simp only [simple_func.map_apply, of_real_norm_eq_coe_nnnorm, snorm_one_eq_lintegral_nnnorm] },
   { exact (simple_func.integrable f).norm },
   { exact eventually_of_forall (λ x, norm_nonneg _) }
 end
@@ -420,7 +422,7 @@ and prove basic properties of this integral. -/
 
 variables [normed_field 𝕜] [normed_space 𝕜 E] [normed_space ℝ E] [smul_comm_class ℝ 𝕜 E]
 
-local attribute [instance] simple_func.normed_group simple_func.normed_space
+local attribute [instance] simple_func.normed_space
 
 /-- The Bochner integral over simple functions in L1 space. -/
 def integral (f : α →₁ₛ[μ] E) : E := ((to_simple_func f)).integral μ
@@ -487,7 +489,7 @@ begin
   { filter_upwards [to_simple_func_eq_to_fun (pos_part f), Lp.coe_fn_pos_part (f : α →₁[μ] ℝ),
       to_simple_func_eq_to_fun f],
     assume a h₁ h₂ h₃,
-    rw [h₁, ← coe_coe, coe_pos_part, h₂, coe_coe, ← h₃] },
+    convert h₂ },
   refine ae_eq.mono (assume a h, _),
   rw [h, eq]
 end
@@ -554,16 +556,15 @@ variables [normed_space ℝ E] [nondiscrete_normed_field 𝕜] [normed_space 
 
 section integration_in_L1
 
-local notation `to_L1` := coe_to_L1 α E ℝ
-local attribute [instance] simple_func.normed_group simple_func.normed_space
+local attribute [instance] simple_func.normed_space
 
 open continuous_linear_map
 
 variables (𝕜) [measurable_space 𝕜] [opens_measurable_space 𝕜]
 /-- The Bochner integral in L1 space as a continuous linear map. -/
 def integral_clm' : (α →₁[μ] E) →L[𝕜] E :=
 (integral_clm' α E 𝕜 μ).extend
-  (coe_to_L1 α E 𝕜) simple_func.dense_range simple_func.uniform_inducing
+  (coe_to_Lp α E 𝕜) (simple_func.dense_range one_ne_top) simple_func.uniform_inducing
 
 variables {𝕜}
 
@@ -577,7 +578,7 @@ lemma integral_eq (f : α →₁[μ] E) : integral f = integral_clm f := rfl
 
 @[norm_cast] lemma simple_func.integral_L1_eq_integral (f : α →₁ₛ[μ] E) :
   integral (f : α →₁[μ] E) = (simple_func.integral f) :=
-uniformly_extend_of_ind simple_func.uniform_inducing simple_func.dense_range
+uniformly_extend_of_ind simple_func.uniform_inducing (simple_func.dense_range one_ne_top)
   (simple_func.integral_clm α E μ).uniform_continuous _
 
 variables (α E)
@@ -626,15 +627,15 @@ begin
   -- Use `is_closed_property` and `is_closed_eq`
   refine @is_closed_property _ _ _ (coe : (α →₁ₛ[μ] ℝ) → (α →₁[μ] ℝ))
     (λ f : α →₁[μ] ℝ, integral f = ∥Lp.pos_part f∥ - ∥Lp.neg_part f∥)
-    L1.simple_func.dense_range (is_closed_eq _ _) _ f,
+    (simple_func.dense_range one_ne_top) (is_closed_eq _ _) _ f,
   { exact cont _ },
   { refine continuous.sub (continuous_norm.comp Lp.continuous_pos_part)
       (continuous_norm.comp Lp.continuous_neg_part) },
   -- Show that the property holds for all simple functions in the `L¹` space.
   { assume s,
     norm_cast,
-    rw [← simple_func.norm_eq, ← simple_func.norm_eq],
-    exact simple_func.integral_eq_norm_pos_part_sub _}
+    rw [← coe_norm_subgroup, ← coe_norm_subgroup],
+    exact simple_func.integral_eq_norm_pos_part_sub _ }
 end
 
 end pos_part
@@ -1107,9 +1108,9 @@ end
 lemma simple_func.integral_eq_integral (f : α →ₛ E) (hfi : integrable f μ) :
   f.integral μ = ∫ x, f x ∂μ :=
 begin
-  rw [integral_eq f hfi, ← L1.simple_func.to_L1_eq_to_L1,
+  rw [integral_eq f hfi, ← L1.simple_func.to_Lp_one_eq_to_L1,
     L1.simple_func.integral_L1_eq_integral, L1.simple_func.integral_eq_integral],
-  exact simple_func.integral_congr hfi (L1.simple_func.to_simple_func_to_L1 _ _).symm
+  exact simple_func.integral_congr hfi (Lp.simple_func.to_simple_func_to_Lp _ _).symm
 end
 
 lemma simple_func.integral_eq_sum (f : α →ₛ E) (hfi : integrable f μ) :

src/measure_theory/integrable_on.lean

@@ -262,7 +262,7 @@ alias measure.finite_at_filter.integrable_at_filter_of_tendsto ← filter.tendst
 
 variables [borel_space E] [second_countable_topology E]
 
-lemma integrable_add [opens_measurable_space E] {f g : α → E}
+lemma integrable_add_of_disjoint {f g : α → E}
   (h : disjoint (support f) (support g)) (hf : measurable f) (hg : measurable g) :
   integrable (f + g) μ ↔ integrable f μ ∧ integrable g μ :=
 begin

src/measure_theory/lp_space.lean

@@ -1339,6 +1339,20 @@ begin
   exact le_rfl,
 end
 
+variables (hs)
+
+lemma snorm_indicator_le {E : Type*} [normed_group E] (f : α → E) :
+  snorm (s.indicator f) p μ ≤ snorm f p μ :=
+begin
+  refine snorm_mono_ae (eventually_of_forall (λ x, _)),
+  suffices : ∥s.indicator f x∥₊ ≤ ∥f x∥₊,
+  { exact nnreal.coe_mono this },
+  rw nnnorm_indicator_eq_indicator_nnnorm,
+  exact s.indicator_le_self _ x,
+end
+
+variables {hs}
+
 lemma snorm_indicator_const {c : G} (hs : measurable_set s) (hp : p ≠ 0) (hp_top : p ≠ ∞) :
   snorm (s.indicator (λ x, c)) p μ = ∥c∥₊ * (μ s) ^ (1 / p.to_real) :=
 begin
@@ -1363,6 +1377,10 @@ begin
   { exact snorm_indicator_const hs hp hp_top, },
 end
 
+lemma mem_ℒp.indicator (hs : measurable_set s) (hf : mem_ℒp f p μ) :
+  mem_ℒp (s.indicator f) p μ :=
+⟨hf.ae_measurable.indicator hs, lt_of_le_of_lt (snorm_indicator_le f) hf.snorm_lt_top⟩
+
 lemma mem_ℒp_indicator_const (p : ℝ≥0∞) (hs : measurable_set s) (c : E) (hμsc : c = 0 ∨ μ s ≠ ∞) :
   mem_ℒp (s.indicator (λ _, c)) p μ :=
 begin
@@ -1390,6 +1408,9 @@ end
 end indicator
 
 section indicator_const_Lp
+
+open set function
+
 variables {s : set α} {hs : measurable_set s} {hμs : μ s ≠ ∞} {c : E}
   [borel_space E] [second_countable_topology E]
 
@@ -1428,6 +1449,15 @@ begin
   { exact norm_indicator_const_Lp hp_pos hp_top, },
 end
 
+lemma mem_ℒp_add_of_disjoint {f g : α → E}
+  (h : disjoint (support f) (support g)) (hf : measurable f) (hg : measurable g) :
+  mem_ℒp (f + g) p μ ↔ mem_ℒp f p μ ∧ mem_ℒp g p μ :=
+begin
+  refine ⟨λ hfg, ⟨_, _⟩, λ h, h.1.add h.2⟩,
+  { rw ← indicator_add_eq_left h, exact hfg.indicator (measurable_set_support hf) },
+  { rw ← indicator_add_eq_right h, exact hfg.indicator (measurable_set_support hg) }
+end
+
 /-- The indicator of a disjoint union of two sets is the sum of the indicators of the sets. -/
 lemma indicator_const_Lp_disjoint_union {s t : set α} (hs : measurable_set s)
   (ht : measurable_set t) (hμs : μ s ≠ ∞) (hμt : μ t ≠ ∞) (hst : s ∩ t = ∅) (c : E) :