Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-08 03:50 2bfa7684

View on Github →

feat(analysis/normed_space/operator_norm): module and norm instances on continuous semilinear maps (#10494) This PR adds a module and a norm instance on continuous semilinear maps, generalizes most of the results in operator_norm.lean to the semilinear case. Many of these results require the ring homomorphism to be isometric, which is expressed via the new typeclass [ring_hom_isometric σ].

Estimated changes

Modified src/analysis/calculus/fderiv_measurable.lean

Modified src/analysis/normed_space/basic.lean

Modified src/analysis/normed_space/dual.lean

Modified src/analysis/normed_space/operator_norm.lean

modified theorem continuous_linear_equiv.homothety_inverse

modified theorem continuous_linear_equiv.nnnorm_symm_pos

modified theorem continuous_linear_equiv.norm_pos

modified theorem continuous_linear_equiv.norm_symm_pos

modified def continuous_linear_equiv.of_homothety

modified theorem continuous_linear_equiv.one_le_norm_mul_norm_symm

modified theorem continuous_linear_equiv.subsingleton_or_nnnorm_symm_pos

modified theorem continuous_linear_equiv.subsingleton_or_norm_symm_pos

modified theorem continuous_linear_equiv.uniform_embedding

modified theorem continuous_linear_map.antilipschitz_of_uniform_embedding

added def continuous_linear_map.apply'

modified def continuous_linear_map.apply

added theorem continuous_linear_map.apply_apply'

modified theorem continuous_linear_map.apply_apply

modified def continuous_linear_map.bilinear_comp

modified theorem continuous_linear_map.bilinear_comp_apply

modified theorem continuous_linear_map.bound

modified theorem continuous_linear_map.bounds_bdd_below

modified theorem continuous_linear_map.bounds_nonempty

modified theorem continuous_linear_map.coe_deriv₂

added theorem continuous_linear_map.coe_flipₗᵢ'

modified theorem continuous_linear_map.coe_flipₗᵢ

modified def continuous_linear_map.compL

modified theorem continuous_linear_map.compL_apply

added def continuous_linear_map.compSL

added theorem continuous_linear_map.compSL_apply

modified def continuous_linear_map.deriv₂

modified def continuous_linear_map.extend

modified theorem continuous_linear_map.extend_unique

modified theorem continuous_linear_map.extend_zero

modified def continuous_linear_map.flip

modified theorem continuous_linear_map.flip_add

modified theorem continuous_linear_map.flip_apply

modified theorem continuous_linear_map.flip_flip

modified theorem continuous_linear_map.flip_smul

added def continuous_linear_map.flipₗᵢ'

added theorem continuous_linear_map.flipₗᵢ'_symm

modified def continuous_linear_map.flipₗᵢ

modified theorem continuous_linear_map.flipₗᵢ_symm

modified theorem continuous_linear_map.homothety_norm

modified theorem continuous_linear_map.is_O_comp

modified theorem continuous_linear_map.is_O_sub

modified theorem continuous_linear_map.is_O_with_comp

modified theorem continuous_linear_map.is_O_with_sub

modified theorem continuous_linear_map.isometry_iff_norm

modified theorem continuous_linear_map.le_op_norm₂

modified theorem continuous_linear_map.map_add₂

modified theorem continuous_linear_map.nnnorm_smul_right_apply

modified theorem continuous_linear_map.norm_def

modified theorem continuous_linear_map.norm_restrict_scalars

modified theorem continuous_linear_map.norm_smul_rightL

modified theorem continuous_linear_map.norm_smul_rightL_apply

modified theorem continuous_linear_map.norm_smul_right_apply

modified def continuous_linear_map.of_homothety

modified def continuous_linear_map.op_norm

modified theorem continuous_linear_map.op_norm_comp_le

modified theorem continuous_linear_map.op_norm_comp_linear_isometry_equiv

modified theorem continuous_linear_map.op_norm_eq_of_bounds

modified theorem continuous_linear_map.op_norm_flip

modified theorem continuous_linear_map.op_norm_le_bound

modified theorem continuous_linear_map.op_norm_le_bound₂

modified theorem continuous_linear_map.op_norm_le_of_ball

modified theorem continuous_linear_map.op_norm_le_of_lipschitz

modified theorem continuous_linear_map.op_norm_le_of_nhds_zero

modified theorem continuous_linear_map.op_norm_le_of_shell'

modified theorem continuous_linear_map.op_norm_le_of_shell

modified theorem continuous_linear_map.op_norm_neg

modified theorem continuous_linear_map.op_norm_prod

modified theorem continuous_linear_map.op_norm_zero

modified def continuous_linear_map.prodₗᵢ

modified def continuous_linear_map.restrict_scalarsL

modified def continuous_linear_map.restrict_scalars_isometry

modified def continuous_linear_map.smul_rightL

modified def linear_equiv.to_continuous_linear_equiv_of_bounds

modified theorem linear_equiv.uniform_embedding

modified theorem linear_isometry.norm_to_continuous_linear_map

modified theorem linear_isometry.norm_to_continuous_linear_map_le

modified theorem linear_map.bound_of_continuous

modified theorem linear_map.bound_of_shell

modified theorem linear_map.bound_of_shell_semi_normed

modified theorem linear_map.mk_continuous_norm_le'

modified theorem linear_map.mk_continuous_norm_le

modified def linear_map.mk_continuous₂

modified theorem linear_map.mk_continuous₂_apply

modified theorem linear_map.mk_continuous₂_norm_le'

modified theorem linear_map.mk_continuous₂_norm_le

modified theorem norm_image_of_norm_zero

Modified src/data/complex/is_R_or_C.lean

Modified src/topology/algebra/module.lean

modified def continuous_linear_map.coe_lm

added def continuous_linear_map.coe_lmₛₗ

modified theorem continuous_linear_map.coe_smul'

modified theorem continuous_linear_map.coe_smul

modified theorem continuous_linear_map.comp_smul

modified def continuous_linear_map.prod_equiv

modified theorem continuous_linear_map.prod_ext

modified theorem continuous_linear_map.prod_ext_iff

modified def continuous_linear_map.prodₗ