mathlib

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

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`