Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-12 08:19 85c6a799

View on Github →

feat(measure_theory/lp_space): Lp is complete (#6563) Prove the completeness of Lp by showing that Cauchy sequences of ℒp have a limit.

Estimated changes

Modified docs/undergrad.yaml

Modified src/measure_theory/ess_sup.lean

added theorem ennreal.ess_sup_liminf_le

Modified src/measure_theory/lp_space.lean

added theorem measure_theory.Lp.ae_tendsto_of_cauchy_snorm'

added theorem measure_theory.Lp.ae_tendsto_of_cauchy_snorm

added theorem measure_theory.Lp.cauchy_complete_ℒp

added theorem measure_theory.Lp.cauchy_tendsto_of_tendsto

added theorem measure_theory.Lp.complete_space_Lp_of_cauchy_complete_ℒp

added theorem measure_theory.Lp.mem_ℒp_of_cauchy_tendsto

added theorem measure_theory.Lp.snorm'_lim_eq_lintegral_liminf

added theorem measure_theory.Lp.snorm'_lim_le_liminf_snorm'

added theorem measure_theory.Lp.snorm_exponent_top_lim_eq_ess_sup_liminf

added theorem measure_theory.Lp.snorm_exponent_top_lim_le_liminf_snorm_exponent_top

added theorem measure_theory.Lp.snorm_lim_le_liminf_snorm

added theorem measure_theory.Lp.tendsto_Lp_of_tendsto_ℒp

added theorem measure_theory.snorm'_norm

Modified src/order/filter/ennreal.lean

added theorem ennreal.limsup_liminf_le_liminf_limsup

Modified src/topology/instances/ennreal.lean