Structures · Analysis
IsometricContinuousFunctionalCalculus
An extension of the ContinuousFunctionalCalculus requiring that cfcHom is an isometry.
- Shape
- 3 explicit arguments · adds isometric
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances3
- Real
- Complex
- NNReal
How is a type an instance?
Loading the hierarchy index…
Assumed by65
- IsGreatest.norm_cfc
- norm_apply_le_norm_cfc
- IsGreatest.nnnorm_cfc_nnreal
- isometry_cfcHom
- continuousOn_cfc
- apply_le_nnnorm_cfc_nnreal
- ContinuousOn.cfc
- ContinuousOn.cfc_nnreal
- norm_cfc_le
- Filter.Tendsto.cfc_nnreal
- lipschitzOnWith_cfc_fun_of_subset
- ContinuousOn.cfc_nnreal_of_mem_nhdsSet
- continuousOn_cfc_nnreal
- norm_cfcHom
- norm_cfc_lt
- IsGreatest.nnnorm_cfc
- Filter.Tendsto.cfc
- ContinuousOn.cfc_of_mem_nhdsSet
- ContinuousOn.cfc'
- IsometricContinuousFunctionalCalculus.isometric
- norm_cfc_lt_iff
- nnnorm_cfc_nnreal_le
- ContinuousWithinAt.cfc_nnreal
- CFC.nnnorm_rpow
- nnnorm_cfc_nnreal_lt
- IsometricContinuousFunctionalCalculus.isGreatest_spectrum
- ContinuousWithinAt.cfc
- nnnorm_apply_le_nnnorm_cfc
- ContinuousOn.cfc_nnreal'
- norm_cfc_le_iff
- lipschitzOnWith_cfc_fun
- continuous_cfcHomSuperset_left
- continuousOn_cfc_setProd
- continuousOn_cfc_nnreal_setProd
- nnnorm_cfc_nnreal_le_iff
- Continuous.cfc_nnreal_of_mem_nhdsSet
- ContinuousAt.cfc
- Continuous.cfc'
- Continuous.cfc_nnreal'
- continuousOn_cfc_setProd_nhdsSet
- IsometricContinuousFunctionalCalculus.nnnorm_spectrum_le
- nnnorm_cfc_lt
- nnnorm_cfc_lt_iff
- IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus
- Continuous.cfc
- SpectrumRestricts.isometric_cfc
- IsometricContinuousFunctionalCalculus.isGreatest_norm_spectrum
- IsometricContinuousFunctionalCalculus.toNonUnital
- nnnorm_cfc_le
- IsometricContinuousFunctionalCalculus.spectrum_le