Commit 2023-11-14 16:55 e29251b7

View on Github →

chore: split Analysis.NormedSpace.Multilinear (#8392) This moves the isomorphisms corresponding to currying or uncurrying variables into a separate file, as they're mostly independent of the rest of the file.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean

Modified Mathlib/Analysis/NormedSpace/Multilinear.lean

deleted theorem ContinuousLinearMap.curry_uncurryLeft

deleted theorem ContinuousLinearMap.norm_map_tail_le

deleted def ContinuousLinearMap.uncurryLeft

deleted theorem ContinuousLinearMap.uncurryLeft_apply

deleted theorem ContinuousLinearMap.uncurryLeft_norm

deleted theorem ContinuousMultilinearMap.apply_zero_curry0

deleted def ContinuousMultilinearMap.curry0

deleted theorem ContinuousMultilinearMap.curry0_apply

deleted theorem ContinuousMultilinearMap.curry0_norm

deleted theorem ContinuousMultilinearMap.curry0_uncurry0

deleted def ContinuousMultilinearMap.curryFinFinset

deleted theorem ContinuousMultilinearMap.curryFinFinset_apply

deleted theorem ContinuousMultilinearMap.curryFinFinset_apply_const

deleted theorem ContinuousMultilinearMap.curryFinFinset_symm_apply

deleted theorem ContinuousMultilinearMap.curryFinFinset_symm_apply_const

deleted theorem ContinuousMultilinearMap.curryFinFinset_symm_apply_piecewise_const

deleted def ContinuousMultilinearMap.curryLeft

deleted theorem ContinuousMultilinearMap.curryLeft_apply

deleted theorem ContinuousMultilinearMap.curryLeft_norm

deleted def ContinuousMultilinearMap.curryRight

deleted theorem ContinuousMultilinearMap.curryRight_apply

deleted theorem ContinuousMultilinearMap.curryRight_norm

deleted def ContinuousMultilinearMap.currySum

deleted def ContinuousMultilinearMap.currySumEquiv

deleted theorem ContinuousMultilinearMap.currySum_apply

deleted theorem ContinuousMultilinearMap.curry_uncurryRight

deleted def ContinuousMultilinearMap.domDomCongrₗᵢ

deleted theorem ContinuousMultilinearMap.fin0_apply_norm

deleted theorem ContinuousMultilinearMap.norm_domDomCongr

deleted theorem ContinuousMultilinearMap.norm_map_cons_le

deleted theorem ContinuousMultilinearMap.norm_map_init_le

deleted theorem ContinuousMultilinearMap.norm_map_snoc_le

deleted def ContinuousMultilinearMap.uncurry0

deleted theorem ContinuousMultilinearMap.uncurry0_apply

deleted theorem ContinuousMultilinearMap.uncurry0_curry0

deleted theorem ContinuousMultilinearMap.uncurry0_norm

deleted def ContinuousMultilinearMap.uncurryRight

deleted theorem ContinuousMultilinearMap.uncurryRight_apply

deleted theorem ContinuousMultilinearMap.uncurryRight_norm

deleted def ContinuousMultilinearMap.uncurrySum

deleted theorem ContinuousMultilinearMap.uncurrySum_apply

deleted theorem ContinuousMultilinearMap.uncurry_curryLeft

deleted theorem ContinuousMultilinearMap.uncurry_curryRight

deleted def continuousMultilinearCurryFin0

deleted theorem continuousMultilinearCurryFin0_apply

deleted theorem continuousMultilinearCurryFin0_symm_apply

deleted def continuousMultilinearCurryFin1

deleted theorem continuousMultilinearCurryFin1_apply

deleted theorem continuousMultilinearCurryFin1_symm_apply

deleted def continuousMultilinearCurryLeftEquiv

deleted theorem continuousMultilinearCurryLeftEquiv_apply

deleted theorem continuousMultilinearCurryLeftEquiv_symm_apply

deleted def continuousMultilinearCurryRightEquiv'

deleted def continuousMultilinearCurryRightEquiv

deleted theorem continuousMultilinearCurryRightEquiv_apply'

deleted theorem continuousMultilinearCurryRightEquiv_apply

deleted theorem continuousMultilinearCurryRightEquiv_symm_apply'

deleted theorem continuousMultilinearCurryRightEquiv_symm_apply

Created Mathlib/Analysis/NormedSpace/MultilinearCurrying.lean

added theorem ContinuousLinearMap.curry_uncurryLeft

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 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.norm_domDomCongr

added theorem ContinuousMultilinearMap.norm_map_cons_le

added theorem ContinuousMultilinearMap.norm_map_init_le

added theorem ContinuousMultilinearMap.norm_map_snoc_le

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 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