Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-07 16:57 2007d34f

View on Github →

feat(analysis/normed_space/multilinear): norm on continuous multilinear maps (#1956)

feat(analysis/normed_space/multilinear): norm on continuous multilinear maps
docstring
improved docstrings

Estimated changes

Created src/analysis/normed_space/multilinear.lean

added theorem continuous_linear_map.curry_uncurry_left

added theorem continuous_linear_map.norm_map_tail_right_le

added def continuous_linear_map.uncurry_left

added theorem continuous_linear_map.uncurry_left_apply

added theorem continuous_linear_map.uncurry_left_norm

added def continuous_multilinear_curry_fin0

added def continuous_multilinear_curry_fin0_aux

added def continuous_multilinear_curry_left_equiv

added def continuous_multilinear_curry_left_equiv_aux

added def continuous_multilinear_curry_right_equiv

added def continuous_multilinear_curry_right_equiv_aux

added theorem continuous_multilinear_map.bound

added theorem continuous_multilinear_map.bounds_bdd_below

added theorem continuous_multilinear_map.bounds_nonempty

added theorem continuous_multilinear_map.continuous_eval

added def continuous_multilinear_map.curry0

added theorem continuous_multilinear_map.curry0_apply

added theorem continuous_multilinear_map.curry0_norm

added theorem continuous_multilinear_map.curry0_uncurry0

added def continuous_multilinear_map.curry_left

added theorem continuous_multilinear_map.curry_left_apply

added theorem continuous_multilinear_map.curry_left_norm

added def continuous_multilinear_map.curry_right

added theorem continuous_multilinear_map.curry_right_apply

added theorem continuous_multilinear_map.curry_right_norm

added theorem continuous_multilinear_map.curry_uncurry_right

added theorem continuous_multilinear_map.le_op_norm

added theorem continuous_multilinear_map.mk_pi_field_apply

added theorem continuous_multilinear_map.mk_pi_ring_apply_one_eq_self

added theorem continuous_multilinear_map.norm_image_sub_le_of_bound'

added theorem continuous_multilinear_map.norm_image_sub_le_of_bound

added theorem continuous_multilinear_map.norm_map_cons_le

added theorem continuous_multilinear_map.norm_map_tail_left_le

added theorem continuous_multilinear_map.norm_zero

added def continuous_multilinear_map.op_norm

added theorem continuous_multilinear_map.op_norm_add_le

added theorem continuous_multilinear_map.op_norm_le_bound

added theorem continuous_multilinear_map.op_norm_neg

added theorem continuous_multilinear_map.op_norm_nonneg

added theorem continuous_multilinear_map.op_norm_smul

added theorem continuous_multilinear_map.op_norm_zero_iff

added theorem continuous_multilinear_map.ratio_le_op_norm

added def continuous_multilinear_map.uncurry0

added theorem continuous_multilinear_map.uncurry0_curry0

added theorem continuous_multilinear_map.uncurry0_norm

added theorem continuous_multilinear_map.uncurry_curry_left

added theorem continuous_multilinear_map.uncurry_curry_right

added def continuous_multilinear_map.uncurry_right

added theorem continuous_multilinear_map.uncurry_right_apply

added theorem continuous_multilinear_map.uncurry_right_norm

added theorem continuous_multilinear_map.unit_le_op_norm

added theorem multilinear_map.continuous_of_bound

added theorem multilinear_map.exists_bound_of_continuous

added def multilinear_map.mk_continuous

added theorem multilinear_map.mk_continuous_norm_le

added theorem multilinear_map.norm_image_sub_le_of_bound'

added theorem multilinear_map.norm_image_sub_le_of_bound