Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-10 00:03 49e50ee5

View on Github →

feat(measure_theory/lp_space): add more API on Lp spaces (#6042) Flesh out the file on L^p spaces, notably adding facts on the composition with Lipschitz functions. This makes it possible to define in one go the positive part of an L^p function, and its image under a continuous linear map. The file ae_eq_fun.lean is split into two, to solve a temporary issue: this file defines a global emetric space instance (of L^1 type) on the space of function classes. This passes to subtypes, and clashes with the topology on L^p coming from the distance. This did not show up before as there were not enough topological statements on L^p, but I have been bitten by this when adding new results. For now, we move this part of ae_eq_fun.lean to another file which is not imported by lp_space.lean, to avoid the clash. This will be solved in a subsequent PR in which I will remove the global instance, and construct the integral based on the specialization of L^p to p = 1 instead of the ad hoc construction we have now (note that, currently, we have two different L^1 spaces in mathlib, denoted Lp E 1 μ and α →₁[μ] E -- I will remove the second one in a later PR).

Estimated changes

modified theorem measure_theory.Lp.coe_fn_mk
added theorem measure_theory.Lp.ext
modified theorem measure_theory.mem_ℒp.add
modified theorem measure_theory.mem_ℒp.neg
modified theorem measure_theory.mem_ℒp.sub
modified def measure_theory.snorm'
modified theorem measure_theory.snorm'_const
modified theorem measure_theory.snorm'_neg
modified theorem measure_theory.snorm'_zero'
modified theorem measure_theory.snorm'_zero
modified def measure_theory.snorm
modified theorem measure_theory.snorm_add_le
modified theorem measure_theory.snorm_const'
modified theorem measure_theory.snorm_const
modified theorem measure_theory.snorm_neg
modified theorem measure_theory.snorm_zero