Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-13 07:09 f302c979

View on Github →

feat(measure_theory/l2_space): the inner product of indicator_const_Lp and a function is the set_integral (#8229)

Estimated changes

Modified src/measure_theory/integrable_on.lean

added theorem measure_theory.integrable_on_Lp_of_measure_ne_top

Modified src/measure_theory/l2_space.lean

added theorem measure_theory.L2.inner_indicator_const_Lp_eq_inner_set_integral

added theorem measure_theory.L2.inner_indicator_const_Lp_eq_set_integral_inner

added theorem measure_theory.L2.inner_indicator_const_Lp_one

Modified src/measure_theory/set_integral.lean

added theorem integral_eq_zero_of_forall_integral_inner_eq_zero

added theorem integral_inner