Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-15 14:54 f4991b97

View on Github →

feat(measure_theory/bochner_integration): properties of simple functions (mem_Lp, integrable, fin_meas_supp) (#7918)

Estimated changes

Modified src/measure_theory/bochner_integration.lean

added theorem measure_theory.simple_func.exists_forall_norm_le

added theorem measure_theory.simple_func.integrable_iff

modified theorem measure_theory.simple_func.integrable_iff_fin_meas_supp

added theorem measure_theory.simple_func.integrable_of_finite_measure

added theorem measure_theory.simple_func.measure_preimage_lt_top_of_integrable

added theorem measure_theory.simple_func.measure_preimage_lt_top_of_mem_ℒp

added theorem measure_theory.simple_func.mem_ℒp_iff

added theorem measure_theory.simple_func.mem_ℒp_iff_fin_meas_supp

added theorem measure_theory.simple_func.mem_ℒp_iff_integrable

added theorem measure_theory.simple_func.mem_ℒp_of_finite_measure

added theorem measure_theory.simple_func.mem_ℒp_of_finite_measure_preimage

added theorem measure_theory.simple_func.mem_ℒp_top

added theorem measure_theory.simple_func.mem_ℒp_zero

Modified src/measure_theory/lp_space.lean

added theorem measure_theory.mem_ℒp_top_of_bound

added theorem measure_theory.snorm_ess_sup_le_of_ae_bound

added theorem measure_theory.snorm_ess_sup_lt_top_of_ae_bound