Commit 2023-01-08 09:48 7c60702a

View on Github →

feat(measure_theory/integral): "integral_prod_mul" for complex coefficients (#18085) This generalises some lemmas in the integration library, currently only stated for ℝ-valued functions, to allow complex-valued functions too. (Note that one can't generalise all the way to an arbitrary Banach algebra, there are problems when one side is integrable and the other isn't.)

Estimated changes

Modified src/measure_theory/constructions/prod.lean

modified theorem measure_theory.integrable_prod_mul

modified theorem measure_theory.integral_prod_mul

modified theorem measure_theory.set_integral_prod_mul

Modified src/measure_theory/function/l1_space.lean

modified theorem measure_theory.integrable.bdd_mul'

modified theorem measure_theory.integrable.const_mul'

modified theorem measure_theory.integrable.const_mul

modified theorem measure_theory.integrable.div_const

modified theorem measure_theory.integrable.mul_const'

modified theorem measure_theory.integrable.mul_const

Modified src/measure_theory/integral/bochner.lean

modified theorem measure_theory.integral_div

modified theorem measure_theory.integral_mul_left

modified theorem measure_theory.integral_mul_right

Modified src/probability/variance.lean