Mathlib v3 is deprecated. Go to Mathlib v4

Theorem integral_inner

Modification history

2023-05-15 16:30
src/measure_theory/function/l2_space.lean
chore(measure_theory/{integral/set_integral,function/*}): split out inner product space material (#19019) …
Modified integral_innerView on Github →
2021-07-13 07:09
src/measure_theory/set_integral.lean
feat(measure_theory/l2_space): the inner product of indicator_const_Lp and a function is the set_integral (#8229)
Added integral_innerView on Github →