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 phillips_1940.norm_bound
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 has_fderiv_at.eventually_ne
modified theorem complex.abs_sub_eq
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 lt_norm_sub_of_not_same_ray
modified theorem norm_add_lt_of_not_same_ray
modified theorem norm_combo_lt_of_ne
modified theorem norm_midpoint_lt_iff
modified theorem same_ray_iff_norm_add
modified theorem same_ray_iff_norm_sub
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 theorem cont_diff_norm_sq
modified theorem differentiable.norm_sq
modified theorem reflection_sub
modified theorem orientation.abs_kahler
modified theorem orientation.area_form_le
modified theorem orientation.kahler_mul
modified theorem orientation.norm_kahler
modified theorem orientation.norm_sq_kahler
modified def balanced_core_aux
modified def balanced_hull
modified theorem mem_balanced_core_aux_iff
modified theorem mem_balanced_hull_iff
modified theorem smul_balanced_core_subset
modified theorem subset_balanced_core
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 add_circle.norm_eq
modified theorem add_circle.norm_eq_of_zero
modified theorem unit_add_circle.norm_eq
modified theorem dist_eq_norm_vsub'
modified theorem dist_eq_norm_vsub
modified theorem dist_vadd_left
modified theorem dist_vadd_right
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 normed_add_group_hom.bound
modified theorem nnnorm_tsum_le
modified theorem norm_tsum_le_tsum_norm
modified theorem summable_of_summable_nnnorm
modified theorem summable_of_summable_norm
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 normed_space.mem_polar_iff
modified theorem enorm.finite_norm_eq
modified theorem enorm.map_smul
modified theorem norm_exp_series_summable'
modified theorem norm_exp_series_summable
modified theorem is_max_on.norm_add_self
modified theorem coord_norm'
modified theorem exists_dual_vector
modified theorem indicator_norm_le_norm_self
modified theorem norm_indicator_le_norm_self
modified theorem int.nnnorm_coe_nat
modified theorem int.nnnorm_coe_units
modified theorem int.norm_coe_nat
modified theorem int.norm_coe_units
modified theorem is_R_or_C.norm_coe_norm
modified theorem norm_smul_inv_norm
modified theorem linear_isometry.nnnorm_map
modified theorem linear_isometry.norm_map
modified theorem equiv_lp_pi_Lp_norm
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 pi_Lp.norm_eq_card
modified theorem pi_Lp.norm_eq_csupr
modified theorem smul_closed_unit_ball
modified theorem smul_unit_ball
modified theorem not_same_ray_iff_of_norm_eq
modified theorem same_ray.eq_of_norm_eq
modified theorem same_ray.norm_add
modified theorem same_ray.norm_eq_iff
modified theorem same_ray.norm_smul_eq
modified theorem same_ray.norm_sub
modified theorem same_ray_iff_norm_smul_eq
modified theorem same_ray_iff_of_norm_eq
modified theorem alg_hom.norm_apply_le_self
modified theorem cstar_ring.norm_coe_unitary
modified theorem cstar_ring.norm_one
modified theorem nnnorm_star
modified theorem op_nnnorm_mul
modified theorem op_nnnorm_mul_flip
modified theorem star_alg_hom.norm_apply_le
modified theorem ideal.eq_top_of_norm_lt_one
modified theorem normed_ring.inverse_one_sub
modified def units.add
modified def units.one_sub
modified def units.unit_of_nearby
modified theorem weak_dual.polar_def
modified theorem quaternion.nnnorm_coe
modified theorem quaternion.norm_coe
modified theorem absorbent_ball
modified theorem seminorm.smul_ball_zero
modified theorem complex.exp_bound_sq
modified theorem sqrt_one_add_norm_sq_le
modified theorem real.norm_rpow_of_nonneg
modified theorem geom_series_mul_neg
modified theorem mul_neg_geom_series
modified theorem norm_sum_neg_one_pow_le
modified theorem tsum_geometric_of_norm_lt_1
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 measurable.nnnorm
modified theorem measurable_ennnorm
modified theorem besicovitch.exists_good_δ
modified theorem measure_theory.Lp.norm_def
modified theorem measure_theory.Lp.norm_neg
modified theorem measure_theory.Lp.norm_zero
modified theorem measure_theory.snorm'_norm
modified theorem measure_theory.snorm_mono
modified theorem measure_theory.snorm_norm
modified theorem hensels_lemma
modified theorem padic_int.inv_mul
modified theorem padic_int.is_unit_iff
modified theorem padic_int.mem_nonunits
modified theorem padic_int.mem_subring_iff
modified def padic_int.mk_units
modified theorem padic_int.mk_units_eq
modified theorem padic_int.mul_inv
modified theorem padic_int.nonarchimedean
modified theorem padic_int.norm_def
modified theorem padic_int.norm_eq_pow_val
modified theorem padic_int.norm_le_one
modified theorem padic_int.norm_lt_one_add
modified theorem padic_int.norm_lt_one_mul
modified theorem padic_int.norm_mul
modified theorem padic_int.norm_p
modified theorem padic_int.norm_p_pow
modified theorem padic_int.norm_pow
modified theorem padic_int.norm_units
modified def padic_int
modified theorem padic.norm_eq_pow_val
modified theorem padic.padic_norm_e_lim_le
modified theorem padic.rat_dense
modified theorem padic_norm_e.eq_padic_norm
modified theorem padic_norm_e.eq_rat_norm
modified theorem padic_norm_e.nonarchimedean
modified theorem padic_norm_e.norm_p
modified theorem padic_norm_e.norm_p_lt_one
modified theorem padic_norm_e.norm_p_pow
modified theorem padic_int.is_unit_denom
modified theorem padic_int.norm_sub_mod_part
modified theorem pgame.fuzzy_iff_game_fuzzy
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
modified theorem continuous_map.norm_le
modified theorem continuous_map.norm_lt_iff