Commit 2024-02-04 13:16 e3a011e5

View on Github →

chore: rename op_norm to opNorm (#10185)

Estimated changes

Modified Counterexamples/Phillips.lean

Modified Mathlib/Analysis/Analytic/Basic.lean

Modified Mathlib/Analysis/Analytic/Composition.lean

Modified Mathlib/Analysis/Analytic/Constructions.lean

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

Modified Mathlib/Analysis/Calculus/FDeriv/Basic.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Measurable.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean

Modified Mathlib/Analysis/Calculus/MeanValue.lean

Modified Mathlib/Analysis/Calculus/ParametricIntegral.lean

Modified Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean

Modified Mathlib/Analysis/Complex/OperatorNorm.lean

Modified Mathlib/Analysis/Convolution.lean

Modified Mathlib/Analysis/Fourier/FourierTransformDeriv.lean

Modified Mathlib/Analysis/InnerProductSpace/Adjoint.lean

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

Modified Mathlib/Analysis/InnerProductSpace/MeanErgodic.lean

Modified Mathlib/Analysis/Matrix.lean

added theorem Matrix.linfty_opNNNorm_col

added theorem Matrix.linfty_opNNNorm_def

added theorem Matrix.linfty_opNNNorm_diagonal

added theorem Matrix.linfty_opNNNorm_eq_opNNNorm

added theorem Matrix.linfty_opNNNorm_mul

added theorem Matrix.linfty_opNNNorm_mulVec

added theorem Matrix.linfty_opNNNorm_row

added theorem Matrix.linfty_opNNNorm_toMatrix

added theorem Matrix.linfty_opNorm_col

added theorem Matrix.linfty_opNorm_def

added theorem Matrix.linfty_opNorm_diagonal

added theorem Matrix.linfty_opNorm_eq_opNorm

added theorem Matrix.linfty_opNorm_mul

added theorem Matrix.linfty_opNorm_mulVec

added theorem Matrix.linfty_opNorm_row

added theorem Matrix.linfty_opNorm_toMatrix

deleted theorem Matrix.linfty_op_nnnorm_col

deleted theorem Matrix.linfty_op_nnnorm_def

deleted theorem Matrix.linfty_op_nnnorm_diagonal

deleted theorem Matrix.linfty_op_nnnorm_eq_op_nnnorm

deleted theorem Matrix.linfty_op_nnnorm_mul

deleted theorem Matrix.linfty_op_nnnorm_mulVec

deleted theorem Matrix.linfty_op_nnnorm_row

deleted theorem Matrix.linfty_op_nnnorm_toMatrix

deleted theorem Matrix.linfty_op_norm_col

deleted theorem Matrix.linfty_op_norm_def

deleted theorem Matrix.linfty_op_norm_diagonal

deleted theorem Matrix.linfty_op_norm_eq_op_norm

deleted theorem Matrix.linfty_op_norm_mul

deleted theorem Matrix.linfty_op_norm_mulVec

deleted theorem Matrix.linfty_op_norm_row

deleted theorem Matrix.linfty_op_norm_toMatrix

Modified Mathlib/Analysis/NormedSpace/Algebra.lean

Modified Mathlib/Analysis/NormedSpace/Banach.lean

Modified Mathlib/Analysis/NormedSpace/BoundedLinearMaps.lean

Modified Mathlib/Analysis/NormedSpace/ContinuousAffineMap.lean

Modified Mathlib/Analysis/NormedSpace/Dual.lean

Modified Mathlib/Analysis/NormedSpace/Extend.lean

Modified Mathlib/Analysis/NormedSpace/FiniteDimension.lean

added theorem Basis.exists_opNNNorm_le

added theorem Basis.exists_opNorm_le

deleted theorem Basis.exists_op_nnnorm_le

deleted theorem Basis.exists_op_norm_le

added theorem Basis.opNNNorm_le

added theorem Basis.opNorm_le

deleted theorem Basis.op_nnnorm_le

deleted theorem Basis.op_norm_le

Modified Mathlib/Analysis/NormedSpace/HahnBanach/Extension.lean

Modified Mathlib/Analysis/NormedSpace/IsROrC.lean

added theorem ContinuousLinearMap.opNorm_bound_of_ball_bound

deleted theorem ContinuousLinearMap.op_norm_bound_of_ball_bound

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

added theorem ContinuousMultilinearMap.isLeast_opNNNorm

added theorem ContinuousMultilinearMap.isLeast_opNorm

deleted theorem ContinuousMultilinearMap.isLeast_op_nnnorm

deleted theorem ContinuousMultilinearMap.isLeast_op_norm

added theorem ContinuousMultilinearMap.le_mul_prod_of_le_opNorm_of_le

deleted theorem ContinuousMultilinearMap.le_mul_prod_of_le_op_norm_of_le

added theorem ContinuousMultilinearMap.le_of_opNNNorm_le

added theorem ContinuousMultilinearMap.le_of_opNorm_le

deleted theorem ContinuousMultilinearMap.le_of_op_nnnorm_le

deleted theorem ContinuousMultilinearMap.le_of_op_norm_le

added theorem ContinuousMultilinearMap.le_opNNNorm

added theorem ContinuousMultilinearMap.le_opNorm

added theorem ContinuousMultilinearMap.le_opNorm_mul_pow_card_of_le

added theorem ContinuousMultilinearMap.le_opNorm_mul_pow_of_le

added theorem ContinuousMultilinearMap.le_opNorm_mul_prod_of_le

deleted theorem ContinuousMultilinearMap.le_op_nnnorm

deleted theorem ContinuousMultilinearMap.le_op_norm

deleted theorem ContinuousMultilinearMap.le_op_norm_mul_pow_card_of_le

deleted theorem ContinuousMultilinearMap.le_op_norm_mul_pow_of_le

deleted theorem ContinuousMultilinearMap.le_op_norm_mul_prod_of_le

added theorem ContinuousMultilinearMap.opNNNorm_le_iff

added theorem ContinuousMultilinearMap.opNNNorm_pi

added theorem ContinuousMultilinearMap.opNNNorm_prod

added theorem ContinuousMultilinearMap.opNorm_add_le

added theorem ContinuousMultilinearMap.opNorm_le_bound

added theorem ContinuousMultilinearMap.opNorm_le_iff

added theorem ContinuousMultilinearMap.opNorm_neg

added theorem ContinuousMultilinearMap.opNorm_nonneg

added theorem ContinuousMultilinearMap.opNorm_pi

added theorem ContinuousMultilinearMap.opNorm_prod

added theorem ContinuousMultilinearMap.opNorm_smul_le

added theorem ContinuousMultilinearMap.opNorm_zero

added theorem ContinuousMultilinearMap.opNorm_zero_iff

deleted theorem ContinuousMultilinearMap.op_nnnorm_le_iff

deleted theorem ContinuousMultilinearMap.op_nnnorm_pi

deleted theorem ContinuousMultilinearMap.op_nnnorm_prod

deleted theorem ContinuousMultilinearMap.op_norm_add_le

deleted theorem ContinuousMultilinearMap.op_norm_le_bound

deleted theorem ContinuousMultilinearMap.op_norm_le_iff

deleted theorem ContinuousMultilinearMap.op_norm_neg

deleted theorem ContinuousMultilinearMap.op_norm_nonneg

deleted theorem ContinuousMultilinearMap.op_norm_pi

deleted theorem ContinuousMultilinearMap.op_norm_prod

deleted theorem ContinuousMultilinearMap.op_norm_smul_le

deleted theorem ContinuousMultilinearMap.op_norm_zero

deleted theorem ContinuousMultilinearMap.op_norm_zero_iff

added theorem ContinuousMultilinearMap.ratio_le_opNorm

deleted theorem ContinuousMultilinearMap.ratio_le_op_norm

added theorem ContinuousMultilinearMap.unit_le_opNorm

deleted theorem ContinuousMultilinearMap.unit_le_op_norm

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

Modified Mathlib/Analysis/NormedSpace/OperatorNorm.lean

added theorem ContinuousLinearMap.dist_le_opNorm

deleted theorem ContinuousLinearMap.dist_le_op_norm

added theorem ContinuousLinearMap.exists_lt_apply_of_lt_opNNNorm

added theorem ContinuousLinearMap.exists_lt_apply_of_lt_opNorm

deleted theorem ContinuousLinearMap.exists_lt_apply_of_lt_op_nnnorm

deleted theorem ContinuousLinearMap.exists_lt_apply_of_lt_op_norm

added theorem ContinuousLinearMap.exists_mul_lt_apply_of_lt_opNNNorm

deleted theorem ContinuousLinearMap.exists_mul_lt_apply_of_lt_op_nnnorm

added theorem ContinuousLinearMap.exists_mul_lt_of_lt_opNorm

deleted theorem ContinuousLinearMap.exists_mul_lt_of_lt_op_norm

added theorem ContinuousLinearMap.isLeast_opNNNorm

added theorem ContinuousLinearMap.isLeast_opNorm

deleted theorem ContinuousLinearMap.isLeast_op_nnnorm

deleted theorem ContinuousLinearMap.isLeast_op_norm

added theorem ContinuousLinearMap.le_of_opNorm_le

added theorem ContinuousLinearMap.le_of_opNorm_le_of_le

added theorem ContinuousLinearMap.le_of_opNorm₂_le_of_le

deleted theorem ContinuousLinearMap.le_of_op_norm_le

deleted theorem ContinuousLinearMap.le_of_op_norm_le_of_le

deleted theorem ContinuousLinearMap.le_of_op_norm₂_le_of_le

added theorem ContinuousLinearMap.le_opNNNorm

added theorem ContinuousLinearMap.le_opNorm

added theorem ContinuousLinearMap.le_opNorm_of_le

added theorem ContinuousLinearMap.le_opNorm₂

deleted theorem ContinuousLinearMap.le_op_nnnorm

deleted theorem ContinuousLinearMap.le_op_norm

deleted theorem ContinuousLinearMap.le_op_norm_of_le

deleted theorem ContinuousLinearMap.le_op_norm₂

added theorem ContinuousLinearMap.nndist_le_opNNNorm

deleted theorem ContinuousLinearMap.nndist_le_op_nnnorm

added theorem ContinuousLinearMap.opNNNorm_comp_le

added theorem ContinuousLinearMap.opNNNorm_eq_of_bounds

added theorem ContinuousLinearMap.opNNNorm_le_bound'

added theorem ContinuousLinearMap.opNNNorm_le_bound

added theorem ContinuousLinearMap.opNNNorm_le_iff

added theorem ContinuousLinearMap.opNNNorm_le_of_lipschitz

added theorem ContinuousLinearMap.opNNNorm_le_of_unit_nnnorm

added theorem ContinuousLinearMap.opNNNorm_mul

added theorem ContinuousLinearMap.opNNNorm_mul_apply

added theorem ContinuousLinearMap.opNNNorm_prod

added theorem ContinuousLinearMap.opNorm_add_le

added theorem ContinuousLinearMap.opNorm_comp_le

added theorem ContinuousLinearMap.opNorm_comp_linearIsometryEquiv

added theorem ContinuousLinearMap.opNorm_eq_of_bounds

added theorem ContinuousLinearMap.opNorm_ext

added theorem ContinuousLinearMap.opNorm_extend_le

added theorem ContinuousLinearMap.opNorm_flip

added theorem ContinuousLinearMap.opNorm_le_bound'

added theorem ContinuousLinearMap.opNorm_le_bound

added theorem ContinuousLinearMap.opNorm_le_bound₂

added theorem ContinuousLinearMap.opNorm_le_iff

added theorem ContinuousLinearMap.opNorm_le_of_ball

added theorem ContinuousLinearMap.opNorm_le_of_lipschitz

added theorem ContinuousLinearMap.opNorm_le_of_nhds_zero

added theorem ContinuousLinearMap.opNorm_le_of_shell'

added theorem ContinuousLinearMap.opNorm_le_of_shell

added theorem ContinuousLinearMap.opNorm_le_of_unit_norm

added theorem ContinuousLinearMap.opNorm_lsmul

added theorem ContinuousLinearMap.opNorm_lsmul_apply_le

added theorem ContinuousLinearMap.opNorm_lsmul_le

added theorem ContinuousLinearMap.opNorm_mul

added theorem ContinuousLinearMap.opNorm_mulLeftRight_apply_apply_le

added theorem ContinuousLinearMap.opNorm_mulLeftRight_apply_le

added theorem ContinuousLinearMap.opNorm_mulLeftRight_le

added theorem ContinuousLinearMap.opNorm_mul_apply

added theorem ContinuousLinearMap.opNorm_mul_apply_le

added theorem ContinuousLinearMap.opNorm_mul_le

added theorem ContinuousLinearMap.opNorm_neg

added theorem ContinuousLinearMap.opNorm_nonneg

added theorem ContinuousLinearMap.opNorm_prod

added theorem ContinuousLinearMap.opNorm_smul_le

added theorem ContinuousLinearMap.opNorm_subsingleton

added theorem ContinuousLinearMap.opNorm_zero

added theorem ContinuousLinearMap.opNorm_zero_iff

deleted theorem ContinuousLinearMap.op_nnnorm_comp_le

deleted theorem ContinuousLinearMap.op_nnnorm_eq_of_bounds

deleted theorem ContinuousLinearMap.op_nnnorm_le_bound'

deleted theorem ContinuousLinearMap.op_nnnorm_le_bound

deleted theorem ContinuousLinearMap.op_nnnorm_le_iff

deleted theorem ContinuousLinearMap.op_nnnorm_le_of_lipschitz

deleted theorem ContinuousLinearMap.op_nnnorm_le_of_unit_nnnorm

deleted theorem ContinuousLinearMap.op_nnnorm_mul

deleted theorem ContinuousLinearMap.op_nnnorm_mul_apply

deleted theorem ContinuousLinearMap.op_nnnorm_prod

deleted theorem ContinuousLinearMap.op_norm_add_le

deleted theorem ContinuousLinearMap.op_norm_comp_le

deleted theorem ContinuousLinearMap.op_norm_comp_linearIsometryEquiv

deleted theorem ContinuousLinearMap.op_norm_eq_of_bounds

deleted theorem ContinuousLinearMap.op_norm_ext

deleted theorem ContinuousLinearMap.op_norm_extend_le

deleted theorem ContinuousLinearMap.op_norm_flip

deleted theorem ContinuousLinearMap.op_norm_le_bound'

deleted theorem ContinuousLinearMap.op_norm_le_bound

deleted theorem ContinuousLinearMap.op_norm_le_bound₂

deleted theorem ContinuousLinearMap.op_norm_le_iff

deleted theorem ContinuousLinearMap.op_norm_le_of_ball

deleted theorem ContinuousLinearMap.op_norm_le_of_lipschitz

deleted theorem ContinuousLinearMap.op_norm_le_of_nhds_zero

deleted theorem ContinuousLinearMap.op_norm_le_of_shell'

deleted theorem ContinuousLinearMap.op_norm_le_of_shell

deleted theorem ContinuousLinearMap.op_norm_le_of_unit_norm

deleted theorem ContinuousLinearMap.op_norm_lsmul

deleted theorem ContinuousLinearMap.op_norm_lsmul_apply_le

deleted theorem ContinuousLinearMap.op_norm_lsmul_le

deleted theorem ContinuousLinearMap.op_norm_mul

deleted theorem ContinuousLinearMap.op_norm_mulLeftRight_apply_apply_le

deleted theorem ContinuousLinearMap.op_norm_mulLeftRight_apply_le

deleted theorem ContinuousLinearMap.op_norm_mulLeftRight_le

deleted theorem ContinuousLinearMap.op_norm_mul_apply

deleted theorem ContinuousLinearMap.op_norm_mul_apply_le

deleted theorem ContinuousLinearMap.op_norm_mul_le

deleted theorem ContinuousLinearMap.op_norm_neg

deleted theorem ContinuousLinearMap.op_norm_nonneg

deleted theorem ContinuousLinearMap.op_norm_prod

deleted theorem ContinuousLinearMap.op_norm_smul_le

deleted theorem ContinuousLinearMap.op_norm_subsingleton

deleted theorem ContinuousLinearMap.op_norm_zero

deleted theorem ContinuousLinearMap.op_norm_zero_iff

added theorem ContinuousLinearMap.ratio_le_opNorm

deleted theorem ContinuousLinearMap.ratio_le_op_norm

added theorem ContinuousLinearMap.unit_le_opNorm

deleted theorem ContinuousLinearMap.unit_le_op_norm

Modified Mathlib/Analysis/NormedSpace/Spectrum.lean

Modified Mathlib/Analysis/NormedSpace/Star/Matrix.lean

added theorem Matrix.l2_opNNNorm_conjTranspose

added theorem Matrix.l2_opNNNorm_conjTranspose_mul_self

added theorem Matrix.l2_opNNNorm_def

added theorem Matrix.l2_opNNNorm_mul

added theorem Matrix.l2_opNNNorm_mulVec

added theorem Matrix.l2_opNorm_conjTranspose

added theorem Matrix.l2_opNorm_conjTranspose_mul_self

added theorem Matrix.l2_opNorm_def

added theorem Matrix.l2_opNorm_mul

added theorem Matrix.l2_opNorm_mulVec

deleted theorem Matrix.l2_op_nnnorm_conjTranspose

deleted theorem Matrix.l2_op_nnnorm_conjTranspose_mul_self

deleted theorem Matrix.l2_op_nnnorm_def

deleted theorem Matrix.l2_op_nnnorm_mul

deleted theorem Matrix.l2_op_nnnorm_mulVec

deleted theorem Matrix.l2_op_norm_conjTranspose

deleted theorem Matrix.l2_op_norm_conjTranspose_mul_self

deleted theorem Matrix.l2_op_norm_def

deleted theorem Matrix.l2_op_norm_mul

deleted theorem Matrix.l2_op_norm_mulVec

Modified Mathlib/Analysis/NormedSpace/Star/Multiplier.lean

Modified Mathlib/Analysis/NormedSpace/Star/Unitization.lean

added theorem ContinuousLinearMap.opNNNorm_mul_flip_apply

added theorem ContinuousLinearMap.opNorm_mul_flip_apply

deleted theorem ContinuousLinearMap.op_nnnorm_mul_flip_apply

deleted theorem ContinuousLinearMap.op_norm_mul_flip_apply

Modified Mathlib/Analysis/NormedSpace/Unitization.lean

Modified Mathlib/Data/IsROrC/Lemmas.lean

Modified Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean

Modified Mathlib/MeasureTheory/Function/Jacobian.lean

Modified Mathlib/MeasureTheory/Function/L1Space.lean

Modified Mathlib/MeasureTheory/Function/LpSpace.lean

Modified Mathlib/MeasureTheory/Integral/Bochner.lean

Modified Mathlib/MeasureTheory/Integral/SetIntegral.lean

Modified Mathlib/MeasureTheory/Integral/SetToL1.lean

added theorem MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_opNorm

deleted theorem MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_op_norm

Modified Mathlib/Topology/ContinuousFunction/Bounded.lean

Modified scripts/style-exceptions.txt