Commit 2024-11-28 16:12 37dfa236

View on Github →

chore(Analysis/Multilinear): avoid explicit variables (#19445) Also change implicitness of some arguments, including the function argument of ContinuousMultilinearMap.opNorm_le_bound, expand some docstrings, and reorder arguments of ContinuousMultilinearMap.le_of_opNorm_le

Estimated changes

Modified Mathlib/Analysis/Analytic/ChangeOrigin.lean

Modified Mathlib/Analysis/Analytic/Composition.lean

Modified Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean

Modified Mathlib/Analysis/Fourier/FourierTransformDeriv.lean

Modified Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean

Modified Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

modified theorem ContinuousLinearMap.continuousAt_uncurry_of_multilinear

modified theorem ContinuousLinearMap.continuousOn_uncurry_of_multilinear

modified theorem ContinuousLinearMap.continuousWithinAt_uncurry_of_multilinear

modified theorem ContinuousLinearMap.continuous_uncurry_of_multilinear

modified theorem ContinuousMultilinearMap.bound

modified theorem ContinuousMultilinearMap.isLeast_opNNNorm

modified theorem ContinuousMultilinearMap.isLeast_opNorm

deleted theorem ContinuousMultilinearMap.le_mul_prod_of_le_opNorm_of_le

added theorem ContinuousMultilinearMap.le_mul_prod_of_opNorm_le_of_le

modified theorem ContinuousMultilinearMap.le_of_opNNNorm_le

modified theorem ContinuousMultilinearMap.le_of_opNorm_le

modified theorem ContinuousMultilinearMap.le_opNNNorm

modified theorem ContinuousMultilinearMap.le_opNorm

modified theorem ContinuousMultilinearMap.le_opNorm_mul_pow_card_of_le

modified theorem ContinuousMultilinearMap.le_opNorm_mul_prod_of_le

modified theorem ContinuousMultilinearMap.norm_def

modified theorem ContinuousMultilinearMap.norm_image_sub_le'

modified theorem ContinuousMultilinearMap.norm_image_sub_le

modified theorem ContinuousMultilinearMap.norm_restrictScalars

modified theorem ContinuousMultilinearMap.opNNNorm_le_iff

modified def ContinuousMultilinearMap.opNorm

modified theorem ContinuousMultilinearMap.opNorm_add_le

modified theorem ContinuousMultilinearMap.opNorm_le_bound

modified theorem ContinuousMultilinearMap.opNorm_le_iff

modified theorem ContinuousMultilinearMap.opNorm_neg

modified theorem ContinuousMultilinearMap.opNorm_nonneg

modified theorem ContinuousMultilinearMap.opNorm_smul_le

modified theorem ContinuousMultilinearMap.opNorm_zero_iff

modified theorem ContinuousMultilinearMap.ratio_le_opNorm

modified theorem ContinuousMultilinearMap.unit_le_opNorm

modified theorem MultilinearMap.bound_of_shell

modified theorem MultilinearMap.bound_of_shell_of_continuous

modified theorem MultilinearMap.bound_of_shell_of_norm_map_coord_zero

modified theorem MultilinearMap.coe_mkContinuous

modified theorem MultilinearMap.continuous_of_bound

modified theorem MultilinearMap.exists_bound_of_continuous

modified def MultilinearMap.mkContinuous

modified theorem MultilinearMap.norm_image_sub_le_of_bound'

modified theorem MultilinearMap.norm_image_sub_le_of_bound

modified theorem MultilinearMap.norm_map_coord_zero

modified theorem MultilinearMap.restr_norm_le

Modified Mathlib/Analysis/NormedSpace/Multilinear/Curry.lean

Modified Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean