There are a number of theorems about Bochner integrals (or even interval integrals) involving continuous linear maps related to composition. Most of these lemmas take honest-to-god ContinuousLinearMaps, but only ever use them in applied form. Therefore, they could be stated for the corresponding morphism class† without committing the cardinal sin of using morphism class coercions†† in the statement of a lemma. Since they are not, this leads to duplication of these lemmas for morphism types which happen to be continuous and linear (e.g., ContinuousLinearEquiv, LinearIsometry, etc.).
I noticed this during review of #40471 but decided not to ask the author to fix it because it's a comparatively large job.
An example of duplicated lemmas include: ContinuousLinearMap.integral_comp_comm, ContinuousLinearEquiv.integral_comp_comm, LinearIsometry.integral_comp_comm, but there are several others.
† We have ContinuousSemilinearMapClass and ContinuousLinearMapClass. We should deprecate these in favor of the existing unbundled classes ContinuousMapClass and SemilinearMapClass and LinearMapClass.
†† It seems we don't have these morphism class coercions for ContinuousLinearMap, which is good, but we're missing the underlying declarations themselves too (i.e., ContinuousLinearMap.ofClass); we should have those.
There are a number of theorems about Bochner integrals (or even interval integrals) involving continuous linear maps related to composition. Most of these lemmas take honest-to-god
ContinuousLinearMaps, but only ever use them in applied form. Therefore, they could be stated for the corresponding morphism class† without committing the cardinal sin of using morphism class coercions†† in the statement of a lemma. Since they are not, this leads to duplication of these lemmas for morphism types which happen to be continuous and linear (e.g.,ContinuousLinearEquiv,LinearIsometry, etc.).I noticed this during review of #40471 but decided not to ask the author to fix it because it's a comparatively large job.
An example of duplicated lemmas include: ContinuousLinearMap.integral_comp_comm, ContinuousLinearEquiv.integral_comp_comm, LinearIsometry.integral_comp_comm, but there are several others.
† We have ContinuousSemilinearMapClass and ContinuousLinearMapClass. We should deprecate these in favor of the existing unbundled classes
ContinuousMapClassandSemilinearMapClassandLinearMapClass.†† It seems we don't have these morphism class coercions for
ContinuousLinearMap, which is good, but we're missing the underlying declarations themselves too (i.e.,ContinuousLinearMap.ofClass); we should have those.