Commit 2023-05-18 20:25 18c085a5

View on Github →

feat: port Analysis.NormedSpace.Multilinear (#4057) Porting notes:

Some declarations are slow and need extra heartbeats
Needed to simp often before applying mkContinuous_norm_le, otherwise Lean wouldn't find the argument H automatically.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/Multilinear.lean

added def ContinuousLinearEquiv.compContinuousMultilinearMapL

added theorem ContinuousLinearEquiv.compContinuousMultilinearMapL_apply

added theorem ContinuousLinearEquiv.compContinuousMultilinearMapL_symm

added def ContinuousLinearMap.compContinuousMultilinearMapL

added theorem ContinuousLinearMap.curry_uncurryLeft

added def ContinuousLinearMap.flipMultilinear

added theorem ContinuousLinearMap.norm_compContinuousMultilinearMap_le

added theorem ContinuousLinearMap.norm_map_tail_le

added def ContinuousLinearMap.uncurryLeft

added theorem ContinuousLinearMap.uncurryLeft_apply

added theorem ContinuousLinearMap.uncurryLeft_norm

added theorem ContinuousMultilinearMap.apply_zero_curry0

added theorem ContinuousMultilinearMap.bound

added theorem ContinuousMultilinearMap.bounds_bddBelow

added theorem ContinuousMultilinearMap.bounds_nonempty

added def ContinuousMultilinearMap.compContinuousLinearMapEquivL

added theorem ContinuousMultilinearMap.compContinuousLinearMapEquivL_apply

added theorem ContinuousMultilinearMap.compContinuousLinearMapEquivL_symm

added def ContinuousMultilinearMap.compContinuousLinearMapL

added theorem ContinuousMultilinearMap.compContinuousLinearMapL_apply

added theorem ContinuousMultilinearMap.continuous_eval

added theorem ContinuousMultilinearMap.continuous_eval_left

added theorem ContinuousMultilinearMap.continuous_restrictScalars

added def ContinuousMultilinearMap.curry0

added theorem ContinuousMultilinearMap.curry0_apply

added theorem ContinuousMultilinearMap.curry0_norm

added theorem ContinuousMultilinearMap.curry0_uncurry0

added def ContinuousMultilinearMap.curryFinFinset

added theorem ContinuousMultilinearMap.curryFinFinset_apply

added theorem ContinuousMultilinearMap.curryFinFinset_apply_const

added theorem ContinuousMultilinearMap.curryFinFinset_symm_apply

added theorem ContinuousMultilinearMap.curryFinFinset_symm_apply_const

added theorem ContinuousMultilinearMap.curryFinFinset_symm_apply_piecewise_const

added def ContinuousMultilinearMap.curryLeft

added theorem ContinuousMultilinearMap.curryLeft_apply

added theorem ContinuousMultilinearMap.curryLeft_norm

added def ContinuousMultilinearMap.curryRight

added theorem ContinuousMultilinearMap.curryRight_apply

added theorem ContinuousMultilinearMap.curryRight_norm

added def ContinuousMultilinearMap.currySum

added def ContinuousMultilinearMap.currySumEquiv

added theorem ContinuousMultilinearMap.currySum_apply

added theorem ContinuousMultilinearMap.curry_uncurryRight

added def ContinuousMultilinearMap.domDomCongr

added theorem ContinuousMultilinearMap.fin0_apply_norm

added theorem ContinuousMultilinearMap.hasSum_eval

added theorem ContinuousMultilinearMap.le_of_op_nnnorm_le

added theorem ContinuousMultilinearMap.le_of_op_norm_le

added theorem ContinuousMultilinearMap.le_op_nnnorm

added theorem ContinuousMultilinearMap.le_op_norm

added theorem ContinuousMultilinearMap.le_op_norm_mul_pow_card_of_le

added theorem ContinuousMultilinearMap.le_op_norm_mul_pow_of_le

added theorem ContinuousMultilinearMap.le_op_norm_mul_prod_of_le

added theorem ContinuousMultilinearMap.mkPiField_apply

added theorem ContinuousMultilinearMap.mkPiField_apply_one_eq_self

added theorem ContinuousMultilinearMap.mkPiField_eq_iff

added theorem ContinuousMultilinearMap.mkPiField_eq_zero_iff

added theorem ContinuousMultilinearMap.mkPiField_zero

added theorem ContinuousMultilinearMap.nnnorm_constOfIsEmpty

added theorem ContinuousMultilinearMap.nnnorm_ofSubsingleton

added theorem ContinuousMultilinearMap.norm_compContinuousLinearMapL_le

added theorem ContinuousMultilinearMap.norm_compContinuousLinearMap_le

added theorem ContinuousMultilinearMap.norm_compContinuous_linearIsometryEquiv

added theorem ContinuousMultilinearMap.norm_compContinuous_linearIsometry_le

added theorem ContinuousMultilinearMap.norm_constOfIsEmpty

added theorem ContinuousMultilinearMap.norm_def

added theorem ContinuousMultilinearMap.norm_image_sub_le'

added theorem ContinuousMultilinearMap.norm_image_sub_le

added theorem ContinuousMultilinearMap.norm_map_cons_le

added theorem ContinuousMultilinearMap.norm_map_init_le

added theorem ContinuousMultilinearMap.norm_map_snoc_le

added theorem ContinuousMultilinearMap.norm_mkPiAlgebra

added theorem ContinuousMultilinearMap.norm_mkPiAlgebraFin

added theorem ContinuousMultilinearMap.norm_mkPiAlgebraFin_le_of_pos

added theorem ContinuousMultilinearMap.norm_mkPiAlgebraFin_succ_le

added theorem ContinuousMultilinearMap.norm_mkPiAlgebraFin_zero

added theorem ContinuousMultilinearMap.norm_mkPiAlgebra_le

added theorem ContinuousMultilinearMap.norm_mkPiAlgebra_of_empty

added theorem ContinuousMultilinearMap.norm_mkPiField

added theorem ContinuousMultilinearMap.norm_ofSubsingleton

added theorem ContinuousMultilinearMap.norm_pi

added theorem ContinuousMultilinearMap.norm_restr

added theorem ContinuousMultilinearMap.norm_restrictScalars

added def ContinuousMultilinearMap.opNorm

added theorem ContinuousMultilinearMap.op_norm_add_le

added theorem ContinuousMultilinearMap.op_norm_le_bound

added theorem ContinuousMultilinearMap.op_norm_neg

added theorem ContinuousMultilinearMap.op_norm_nonneg

added theorem ContinuousMultilinearMap.op_norm_prod

added theorem ContinuousMultilinearMap.op_norm_smul_le

added theorem ContinuousMultilinearMap.op_norm_zero

added theorem ContinuousMultilinearMap.op_norm_zero_iff

added def ContinuousMultilinearMap.piₗᵢ

added def ContinuousMultilinearMap.prodL

added theorem ContinuousMultilinearMap.ratio_le_op_norm

added def ContinuousMultilinearMap.restr

added def ContinuousMultilinearMap.restrictScalarsLinear

added theorem ContinuousMultilinearMap.tsum_eval

added def ContinuousMultilinearMap.uncurry0

added theorem ContinuousMultilinearMap.uncurry0_apply

added theorem ContinuousMultilinearMap.uncurry0_curry0

added theorem ContinuousMultilinearMap.uncurry0_norm

added def ContinuousMultilinearMap.uncurryRight

added theorem ContinuousMultilinearMap.uncurryRight_apply

added theorem ContinuousMultilinearMap.uncurryRight_norm

added def ContinuousMultilinearMap.uncurrySum

added theorem ContinuousMultilinearMap.uncurrySum_apply

added theorem ContinuousMultilinearMap.uncurry_curryLeft

added theorem ContinuousMultilinearMap.uncurry_curryRight

added theorem ContinuousMultilinearMap.unit_le_op_norm

added theorem LinearIsometry.norm_compContinuousMultilinearMap

added theorem MultilinearMap.bound_of_shell

added theorem MultilinearMap.coe_mkContinuous

added theorem MultilinearMap.continuous_of_bound

added theorem MultilinearMap.exists_bound_of_continuous

added def MultilinearMap.mkContinuous

added def MultilinearMap.mkContinuousLinear

added theorem MultilinearMap.mkContinuousLinear_norm_le'

added theorem MultilinearMap.mkContinuousLinear_norm_le

added def MultilinearMap.mkContinuousMultilinear

added theorem MultilinearMap.mkContinuousMultilinear_apply

added theorem MultilinearMap.mkContinuousMultilinear_norm_le'

added theorem MultilinearMap.mkContinuousMultilinear_norm_le

added theorem MultilinearMap.mkContinuous_norm_le'

added theorem MultilinearMap.mkContinuous_norm_le

added theorem MultilinearMap.norm_image_sub_le_of_bound'

added theorem MultilinearMap.norm_image_sub_le_of_bound

added theorem MultilinearMap.restr_norm_le

added def continuousMultilinearCurryFin0

added theorem continuousMultilinearCurryFin0_apply

added theorem continuousMultilinearCurryFin0_symm_apply

added def continuousMultilinearCurryFin1

added theorem continuousMultilinearCurryFin1_apply

added theorem continuousMultilinearCurryFin1_symm_apply

added def continuousMultilinearCurryLeftEquiv

added theorem continuousMultilinearCurryLeftEquiv_apply

added theorem continuousMultilinearCurryLeftEquiv_symm_apply

added def continuousMultilinearCurryRightEquiv'

added def continuousMultilinearCurryRightEquiv

added theorem continuousMultilinearCurryRightEquiv_apply'

added theorem continuousMultilinearCurryRightEquiv_apply

added theorem continuousMultilinearCurryRightEquiv_symm_apply'

added theorem continuousMultilinearCurryRightEquiv_symm_apply