Commit 2021-03-14 03:22 d61d8bfe

View on Github →

feat(measure_theory/bochner_integration): extend the integral_smul lemmas (#6654) Extend the integral_smul lemmas to multiplication of a function f : α → E with scalars in 𝕜 with [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [smul_comm_class ℝ 𝕜 E] instead of only ℝ.

Estimated changes

Modified src/measure_theory/bochner_integration.lean

added def measure_theory.L1.integral_clm'

modified def measure_theory.L1.integral_clm

modified theorem measure_theory.L1.integral_smul

added def measure_theory.L1.simple_func.integral_clm'

modified def measure_theory.L1.simple_func.integral_clm

modified theorem measure_theory.L1.simple_func.integral_smul

modified theorem measure_theory.integral_smul

modified theorem measure_theory.simple_func.integral_smul