Theorem bounded_continuous_function.to_Lp_norm_le
Modification history
2023-01-08 13:02
src/measure_theory/function/lp_space.lean
feat(analysis/fourier): convergence of Fourier series (#17913) …
Modified bounded_continuous_function.to_Lp_norm_leView on Github →2022-07-23 17:07
src/measure_theory/function/lp_space.lean
refactor(*): rename `nondiscrete_normed_field` (#15625) …
Modified bounded_continuous_function.to_Lp_norm_leView on Github →