Commit 2023-05-20 10:55 33109352

View on Github →

feat: port Analysis.NormedSpace.BoundedLinearMaps (#4091) Simplify a few proofs to avoid non-terminal simps in favor of rewrites and have instead of convert.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/BoundedLinearMaps.lean

added theorem Continuous.clm_comp

added theorem ContinuousLinearMap.continuous₂

added theorem ContinuousLinearMap.isBoundedBilinearMap

added theorem ContinuousLinearMap.isBoundedLinearMap

added theorem ContinuousLinearMap.isBoundedLinearMap_comp_left

added theorem ContinuousLinearMap.isBoundedLinearMap_comp_right

added theorem ContinuousLinearMap.map_add₂

added theorem ContinuousLinearMap.map_neg₂

added theorem ContinuousLinearMap.map_smul₂

added theorem ContinuousLinearMap.map_smulₛₗ₂

added theorem ContinuousLinearMap.map_sub₂

added theorem ContinuousLinearMap.map_zero₂

added theorem ContinuousLinearMap.mulLeftRightIsBoundedBilinear

added theorem ContinuousOn.clm_comp

added theorem IsBoundedBilinearMap.continuous

added theorem IsBoundedBilinearMap.continuous_left

added theorem IsBoundedBilinearMap.continuous_right

added def IsBoundedBilinearMap.deriv

added theorem IsBoundedBilinearMap.isBigO_comp

added theorem IsBoundedBilinearMap.isBoundedLinearMap_deriv

added theorem IsBoundedBilinearMap.isBoundedLinearMap_left

added theorem IsBoundedBilinearMap.isBoundedLinearMap_right

added def IsBoundedBilinearMap.linearDeriv

added theorem IsBoundedBilinearMap.map_sub_left

added theorem IsBoundedBilinearMap.map_sub_right

added structure IsBoundedBilinearMap

added theorem IsBoundedLinearMap.add

added theorem IsBoundedLinearMap.comp

added theorem IsBoundedLinearMap.continuous

added theorem IsBoundedLinearMap.fst

added theorem IsBoundedLinearMap.id

added theorem IsBoundedLinearMap.isBigO_comp

added theorem IsBoundedLinearMap.isBigO_id

added theorem IsBoundedLinearMap.isBigO_sub

added theorem IsBoundedLinearMap.lim_zero_bounded_linear_map

added theorem IsBoundedLinearMap.neg

added theorem IsBoundedLinearMap.smul

added theorem IsBoundedLinearMap.snd

added theorem IsBoundedLinearMap.sub

added def IsBoundedLinearMap.toContinuousLinearMap

added def IsBoundedLinearMap.toLinearMap

added theorem IsBoundedLinearMap.zero

added structure IsBoundedLinearMap

added theorem IsLinearMap.with_bound

added theorem isBoundedBilinearMapApply

added theorem isBoundedBilinearMapComp

added theorem isBoundedBilinearMapCompMultilinear

added theorem isBoundedBilinearMapMul

added theorem isBoundedBilinearMapSmul

added theorem isBoundedBilinearMapSmulRight

added theorem isBoundedBilinearMap_deriv_coe

added theorem isBoundedLinearMap_continuousMultilinearMap_comp_linear

added theorem isBoundedLinearMap_prod_multilinear