Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-13 19:37 e33245ca

View on Github →

feat(topology/metric_space/pi_Lp): L^p distance on finite products (#3059) L^p edistance (or distance, or norm) on finite products of emetric spaces (or metric spaces, or normed groups), put on a type synonym pi_Lp p hp α to avoid instance clashes, and being careful to register as uniformity the product uniformity.

Estimated changes

Modified src/analysis/special_functions/pow.lean

added theorem ennreal.mul_rpow_of_nonneg

modified theorem ennreal.rpow_eq_top_iff

modified theorem ennreal.rpow_eq_zero_iff

added theorem ennreal.to_real_rpow

modified theorem ennreal.top_rpow_of_neg

modified theorem ennreal.top_rpow_of_pos

modified theorem ennreal.zero_rpow_of_neg

modified theorem ennreal.zero_rpow_of_pos

added theorem nnreal.rpow_neg_one

Created src/topology/metric_space/pi_Lp.lean

added theorem pi_Lp.add_apply

added theorem pi_Lp.antilipschitz_with_equiv

added theorem pi_Lp.aux_uniformity_eq

added def pi_Lp.emetric_aux

added theorem pi_Lp.lipschitz_with_equiv

added theorem pi_Lp.neg_apply

added theorem pi_Lp.norm_eq

added theorem pi_Lp.smul_apply

added theorem pi_Lp.sub_apply

added def pi_Lp