Commit 2023-06-11 13:19 19ef206f

View on Github →

feat: port Analysis.NormedSpace.Spectrum (#4946)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/Spectrum.lean

added theorem AlgHom.coe_toContinuousLinearMap

added theorem AlgHom.norm_apply_le_self

added theorem AlgHom.norm_apply_le_self_mul_norm_one

added def AlgHom.toContinuousLinearMap

added theorem AlgHom.toContinuousLinearMap_norm

added def WeakDual.CharacterSpace.equivAlgHom

added theorem WeakDual.CharacterSpace.equivAlgHom_coe

added theorem WeakDual.CharacterSpace.equivAlgHom_symm_coe

added theorem spectrum.SpectralRadius.of_subsingleton

added theorem spectrum.algebraMap_eq_of_mem

added theorem spectrum.differentiableOn_inverse_one_sub_smul

added theorem spectrum.exists_nnnorm_eq_spectralRadius

added theorem spectrum.exists_nnnorm_eq_spectralRadius_of_nonempty

added theorem spectrum.exp_mem_exp

added theorem spectrum.hasDerivAt_resolvent

added theorem spectrum.hasFPowerSeriesOnBall_inverse_one_sub_smul

added theorem spectrum.isOpen_resolventSet

added theorem spectrum.isUnit_one_sub_smul_of_lt_inv_radius

added theorem spectrum.is_bounded

added theorem spectrum.limsup_pow_nnnorm_pow_one_div_le_spectralRadius

added theorem spectrum.map_polynomial_aeval

added theorem spectrum.mem_resolventSet_of_norm_lt

added theorem spectrum.mem_resolventSet_of_norm_lt_mul

added theorem spectrum.mem_resolventSet_of_spectralRadius_lt

added theorem spectrum.norm_le_norm_mul_of_mem

added theorem spectrum.norm_le_norm_of_mem

added theorem spectrum.norm_resolvent_le_forall

added theorem spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius

added theorem spectrum.pow_norm_pow_one_div_tendsto_nhds_spectralRadius

added theorem spectrum.spectralRadius_le_liminf_pow_nnnorm_pow_one_div

added theorem spectrum.spectralRadius_le_nnnorm

added theorem spectrum.spectralRadius_le_pow_nnnorm_pow_one_div

added theorem spectrum.spectralRadius_lt_of_forall_lt

added theorem spectrum.spectralRadius_lt_of_forall_lt_of_nonempty

added theorem spectrum.spectralRadius_zero

added theorem spectrum.subset_closedBall_norm

added theorem spectrum.subset_closedBall_norm_mul