Commit 2025-05-17 18:54 fb3ad982

View on Github →

feat(Analysis/NormedSpace): add NormedSpace.Alternating (#8691) The file was copied from the file about continuous multilinear maps, then adjusted to continuous alternating maps. Most proofs were replaced by calls to the corresponding fact about multilinear maps.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/Alternating/Basic.lean

added theorem AlternatingMap.bound_of_shell

added theorem AlternatingMap.bound_of_shell_of_continuous

added theorem AlternatingMap.bound_of_shell_of_norm_map_coord_zero

added theorem AlternatingMap.coe_mkContinuous

added theorem AlternatingMap.continuous_of_bound

added theorem AlternatingMap.exists_bound_of_continuous

added def AlternatingMap.mkContinuous

added def AlternatingMap.mkContinuousAlternating

added theorem AlternatingMap.mkContinuousAlternating_apply

added theorem AlternatingMap.mkContinuousAlternating_norm_le

added theorem AlternatingMap.mkContinuousAlternating_norm_le_max

added def AlternatingMap.mkContinuousLinear

added theorem AlternatingMap.mkContinuousLinear_norm_le

added theorem AlternatingMap.mkContinuousLinear_norm_le_max

added theorem AlternatingMap.mkContinuous_norm_le'

added theorem AlternatingMap.mkContinuous_norm_le

added theorem AlternatingMap.norm_image_sub_le_of_bound'

added theorem AlternatingMap.norm_image_sub_le_of_bound

added theorem AlternatingMap.norm_map_coord_zero

added theorem ContinuousAlternatingMap.bound

added theorem ContinuousAlternatingMap.bounds_bddBelow

added theorem ContinuousAlternatingMap.bounds_nonempty

added def ContinuousAlternatingMap.compContinuousLinearMapCLM

added theorem ContinuousAlternatingMap.enorm_toContinuousMultilinearMap

added theorem ContinuousAlternatingMap.isLeast_opNNNorm

added theorem ContinuousAlternatingMap.isLeast_opNorm

added theorem ContinuousAlternatingMap.le_mul_prod_of_opNorm_le_of_le

added theorem ContinuousAlternatingMap.le_of_opNNNorm_le

added theorem ContinuousAlternatingMap.le_of_opNorm_le

added theorem ContinuousAlternatingMap.le_opNNNorm

added theorem ContinuousAlternatingMap.le_opNorm

added theorem ContinuousAlternatingMap.le_opNorm_mul_pow_card_of_le

added theorem ContinuousAlternatingMap.le_opNorm_mul_pow_of_le

added theorem ContinuousAlternatingMap.le_opNorm_mul_prod_of_le

added theorem ContinuousAlternatingMap.nnnorm_constOfIsEmpty

added theorem ContinuousAlternatingMap.nnnorm_ofSubsingleton

added theorem ContinuousAlternatingMap.nnnorm_ofSubsingleton_id

added theorem ContinuousAlternatingMap.nnnorm_ofSubsingleton_id_le

added theorem ContinuousAlternatingMap.nnnorm_toContinuousMultilinearMap

added theorem ContinuousAlternatingMap.norm_compContinuousLinearMap_le

added theorem ContinuousAlternatingMap.norm_constOfIsEmpty

added theorem ContinuousAlternatingMap.norm_def

added theorem ContinuousAlternatingMap.norm_image_sub_le'

added theorem ContinuousAlternatingMap.norm_image_sub_le

added theorem ContinuousAlternatingMap.norm_ofSubsingleton

added theorem ContinuousAlternatingMap.norm_ofSubsingleton_id

added theorem ContinuousAlternatingMap.norm_ofSubsingleton_id_le

added theorem ContinuousAlternatingMap.norm_restrictScalars

added theorem ContinuousAlternatingMap.norm_toContinuousMultilinearMap

added def ContinuousAlternatingMap.ofSubsingletonLIE

added theorem ContinuousAlternatingMap.opNNNorm_le_iff

added theorem ContinuousAlternatingMap.opNNNorm_pi

added theorem ContinuousAlternatingMap.opNNNorm_prod

added theorem ContinuousAlternatingMap.opNorm_le_bound

added theorem ContinuousAlternatingMap.opNorm_le_iff

added theorem ContinuousAlternatingMap.opNorm_pi

added theorem ContinuousAlternatingMap.opNorm_prod

added def ContinuousAlternatingMap.piLIE

added def ContinuousAlternatingMap.prodLIE

added theorem ContinuousAlternatingMap.ratio_le_opNorm

added def ContinuousAlternatingMap.restrictScalarsLI

added def ContinuousAlternatingMap.toContinuousMultilinearMapLI

added theorem ContinuousAlternatingMap.unit_le_opNorm

added def ContinuousLinearEquiv.continuousAlternatingMapCongr

added def ContinuousLinearEquiv.continuousAlternatingMapCongrLeft

added def ContinuousLinearEquiv.continuousAlternatingMapCongrRight

added theorem ContinuousLinearEquiv.continuousAlternatingMapCongrRight_symm

added def ContinuousLinearMap.compContinuousAlternatingMapCLM

added def ContinuousLinearMap.flipAlternating

added theorem ContinuousLinearMap.norm_compContinuousAlternatingMap_le

added theorem LinearIsometry.norm_compContinuousAlternatingMap

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

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

added def ContinuousAlternatingMap.toContinuousMultilinearMapCLM