Commit 2021-07-12 21:10 4cd6179c

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_subgroups 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