← all areas

Namespace ContinuousLinearMap 10 theorems

• Orthogonal complement of the non-zero eigenspaces is ker T ContinuousLinearMap.orthogonal_iSup_eigenspace_ne_zero_eq_ker 0 below · cited by 4 · depth 19
• Symmetry on a subspace forbids v∈(T-c)(E) for all real c ContinuousLinearMap.eq_zero_of_forall_exists_mem_sub_real_smul_eq 0 below · cited by 2 · depth 20
• Commuting operators preserve eigenspaces of a symmetric operator ContinuousLinearMap.map_eigenspace_orthogonal_le_of_commute 0 below · cited by 2 · depth 20
• Dichotomy against high eigenspaces forces kernel or finite dimension ContinuousLinearMap.le_ker_or_finiteDimensional_of_forall_inf_highPart_orthogonal 0 below · cited by 1 · depth 21
• Weighted averages of a compact group representation compose by convolution ContinuousLinearMap.comp_eq_of_forall_apply_eq_integral_smul_apply_of_convolution 0 below · cited by 1 · depth 22
• Weighted Haar average of a bounded continuous representation ContinuousLinearMap.exists_forall_apply_eq_integral_smul_apply_of_forall_norm_le_of_continuous 0 below · cited by 2 · depth 22
• Commuting operators preserve the orthocomplement of the high eigen-part ContinuousLinearMap.map_highPart_orthogonal_le_of_commute 0 below · cited by 1 · depth 22
• Atom-free functionals pull back along coordinatewise finite-fibre maps ContinuousLinearMap.noAtomicMass_comp_of_finite_fibres 0 below · cited by 2 · depth 24
• Laurent expansion of monomials pulled back to the torus ContinuousLinearMap.apply_comp_comp_torusEmb_eq_sum_laurentCoeff_mul_of_apply_fourier_eq 0 below · cited by 1 · depth 28
• Pushing a box-atomless functional from the torus to (ℂ×ℂ)ᵈ ContinuousLinearMap.exists_comp_torusEmb_eq_and_cylinder_noAtomicMass_of_box_noAtomicMass 0 below · cited by 1 · depth 28