Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-24 10:50 49c53d4f

View on Github →

feat(measure_theory/lp_space): define Lp, subtype of ae_eq_fun with finite norm (#5853)

Estimated changes

Modified docs/undergrad.yaml

Modified src/measure_theory/lp_space.lean

added theorem measure_theory.Lp.ae_measurable

added theorem measure_theory.Lp.antimono

added theorem measure_theory.Lp.coe_fn_add

added theorem measure_theory.Lp.coe_fn_mk

added theorem measure_theory.Lp.coe_fn_neg

added theorem measure_theory.Lp.coe_fn_smul

added theorem measure_theory.Lp.coe_fn_sub

added theorem measure_theory.Lp.coe_fn_zero

added theorem measure_theory.Lp.measurable

added theorem measure_theory.Lp.mem_Lp_const

added theorem measure_theory.Lp.mem_Lp_const_smul

added theorem measure_theory.Lp.mem_Lp_iff_snorm_lt_top

added theorem measure_theory.Lp.mem_ℒp

added theorem measure_theory.Lp.norm_const_smul

added theorem measure_theory.Lp.norm_def

added theorem measure_theory.Lp.norm_eq_zero_iff

added theorem measure_theory.Lp.norm_neg

added theorem measure_theory.Lp.norm_zero

added theorem measure_theory.Lp.snorm_lt_top

added theorem measure_theory.Lp.snorm_ne_top

added def measure_theory.Lp

added theorem measure_theory.ae_eq_zero_of_snorm'_eq_zero

added theorem measure_theory.coe_nnnorm_ae_le_snorm_ess_sup

added theorem measure_theory.lintegral_rpow_nnnorm_eq_rpow_snorm'

added theorem measure_theory.lintegral_rpow_nnnorm_lt_top_of_snorm'_lt_top

added theorem measure_theory.mem_ℒp.add

added theorem measure_theory.mem_ℒp.ae_eq

added theorem measure_theory.mem_ℒp.coe_fn_to_Lp

added theorem measure_theory.mem_ℒp.const_smul

added theorem measure_theory.mem_ℒp.integrable

added theorem measure_theory.mem_ℒp.mem_ℒp_of_exponent_le

added theorem measure_theory.mem_ℒp.neg

added theorem measure_theory.mem_ℒp.snorm_lt_top

added theorem measure_theory.mem_ℒp.snorm_mk_lt_top

added theorem measure_theory.mem_ℒp.snorm_ne_top

added theorem measure_theory.mem_ℒp.sub

added def measure_theory.mem_ℒp.to_Lp

added def measure_theory.mem_ℒp

added theorem measure_theory.mem_ℒp_congr_ae

added theorem measure_theory.mem_ℒp_const

added theorem measure_theory.mem_ℒp_one_iff_integrable

added theorem measure_theory.mem_ℒp_zero_iff_ae_measurable

added def measure_theory.snorm'

added theorem measure_theory.snorm'_add_le

added theorem measure_theory.snorm'_add_lt_top_of_le_one

added theorem measure_theory.snorm'_congr_ae

added theorem measure_theory.snorm'_const'

added theorem measure_theory.snorm'_const

added theorem measure_theory.snorm'_const_of_probability_measure

added theorem measure_theory.snorm'_const_smul

added theorem measure_theory.snorm'_eq_zero_iff

added theorem measure_theory.snorm'_eq_zero_of_ae_zero'

added theorem measure_theory.snorm'_eq_zero_of_ae_zero

added theorem measure_theory.snorm'_exponent_zero

added theorem measure_theory.snorm'_le_snorm'_mul_rpow_measure_univ

added theorem measure_theory.snorm'_le_snorm'_of_exponent_le

added theorem measure_theory.snorm'_le_snorm_ess_sup

added theorem measure_theory.snorm'_le_snorm_ess_sup_mul_rpow_measure_univ

added theorem measure_theory.snorm'_lt_top_of_snorm'_lt_top_of_exponent_le

added theorem measure_theory.snorm'_measure_zero_of_exponent_zero

added theorem measure_theory.snorm'_measure_zero_of_neg

added theorem measure_theory.snorm'_measure_zero_of_pos

added theorem measure_theory.snorm'_neg

added theorem measure_theory.snorm'_smul_le_mul_snorm'

added theorem measure_theory.snorm'_zero'

added theorem measure_theory.snorm'_zero

added def measure_theory.snorm

added theorem measure_theory.snorm_add_le

added theorem measure_theory.snorm_add_lt_top

added theorem measure_theory.snorm_add_lt_top_of_one_le

added theorem measure_theory.snorm_ae_eq_fun

added theorem measure_theory.snorm_congr_ae

added theorem measure_theory.snorm_const'

added theorem measure_theory.snorm_const

added theorem measure_theory.snorm_const_smul

added theorem measure_theory.snorm_eq_snorm'

added theorem measure_theory.snorm_eq_zero_iff

added def measure_theory.snorm_ess_sup

added theorem measure_theory.snorm_ess_sup_add_le

added theorem measure_theory.snorm_ess_sup_congr_ae

added theorem measure_theory.snorm_ess_sup_const

added theorem measure_theory.snorm_ess_sup_const_smul

added theorem measure_theory.snorm_ess_sup_eq_zero_iff

added theorem measure_theory.snorm_ess_sup_measure_zero

added theorem measure_theory.snorm_ess_sup_zero

added theorem measure_theory.snorm_exponent_top

added theorem measure_theory.snorm_exponent_zero

added theorem measure_theory.snorm_le_snorm_of_exponent_le

added theorem measure_theory.snorm_measure_zero

added theorem measure_theory.snorm_neg

added theorem measure_theory.snorm_zero

added theorem measure_theory.zero_mem_ℒp

deleted theorem ℒp_space.ae_eq_zero_of_snorm'_eq_zero

deleted theorem ℒp_space.coe_nnnorm_ae_le_snorm_ess_sup

deleted theorem ℒp_space.lintegral_rpow_nnnorm_eq_rpow_snorm'

deleted theorem ℒp_space.lintegral_rpow_nnnorm_lt_top_of_snorm'_lt_top

deleted theorem ℒp_space.mem_ℒp.add

deleted theorem ℒp_space.mem_ℒp.ae_eq

deleted theorem ℒp_space.mem_ℒp.const_smul

deleted theorem ℒp_space.mem_ℒp.integrable

deleted theorem ℒp_space.mem_ℒp.mem_ℒp_of_exponent_le

deleted theorem ℒp_space.mem_ℒp.neg

deleted theorem ℒp_space.mem_ℒp.snorm_lt_top

deleted theorem ℒp_space.mem_ℒp.snorm_ne_top

deleted theorem ℒp_space.mem_ℒp.sub

deleted def ℒp_space.mem_ℒp

deleted theorem ℒp_space.mem_ℒp_congr_ae

deleted theorem ℒp_space.mem_ℒp_const

deleted theorem ℒp_space.mem_ℒp_one_iff_integrable

deleted theorem ℒp_space.mem_ℒp_zero_iff_ae_measurable

deleted def ℒp_space.snorm'

deleted theorem ℒp_space.snorm'_add_le

deleted theorem ℒp_space.snorm'_add_lt_top_of_le_one

deleted theorem ℒp_space.snorm'_congr_ae

deleted theorem ℒp_space.snorm'_const'

deleted theorem ℒp_space.snorm'_const

deleted theorem ℒp_space.snorm'_const_of_probability_measure

deleted theorem ℒp_space.snorm'_const_smul

deleted theorem ℒp_space.snorm'_eq_zero_iff

deleted theorem ℒp_space.snorm'_eq_zero_of_ae_zero'

deleted theorem ℒp_space.snorm'_eq_zero_of_ae_zero

deleted theorem ℒp_space.snorm'_exponent_zero

deleted theorem ℒp_space.snorm'_le_snorm'_mul_rpow_measure_univ

deleted theorem ℒp_space.snorm'_le_snorm'_of_exponent_le

deleted theorem ℒp_space.snorm'_le_snorm_ess_sup

deleted theorem ℒp_space.snorm'_le_snorm_ess_sup_mul_rpow_measure_univ

deleted theorem ℒp_space.snorm'_lt_top_of_snorm'_lt_top_of_exponent_le

deleted theorem ℒp_space.snorm'_measure_zero_of_exponent_zero

deleted theorem ℒp_space.snorm'_measure_zero_of_neg

deleted theorem ℒp_space.snorm'_measure_zero_of_pos

deleted theorem ℒp_space.snorm'_neg

deleted theorem ℒp_space.snorm'_smul_le_mul_snorm'

deleted theorem ℒp_space.snorm'_zero'

deleted theorem ℒp_space.snorm'_zero

deleted def ℒp_space.snorm

deleted theorem ℒp_space.snorm_add_le

deleted theorem ℒp_space.snorm_add_lt_top

deleted theorem ℒp_space.snorm_add_lt_top_of_one_le

deleted theorem ℒp_space.snorm_congr_ae

deleted theorem ℒp_space.snorm_const'

deleted theorem ℒp_space.snorm_const

deleted theorem ℒp_space.snorm_const_smul

deleted theorem ℒp_space.snorm_eq_snorm'

deleted theorem ℒp_space.snorm_eq_zero_iff

deleted def ℒp_space.snorm_ess_sup

deleted theorem ℒp_space.snorm_ess_sup_add_le

deleted theorem ℒp_space.snorm_ess_sup_congr_ae

deleted theorem ℒp_space.snorm_ess_sup_const

deleted theorem ℒp_space.snorm_ess_sup_const_smul

deleted theorem ℒp_space.snorm_ess_sup_eq_zero_iff

deleted theorem ℒp_space.snorm_ess_sup_measure_zero

deleted theorem ℒp_space.snorm_ess_sup_zero

deleted theorem ℒp_space.snorm_exponent_top

deleted theorem ℒp_space.snorm_exponent_zero

deleted theorem ℒp_space.snorm_le_snorm_of_exponent_le

deleted theorem ℒp_space.snorm_measure_zero

deleted theorem ℒp_space.snorm_neg

deleted theorem ℒp_space.snorm_zero

deleted theorem ℒp_space.zero_mem_ℒp