Commit 2023-05-17 20:21 9ab40165

View on Github →

feat: port Analysis.NormedSpace.OperatorNorm (#3903)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/OperatorNorm.lean

added theorem Continuous.clm_comp_const

added theorem Continuous.const_clm_comp

added theorem Continuous.prod_mapL

added theorem Continuous.prod_map_equivL

added def ContinuousLinearEquiv.arrowCongr

added def ContinuousLinearEquiv.arrowCongrSL

added theorem ContinuousLinearEquiv.coord_norm

added theorem ContinuousLinearEquiv.isBigO_comp

added theorem ContinuousLinearEquiv.isBigO_comp_rev

added theorem ContinuousLinearEquiv.isBigO_sub

added theorem ContinuousLinearEquiv.isBigO_sub_rev

added theorem ContinuousLinearEquiv.nnnorm_symm_pos

added theorem ContinuousLinearEquiv.norm_pos

added theorem ContinuousLinearEquiv.norm_symm_pos

added theorem ContinuousLinearEquiv.one_le_norm_mul_norm_symm

added theorem ContinuousLinearEquiv.subsingleton_or_nnnorm_symm_pos

added theorem ContinuousLinearEquiv.subsingleton_or_norm_symm_pos

added theorem ContinuousLinearMap.antilipschitz_of_embedding

added def ContinuousLinearMap.apply'

added def ContinuousLinearMap.apply

added theorem ContinuousLinearMap.apply_apply'

added theorem ContinuousLinearMap.apply_apply

added def ContinuousLinearMap.bilinearComp

added theorem ContinuousLinearMap.bilinearComp_apply

added theorem ContinuousLinearMap.bound

added theorem ContinuousLinearMap.bounds_bddBelow

added theorem ContinuousLinearMap.bounds_nonempty

added theorem ContinuousLinearMap.coe_deriv₂

added theorem ContinuousLinearMap.coe_flipₗᵢ'

added theorem ContinuousLinearMap.coe_flipₗᵢ

added theorem ContinuousLinearMap.coe_mulₗᵢ

added theorem ContinuousLinearMap.coe_restrictScalarsIsometry

added theorem ContinuousLinearMap.coe_restrictScalarsL

added theorem ContinuousLinearMap.coe_restrict_scalarsL'

added def ContinuousLinearMap.compL

added theorem ContinuousLinearMap.compL_apply

added def ContinuousLinearMap.compSL

added theorem ContinuousLinearMap.compSL_apply

added def ContinuousLinearMap.deriv₂

added theorem ContinuousLinearMap.dist_le_op_norm

added theorem ContinuousLinearMap.exists_lt_apply_of_lt_op_nnnorm

added theorem ContinuousLinearMap.exists_lt_apply_of_lt_op_norm

added theorem ContinuousLinearMap.exists_mul_lt_apply_of_lt_op_nnnorm

added theorem ContinuousLinearMap.exists_mul_lt_of_lt_op_norm

added def ContinuousLinearMap.extend

added theorem ContinuousLinearMap.extend_eq

added theorem ContinuousLinearMap.extend_unique

added theorem ContinuousLinearMap.extend_zero

added def ContinuousLinearMap.flip

added theorem ContinuousLinearMap.flip_add

added theorem ContinuousLinearMap.flip_apply

added theorem ContinuousLinearMap.flip_flip

added theorem ContinuousLinearMap.flip_smul

added def ContinuousLinearMap.flipₗᵢ'

added theorem ContinuousLinearMap.flipₗᵢ'_symm

added def ContinuousLinearMap.flipₗᵢ

added theorem ContinuousLinearMap.flipₗᵢ_symm

added theorem ContinuousLinearMap.homothety_norm

added theorem ContinuousLinearMap.isBigOWith_comp

added theorem ContinuousLinearMap.isBigOWith_id

added theorem ContinuousLinearMap.isBigOWith_sub

added theorem ContinuousLinearMap.isBigO_comp

added theorem ContinuousLinearMap.isBigO_id

added theorem ContinuousLinearMap.isBigO_sub

added theorem ContinuousLinearMap.isClosed_image_coe_closedBall

added theorem ContinuousLinearMap.isClosed_image_coe_of_bounded_of_weak_closed

added theorem ContinuousLinearMap.isCompact_closure_image_coe_of_bounded

added theorem ContinuousLinearMap.isCompact_image_coe_closedBall

added theorem ContinuousLinearMap.isCompact_image_coe_of_bounded_of_closed_image

added theorem ContinuousLinearMap.isCompact_image_coe_of_bounded_of_weak_closed

added theorem ContinuousLinearMap.is_weak_closed_closedBall

added theorem ContinuousLinearMap.le_of_op_norm_le

added theorem ContinuousLinearMap.le_op_nnnorm

added theorem ContinuousLinearMap.le_op_norm

added theorem ContinuousLinearMap.le_op_norm_of_le

added theorem ContinuousLinearMap.le_op_norm₂

added theorem ContinuousLinearMap.lipschitz

added theorem ContinuousLinearMap.lipschitz_apply

added def ContinuousLinearMap.lsmul

added theorem ContinuousLinearMap.lsmul_apply

added theorem ContinuousLinearMap.map_add_add

added def ContinuousLinearMap.mul

added def ContinuousLinearMap.mulLeftRight

added theorem ContinuousLinearMap.mulLeftRight_apply

added theorem ContinuousLinearMap.mul_apply'

added def ContinuousLinearMap.mulₗᵢ

added theorem ContinuousLinearMap.nndist_le_op_nnnorm

added theorem ContinuousLinearMap.nnnorm_def

added theorem ContinuousLinearMap.nnnorm_smulRight_apply

added theorem ContinuousLinearMap.norm_compL_le

added theorem ContinuousLinearMap.norm_compSL_le

added theorem ContinuousLinearMap.norm_def

added theorem ContinuousLinearMap.norm_id

added theorem ContinuousLinearMap.norm_id_le

added theorem ContinuousLinearMap.norm_id_of_nontrivial_seminorm

added theorem ContinuousLinearMap.norm_precompL_le

added theorem ContinuousLinearMap.norm_precompR_le

added theorem ContinuousLinearMap.norm_restrictScalars

added theorem ContinuousLinearMap.norm_smulRightL

added theorem ContinuousLinearMap.norm_smulRightL_apply

added theorem ContinuousLinearMap.norm_smulRight_apply

added theorem ContinuousLinearMap.norm_toSpanSingleton

added def ContinuousLinearMap.ofMemClosureImageCoeBounded

added def ContinuousLinearMap.ofTendstoOfBoundedRange

added def ContinuousLinearMap.opNorm

added theorem ContinuousLinearMap.op_nnnorm_comp_le

added theorem ContinuousLinearMap.op_nnnorm_eq_of_bounds

added theorem ContinuousLinearMap.op_nnnorm_le_bound'

added theorem ContinuousLinearMap.op_nnnorm_le_bound

added theorem ContinuousLinearMap.op_nnnorm_le_of_lipschitz

added theorem ContinuousLinearMap.op_nnnorm_le_of_unit_nnnorm

added theorem ContinuousLinearMap.op_nnnorm_prod

added theorem ContinuousLinearMap.op_norm_add_le

added theorem ContinuousLinearMap.op_norm_comp_le'

added theorem ContinuousLinearMap.op_norm_comp_le

added theorem ContinuousLinearMap.op_norm_comp_linearIsometryEquiv

added theorem ContinuousLinearMap.op_norm_eq_of_bounds

added theorem ContinuousLinearMap.op_norm_ext

added theorem ContinuousLinearMap.op_norm_extend_le

added theorem ContinuousLinearMap.op_norm_flip

added theorem ContinuousLinearMap.op_norm_le_bound'

added theorem ContinuousLinearMap.op_norm_le_bound

added theorem ContinuousLinearMap.op_norm_le_bound₂

added theorem ContinuousLinearMap.op_norm_le_of_ball

added theorem ContinuousLinearMap.op_norm_le_of_lipschitz

added theorem ContinuousLinearMap.op_norm_le_of_nhds_zero

added theorem ContinuousLinearMap.op_norm_le_of_shell'

added theorem ContinuousLinearMap.op_norm_le_of_shell

added theorem ContinuousLinearMap.op_norm_le_of_unit_norm

added theorem ContinuousLinearMap.op_norm_lsmul

added theorem ContinuousLinearMap.op_norm_lsmul_apply_le

added theorem ContinuousLinearMap.op_norm_lsmul_le

added theorem ContinuousLinearMap.op_norm_mul

added theorem ContinuousLinearMap.op_norm_mulLeftRight_apply_apply_le

added theorem ContinuousLinearMap.op_norm_mulLeftRight_apply_le

added theorem ContinuousLinearMap.op_norm_mulLeftRight_le

added theorem ContinuousLinearMap.op_norm_mul_apply

added theorem ContinuousLinearMap.op_norm_mul_apply_le

added theorem ContinuousLinearMap.op_norm_mul_le

added theorem ContinuousLinearMap.op_norm_neg

added theorem ContinuousLinearMap.op_norm_nonneg

added theorem ContinuousLinearMap.op_norm_prod

added theorem ContinuousLinearMap.op_norm_smul_le

added theorem ContinuousLinearMap.op_norm_subsingleton

added theorem ContinuousLinearMap.op_norm_zero

added theorem ContinuousLinearMap.op_norm_zero_iff

added def ContinuousLinearMap.precompL

added def ContinuousLinearMap.precompR

added def ContinuousLinearMap.prodMapL

added theorem ContinuousLinearMap.prodMapL_apply

added def ContinuousLinearMap.prodₗᵢ

added theorem ContinuousLinearMap.ratio_le_op_norm

added def ContinuousLinearMap.restrictScalarsIsometry

added theorem ContinuousLinearMap.restrictScalarsIsometry_toLinearMap

added def ContinuousLinearMap.restrictScalarsL

added theorem ContinuousLinearMap.sSup_closed_unit_ball_eq_nnnorm

added theorem ContinuousLinearMap.sSup_closed_unit_ball_eq_norm

added theorem ContinuousLinearMap.sSup_unit_ball_eq_nnnorm

added theorem ContinuousLinearMap.sSup_unit_ball_eq_norm

added def ContinuousLinearMap.smulRightL

added theorem ContinuousLinearMap.tendsto_of_tendsto_pointwise_of_cauchySeq

added theorem ContinuousLinearMap.unit_le_op_norm

added theorem ContinuousOn.prod_mapL

added theorem ContinuousOn.prod_map_equivL

added def IsCoercive

added theorem LinearIsometry.coe_toSpanSingleton

added theorem LinearIsometry.norm_toContinuousLinearMap

added theorem LinearIsometry.norm_toContinuousLinearMap_comp

added theorem LinearIsometry.norm_toContinuousLinearMap_le

added def LinearIsometry.toSpanSingleton

added theorem LinearIsometry.toSpanSingleton_apply

added theorem LinearMap.antilipschitz_of_comap_nhds_le

added theorem LinearMap.bound_of_ball_bound

added theorem LinearMap.bound_of_shell

added theorem LinearMap.mkContinuous_norm_le'

added theorem LinearMap.mkContinuous_norm_le

added def LinearMap.mkContinuous₂

added theorem LinearMap.mkContinuous₂_apply

added theorem LinearMap.mkContinuous₂_norm_le'

added theorem LinearMap.mkContinuous₂_norm_le

added theorem SemilinearMapClass.bound_of_continuous

added theorem SemilinearMapClass.bound_of_shell_semi_normed

added theorem Submodule.norm_subtypeL

added theorem Submodule.norm_subtypeL_le

added theorem norm_image_of_norm_zero

Modified Mathlib/Topology/Algebra/Module/Basic.lean

Modified Mathlib/Topology/Algebra/Module/StrongTopology.lean