Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-17 13:13 17ef379e

View on Github →

refactor(analysis): change the symbol for norm to align with the unicode spec (#17575) The characters in question are:

  • U+2016 DOUBLE VERTICAL LINE . The Unicode Character Database says "used in pairs to indicate norm of a matrix", for instance here and here
  • U+2225 PARALLEL TO . On some platforms this renders with a forward slant! Previously norm was the latter and parallel was the former. This change swaps them around:
  • ∥x∥, S ‖ T: before
  • ‖x‖, S ∥ T: after Code using U+2016 for fintype cardinality has been left unchanged.

Estimated changes

modified theorem asymptotics.is_O.bound
modified theorem asymptotics.is_O.of_bound'
modified theorem asymptotics.is_O.of_bound
modified theorem asymptotics.is_O.trans_le
modified theorem asymptotics.is_O_iff
modified theorem asymptotics.is_O_norm_left
modified theorem asymptotics.is_O_norm_norm
modified theorem asymptotics.is_O_norm_right
modified theorem asymptotics.is_O_of_le'
modified theorem asymptotics.is_O_of_le
modified theorem asymptotics.is_O_one_iff
modified theorem asymptotics.is_O_principal
modified theorem asymptotics.is_O_top
modified theorem asymptotics.is_O_with_iff
modified theorem asymptotics.is_O_with_inv
modified theorem asymptotics.is_O_with_of_le
modified theorem asymptotics.is_O_with_pure
modified theorem asymptotics.is_O_with_top
modified theorem asymptotics.is_o.def
modified theorem asymptotics.is_o.trans_le
modified theorem asymptotics.is_o_iff
modified theorem asymptotics.is_o_irrefl'
modified theorem asymptotics.is_o_norm_left
modified theorem asymptotics.is_o_norm_norm
modified theorem asymptotics.is_o_norm_right
modified theorem complex.conj_cle_nnorm
modified theorem complex.conj_cle_norm
modified theorem complex.im_clm_nnnorm
modified theorem complex.im_clm_norm
modified theorem complex.nnnorm_int
modified theorem complex.nnnorm_nat
modified theorem complex.nnnorm_real
modified theorem complex.norm_eq_abs
modified theorem complex.norm_int
modified theorem complex.norm_int_of_nonneg
modified theorem complex.norm_nat
modified theorem complex.norm_rat
modified theorem complex.norm_real
modified theorem complex.of_real_clm_nnnorm
modified theorem complex.of_real_clm_norm
modified theorem complex.re_clm_nnnorm
modified theorem complex.re_clm_norm
modified theorem gauge_ball
modified theorem gauge_norm_smul
modified theorem gauge_smul
modified theorem gauge_unit_ball
modified theorem mul_gauge_le_norm
modified theorem abs_inner_le_norm
modified theorem abs_real_inner_le_norm
modified theorem innerSL_apply_norm
modified theorem inner_eq_norm_mul_iff_real
modified theorem inner_self_eq_norm_mul_norm
modified theorem inner_self_eq_norm_sq
modified theorem inner_self_eq_norm_sq_to_K
modified theorem nnnorm_inner_le_nnnorm
modified theorem norm_add_mul_self
modified theorem norm_add_mul_self_real
modified theorem norm_add_sq
modified theorem norm_add_sq_real
modified theorem norm_eq_sqrt_inner
modified theorem norm_eq_sqrt_real_inner
modified theorem norm_inner_le_norm
modified theorem norm_sub_eq_norm_add
modified theorem norm_sub_mul_self
modified theorem norm_sub_mul_self_real
modified theorem norm_sub_sq
modified theorem norm_sub_sq_real
modified theorem re_inner_le_norm
modified theorem real_inner_le_norm
modified theorem real_inner_self_eq_norm_sq
modified theorem real_inner_smul_self_left
modified theorem real_inner_smul_self_right
modified def absorbent
modified theorem absorbent_iff_nonneg_lt
modified def absorbs
modified theorem balanced.mem_smul_iff
modified theorem balanced.smul_eq
modified theorem balanced.smul_mono
modified theorem balanced.subset_smul
modified def balanced
modified theorem balanced_iff_smul_mem
modified theorem matrix.frobenius_nnnorm_col
modified theorem matrix.frobenius_nnnorm_mul
modified theorem matrix.frobenius_nnnorm_row
modified theorem matrix.frobenius_norm_col
modified theorem matrix.frobenius_norm_mul
modified theorem matrix.frobenius_norm_row
modified theorem matrix.linfty_op_nnnorm_mul
modified theorem matrix.linfty_op_norm_mul
modified theorem matrix.nnnorm_col
modified theorem matrix.nnnorm_diagonal
modified theorem matrix.nnnorm_map_eq
modified theorem matrix.nnnorm_row
modified theorem matrix.nnnorm_transpose
modified theorem matrix.norm_col
modified theorem matrix.norm_diagonal
modified theorem matrix.norm_map_eq
modified theorem matrix.norm_row
modified theorem matrix.norm_transpose
modified theorem eventually_norm_pow_le
modified theorem int.abs_le_floor_nnreal_iff
modified theorem int.norm_cast_rat
modified theorem int.norm_cast_real
modified theorem int.norm_eq_abs
modified theorem list.nnnorm_prod_le'
modified theorem list.nnnorm_prod_le
modified theorem list.norm_prod_le'
modified theorem list.norm_prod_le
modified theorem nat.norm_cast_le
modified theorem nnnorm_div
modified theorem nnnorm_inv
modified theorem nnnorm_mul
modified theorem nnnorm_mul_le
modified theorem nnnorm_norm
modified theorem nnnorm_nsmul_le
modified theorem nnnorm_pow
modified theorem nnnorm_pow_le'
modified theorem nnnorm_pow_le
modified theorem nnnorm_zpow
modified theorem nnnorm_zsmul_le
modified theorem nnreal.coe_nat_abs
modified theorem nnreal.nnnorm_eq
modified theorem nnreal.norm_eq
modified theorem norm_div
modified theorem norm_inv
modified theorem norm_mul
modified theorem norm_mul_le
modified theorem norm_norm
modified theorem norm_nsmul_le
modified theorem norm_pow
modified theorem norm_pow_le'
modified theorem norm_pow_le
modified theorem norm_zpow
modified theorem norm_zsmul_le
modified theorem normed_field.exists_lt_norm
modified theorem normed_field.exists_norm_lt
modified theorem one_le_nnnorm_one
modified theorem one_le_norm_one
modified theorem rat.norm_cast_real
modified theorem real.nnnorm_mul_to_nnreal
modified theorem real.to_nnreal_mul_nnnorm
modified theorem units.nnnorm_pos
modified theorem units.norm_pos
modified theorem abs_norm_sub_norm_le'
modified theorem ball_eq'
modified theorem ball_one_eq
modified theorem bounded_iff_forall_norm_le'
modified theorem closure_one_eq
modified theorem coe_nnnorm'
modified theorem continuous.nnnorm'
modified theorem continuous.norm'
modified theorem continuous_at.nnnorm'
modified theorem continuous_at.norm'
modified theorem continuous_nnnorm'
modified theorem continuous_norm'
modified theorem continuous_on.nnnorm'
modified theorem continuous_on.norm'
modified theorem dist_eq_norm_div'
modified theorem dist_eq_norm_div
modified theorem dist_le_norm_mul_norm
modified theorem dist_mul_self_left
modified theorem dist_mul_self_right
modified theorem dist_norm_norm_le'
modified theorem dist_one_right
modified theorem dist_self_div_left
modified theorem dist_self_div_right
modified theorem dist_self_mul_left
modified theorem dist_self_mul_right
modified theorem edist_eq_coe_nnnorm'
modified theorem edist_eq_coe_nnnorm_div
modified theorem eq_of_norm_div_le_zero
modified theorem mem_ball_iff_norm'''
modified theorem mem_ball_iff_norm''
modified theorem mem_ball_one_iff
modified theorem mem_closed_ball_iff_norm'''
modified theorem mem_closed_ball_iff_norm''
modified theorem mem_closed_ball_one_iff
modified theorem mem_closure_one_iff_norm
modified theorem mem_emetric_ball_one_iff
modified theorem mem_sphere_iff_norm'
modified theorem mem_sphere_one_iff_norm
modified theorem mul_mem_ball_iff_norm
modified theorem ne_one_of_nnnorm_ne_zero
modified theorem ne_one_of_norm_ne_zero
modified theorem nndist_eq_nnnorm_div
modified theorem nndist_nnnorm_nnnorm_le'
modified theorem nnnorm_div_le
modified theorem nnnorm_eq_zero'
modified theorem nnnorm_inv'
modified theorem nnnorm_le_mul_nnnorm_add
modified theorem nnnorm_le_pi_nnnorm'
modified theorem nnnorm_mul_le'
modified theorem nnnorm_multiset_prod_le
modified theorem nnnorm_ne_zero_iff'
modified theorem nnnorm_of_add
modified theorem nnnorm_of_dual
modified theorem nnnorm_of_mul
modified theorem nnnorm_one'
modified theorem nnnorm_prod_le_of_le
modified theorem nnnorm_to_add
modified theorem nnnorm_to_dual
modified theorem nnnorm_to_mul
modified theorem norm_div_eq_zero_iff
modified theorem norm_div_le
modified theorem norm_div_le_of_le
modified theorem norm_div_pos_iff
modified theorem norm_div_rev
modified theorem norm_eq_of_mem_sphere'
modified theorem norm_eq_zero'''
modified theorem norm_eq_zero''
modified theorem norm_fst_le
modified theorem norm_inv'
modified theorem norm_le_mul_norm_add
modified theorem norm_le_norm_add_norm_div'
modified theorem norm_le_norm_add_norm_div
modified theorem norm_le_of_mem_closed_ball'
modified theorem norm_le_pi_norm'
modified theorem norm_le_zero_iff'''
modified theorem norm_le_zero_iff''
modified theorem norm_lt_of_mem_ball'
modified theorem norm_mul_le'
modified theorem norm_mul_le_of_le
modified theorem norm_multiset_prod_le
modified theorem norm_mul₃_le
modified theorem norm_ne_zero_iff'
modified theorem norm_nonneg'
modified theorem norm_of_add
modified theorem norm_of_dual
modified theorem norm_of_mul
modified theorem norm_of_subsingleton'
modified theorem norm_one'
modified theorem norm_pos_iff'''
modified theorem norm_pos_iff''
modified theorem norm_prod_le
modified theorem norm_prod_le_iff
modified theorem norm_prod_le_of_le
modified theorem norm_snd_le
modified theorem norm_sub_norm_le'
modified theorem norm_to_add
modified theorem norm_to_dual
modified theorem norm_to_mul
modified theorem norm_to_nnreal'
modified theorem of_real_norm_eq_coe_nnnorm'
modified theorem pi.nnnorm_def'
modified theorem pi.norm_def'
modified theorem pi.sum_norm_apply_le_norm'
modified theorem pi_nnnorm_const'
modified theorem pi_nnnorm_const_le'
modified theorem pi_nnnorm_le_iff'
modified theorem pi_nnnorm_lt_iff'
modified theorem pi_norm_const'
modified theorem pi_norm_const_le'
modified theorem pi_norm_le_iff_of_nonempty'
modified theorem pi_norm_le_iff_of_nonneg'
modified theorem pi_norm_lt_iff'
modified theorem prod.nnorm_def
modified theorem prod.norm_def
modified theorem punit.norm_eq_zero
modified theorem real.ennnorm_eq_of_real
modified theorem real.le_norm_self
modified theorem real.nnnorm_coe_nat
modified theorem real.nnnorm_of_nonneg
modified theorem real.nnnorm_two
modified theorem real.norm_coe_nat
modified theorem real.norm_eq_abs
modified theorem real.norm_of_nonneg
modified theorem real.norm_of_nonpos
modified theorem real.norm_two
modified theorem real.of_real_le_ennnorm
modified theorem squeeze_one_norm'
modified theorem squeeze_one_norm
modified theorem subgroup.coe_norm
modified theorem subgroup.norm_coe
modified theorem tendsto_norm'
modified theorem tendsto_norm_div_self
modified theorem tendsto_norm_one
modified theorem ulift.nnnorm_def
modified theorem ulift.nnnorm_down
modified theorem ulift.nnnorm_up
modified theorem ulift.norm_def
modified theorem ulift.norm_down
modified theorem ulift.norm_up
modified theorem uniform_continuous_nnnorm'
modified theorem zero_lt_one_add_norm_sq'
modified theorem norm_mk_nonneg
modified theorem norm_mk_zero
modified theorem quotient_norm_add_le
modified theorem quotient_norm_neg
modified theorem quotient_norm_nonneg
modified theorem quotient_norm_sub_rev
modified theorem dual_solid
modified theorem norm_abs_eq_norm
modified theorem norm_inf_le_add
modified theorem norm_inf_sub_inf_le_norm
modified theorem norm_sup_le_add
modified theorem norm_sup_sub_sup_le_norm
modified theorem solid
modified theorem abs_norm_eq_norm
modified theorem dist_smul
modified theorem exists_norm_eq
modified theorem lipschitz_with_smul
modified theorem nnnorm_algebra_map'
modified theorem nnnorm_algebra_map
modified theorem nnnorm_algebra_map_nnreal
modified theorem nnnorm_smul
modified theorem norm_algebra_map'
modified theorem norm_algebra_map
modified theorem norm_algebra_map_nnreal
modified theorem norm_smul
modified theorem normed_space.exists_lt_norm
modified theorem rescale_to_shell
modified theorem lp.is_lub_norm
modified theorem lp.norm_apply_le_norm
modified theorem lp.norm_apply_le_of_tendsto
modified theorem lp.norm_const_smul
modified theorem lp.norm_eq_card_dsupport
modified theorem lp.norm_eq_csupr
modified theorem lp.norm_eq_zero_iff
modified theorem lp.norm_le_of_forall_le'
modified theorem lp.norm_le_of_forall_le
modified theorem lp.norm_le_of_tendsto
modified theorem lp.norm_neg
modified theorem lp.norm_nonneg'
modified theorem lp.norm_zero
modified theorem lp.sum_rpow_le_of_tendsto
modified theorem mem_ℓp.bdd_above
modified theorem mem_ℓp_gen'
modified theorem mem_ℓp_gen
modified theorem mem_ℓp_infty
modified theorem mem_ℓp_infty_iff
modified theorem submodule.norm_subtypeL
modified theorem submodule.norm_subtypeL_le
modified theorem is_R_or_C.conj_cle_norm
modified theorem is_R_or_C.inv_def
modified theorem is_R_or_C.norm_conj
modified theorem is_R_or_C.norm_eq_abs
modified theorem is_R_or_C.norm_im_le_norm
modified theorem is_R_or_C.norm_of_nonneg
modified theorem is_R_or_C.norm_of_real
modified theorem is_R_or_C.norm_re_le_norm
modified theorem is_R_or_C.norm_real
modified theorem is_R_or_C.norm_sq_eq_def'
modified theorem is_R_or_C.norm_sq_eq_def
modified theorem is_R_or_C.of_real_clm_norm
modified theorem is_R_or_C.re_clm_norm
modified theorem continuous_stereo_inv_fun
modified def stereo_inv_fun
modified theorem stereo_inv_fun_apply
modified def stereo_inv_fun_aux
modified theorem stereo_inv_fun_aux_mem
modified theorem stereo_left_inv
modified theorem stereo_right_inv
modified def stereographic
modified theorem stereographic_apply
modified theorem stereographic_source
modified theorem stereographic_target
modified theorem pgame.equiv.not_fuzzy'
modified theorem pgame.equiv.not_fuzzy
modified theorem pgame.fuzzy.not_equiv'
modified theorem pgame.fuzzy.not_equiv
modified theorem pgame.fuzzy.swap
modified theorem pgame.fuzzy.swap_iff
modified theorem pgame.fuzzy_congr
modified theorem pgame.fuzzy_congr_imp
modified theorem pgame.fuzzy_congr_left
modified theorem pgame.fuzzy_congr_right
modified theorem pgame.fuzzy_irrefl
modified theorem pgame.lf_iff_lt_or_fuzzy
modified theorem pgame.lf_of_fuzzy
modified theorem pgame.lt_or_fuzzy_of_lf
modified theorem pgame.neg_fuzzy_iff
modified theorem pgame.neg_fuzzy_neg_iff
modified theorem pgame.neg_fuzzy_zero_iff
modified theorem pgame.not_fuzzy_of_ge
modified theorem pgame.not_fuzzy_of_le
modified theorem pgame.star_fuzzy_zero
modified theorem pgame.zero_fuzzy_neg_iff