Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-28 19:54 a17f38f2

View on Github →

feat(measure_theory/lp_space): bounded continuous functions are in Lp (#6878) Under appropriate conditions (finite Borel measure, second-countable), a bounded continuous function is in L^p. The main result of this PR is bounded_continuous_function.to_Lp, which provides this operation as a bounded linear map. There are also several variations.

Estimated changes

Modified src/data/real/ennreal.lean

added theorem ennreal.to_real_le_coe_of_le_coe

Modified src/measure_theory/ae_eq_fun.lean

added theorem continuous_map.coe_fn_to_ae_eq_fun

added def continuous_map.to_ae_eq_fun

added def continuous_map.to_ae_eq_fun_linear_map

added def continuous_map.to_ae_eq_fun_mul_hom

Modified src/measure_theory/lp_space.lean

added theorem bounded_continuous_function.Lp_norm_le

added theorem bounded_continuous_function.mem_Lp

added def bounded_continuous_function.to_Lp

added def bounded_continuous_function.to_Lp_hom

added theorem bounded_continuous_function.to_Lp_norm_le

added def measure_theory.Lp.Lp_submodule

added theorem measure_theory.Lp.coe_Lp_submodule

added theorem measure_theory.Lp.mem_Lp_of_ae_bound

added theorem measure_theory.Lp.norm_le_of_ae_bound

added theorem measure_theory.mem_ℒp.of_bound

added theorem measure_theory.snorm_le_of_ae_bound

Modified src/measure_theory/measure_space.lean

added theorem measure_theory.coe_measure_univ_nnreal

added def measure_theory.measure_univ_nnreal

added theorem measure_theory.measure_univ_nnreal_eq_zero

added theorem measure_theory.measure_univ_nnreal_pos

added theorem measure_theory.measure_univ_nnreal_zero

Modified src/topology/continuous_function/bounded.lean

added def bounded_continuous_function.forget_boundedness_linear_map