Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-12 15:02 e17e9eac

View on Github →

feat(measure_theory/lp_space): add mem_Lp and integrable lemmas for is_R_or_C.re/im and inner product with a constant (#8615)

Estimated changes

Modified src/data/complex/is_R_or_C.lean

added theorem is_R_or_C.norm_im_le_norm

added theorem is_R_or_C.norm_re_le_norm

Modified src/measure_theory/function/l1_space.lean

added theorem measure_theory.integrable.const_inner

added theorem measure_theory.integrable.im

added theorem measure_theory.integrable.inner_const

added theorem measure_theory.integrable.re

Modified src/measure_theory/function/lp_space.lean

added theorem measure_theory.mem_ℒp.const_inner

added theorem measure_theory.mem_ℒp.im

added theorem measure_theory.mem_ℒp.inner_const

added theorem measure_theory.mem_ℒp.re