AbsMax

📁 Source: Mathlib/Analysis/Complex/AbsMax.lean

Statistics

Metric	Count
Definitions	0
Theorems eqOn_closedBall_of_isMaxOn_norm, eqOn_closure_of_eqOn_frontier, eqOn_closure_of_isPreconnected_of_isMaxOn_norm, eqOn_of_eqOn_frontier, eqOn_of_isPreconnected_of_isMaxOn_norm, eq_const_of_exists_le, eq_const_of_exists_max, eq_of_isMaxOn_of_ball_subset, eventually_eq_of_isLocalMax_norm, eventually_eq_or_eq_zero_of_isLocalMin_norm, exists_mem_frontier_isMaxOn_norm, isOpen_setOf_mem_nhds_and_isMaxOn_norm, norm_eqOn_closedBall_of_isMaxOn, norm_eqOn_closure_of_isPreconnected_of_isMaxOn, norm_eqOn_of_isPreconnected_of_isMaxOn, norm_eq_norm_of_isMaxOn_of_ball_subset, norm_eventually_eq_of_isLocalMax, norm_le_of_forall_mem_frontier_norm_le, norm_max_aux₁, norm_max_aux₂, norm_max_aux₃	21
Total	21

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eqOn_closedBall_of_isMaxOn_norm 📖	mathematical	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup IsMaxOn Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm	Set.EqOn Metric.closedBall	—	eq_of_isMaxOn_of_ball_subset Metric.ball_subset_ball
eqOn_closure_of_eqOn_frontier 📖	mathematical	Bornology.IsBounded PseudoMetricSpace.toBornology SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField Set.EqOn frontier UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	closure	—	norm_le_of_forall_mem_frontier_norm_le DiffContOnCl.sub sub_self norm_zero
eqOn_closure_of_isPreconnected_of_isMaxOn_norm 📖	mathematical	IsPreconnected UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup IsOpen DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField Set Set.instMembership IsMaxOn Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm	Set.EqOn closure	—	Set.EqOn.of_subset_closure TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace eqOn_of_isPreconnected_of_isMaxOn_norm DiffContOnCl.differentiableOn DiffContOnCl.continuousOn continuousOn_const subset_closure Set.Subset.rfl
eqOn_of_eqOn_frontier 📖	—	Bornology.IsBounded PseudoMetricSpace.toBornology SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField Set.EqOn frontier UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	—	—	Set.EqOn.mono subset_closure eqOn_closure_of_eqOn_frontier
eqOn_of_isPreconnected_of_isMaxOn_norm 📖	mathematical	IsPreconnected UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup IsOpen DifferentiableOn Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule instNormedField Set Set.instMembership IsMaxOn Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm	Set.EqOn	—	norm_eqOn_of_isPreconnected_of_isMaxOn DifferentiableOn.add_const IsMaxOn.norm_add_self eq_of_norm_eq_of_norm_add_eq SameRay.norm_add SameRay.rfl Real.instIsStrictOrderedRing
eq_const_of_exists_le 📖	mathematical	DifferentiableOn Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule instNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Metric.ball NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Real Real.instLE Real.instZero Real.instLT Set Set.instMembership Metric.closedBall Norm.norm NormedAddCommGroup.toNorm	Set.EqOn	—	IsCompact.exists_isMaxOn instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid ProperSpace.isCompact_closedBall Metric.nonempty_closedBall ContinuousOn.norm ContinuousOn.mono DifferentiableOn.continuousOn IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Metric.closedBall_subset_ball eq_const_of_exists_max LE.le.trans Metric.mem_ball_self LE.le.trans_lt
eq_const_of_exists_max 📖	mathematical	DifferentiableOn Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule instNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Metric.ball NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Set Set.instMembership IsMaxOn Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm	Set.EqOn	—	eqOn_of_isPreconnected_of_isMaxOn_norm Convex.isPreconnected IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul convex_ball Metric.isOpen_ball
eq_of_isMaxOn_of_ball_subset 📖	—	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField IsMaxOn Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm Set Set.instHasSubset Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Dist.dist PseudoMetricSpace.toDist	—	—	norm_eq_norm_of_isMaxOn_of_ball_subset DiffContOnCl.add_const IsMaxOn.norm_add_self eq_of_norm_eq_of_norm_add_eq SameRay.norm_add SameRay.rfl Real.instIsStrictOrderedRing
eventually_eq_of_isLocalMax_norm 📖	—	Filter.Eventually DifferentiableAt Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule instNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace nhds IsLocalMax Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm	—	—	Filter.HasBasis.eventually_iff Metric.nhds_basis_closedBall Filter.Eventually.and eqOn_closedBall_of_isMaxOn_norm DifferentiableOn.diffContOnCl DifferentiableAt.differentiableWithinAt Metric.closure_ball_subset_closedBall Metric.ball_subset_closedBall
eventually_eq_or_eq_zero_of_isLocalMin_norm 📖	mathematical	Filter.Eventually DifferentiableAt Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule instNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace addCommGroup instModuleSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing nhds IsLocalMin Real Real.instPreorder Norm.norm instNorm	instZero	—	ContinuousAt.eventually_ne T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace DifferentiableAt.continuousAt IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology Filter.Eventually.self_of_nhds IsLocalMin.inv Real.instIsStrictOrderedRing Filter.Eventually.mono norm_pos_iff IsLocalMax.congr Filter.Eventually.of_forall norm_inv Filter.mp_mem Filter.univ_mem' DifferentiableAt.inv eventually_eq_of_isLocalMax_norm UniformConvexSpace.toStrictConvexSpace InnerProductSpace.toUniformConvexSpace
exists_mem_frontier_isMaxOn_norm 📖	mathematical	Bornology.IsBounded PseudoMetricSpace.toBornology SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.Nonempty DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField	Set Set.instMembership frontier UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace IsMaxOn Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm closure	—	Bornology.IsBounded.isCompact_closure FiniteDimensional.proper_real Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.complexToReal Module.Projective.of_free Module.Free.of_divisionRing IsCompact.exists_isMaxOn instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Set.Nonempty.closure ContinuousOn.norm DiffContOnCl.continuousOn Set.mem_union closure_eq_interior_union_frontier ne_top_of_le_ne_top IsCompact.ne_univ RealNormedSpace.noncompactSpace interior_subset_closure exists_mem_frontier_infDist_compl_eq_dist frontier_interior_subset LE.le.trans_eq Membership.mem.out norm_eq_norm_of_isMaxOn_of_ball_subset IsMaxOn.on_subset subset_closure dist_comm HasSubset.Subset.trans Set.instIsTransSubset Metric.ball_infDist_compl_subset interior_subset
isOpen_setOf_mem_nhds_and_isMaxOn_norm 📖	mathematical	DifferentiableOn Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule instNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	IsOpen setOf Set Filter Filter.instMembership nhds IsMaxOn Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm	—	isOpen_iff_mem_nhds Filter.Eventually.and eventually_eventually_nhds DifferentiableOn.eventually_differentiableAt Filter.Eventually.mono norm_eventually_eq_of_isLocalMax IsMaxOn.isLocalMax le_trans Membership.mem.out Eq.ge
norm_eqOn_closedBall_of_isMaxOn 📖	mathematical	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup IsMaxOn Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm	Set.EqOn Metric.closedBall	—	eq_or_ne dist_comm Metric.mem_closedBall Differentiable.add_const Differentiable.smul_const NormedSpace.toIsBoundedSMul IsScalarTower.left differentiable_id dist_zero_right CStarRing.norm_of_mem_unitary RCLike.instCStarRing instNontrivial SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass Set.MapsTo.mono LipschitzWith.mapsTo_ball lipschitzWith_lineMap nndist_eq_zero Set.Subset.rfl AffineMap.lineMap_apply_zero mul_one Metric.ball_subset_ball norm_max_aux₃ DiffContOnCl.comp Differentiable.diffContOnCl IsMaxOn.comp_mapsTo AffineMap.lineMap_apply_one
norm_eqOn_closure_of_isPreconnected_of_isMaxOn 📖	mathematical	IsPreconnected UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup IsOpen DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField Set Set.instMembership IsMaxOn Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm	Set.EqOn closure	—	Set.EqOn.of_subset_closure TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace norm_eqOn_of_isPreconnected_of_isMaxOn DiffContOnCl.differentiableOn ContinuousOn.norm DiffContOnCl.continuousOn continuousOn_const subset_closure Set.Subset.rfl
norm_eqOn_of_isPreconnected_of_isMaxOn 📖	mathematical	IsPreconnected UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup IsOpen DifferentiableOn Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule instNormedField Set Set.instMembership IsMaxOn Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm	Set.EqOn	—	le_antisymm IsOpen.mem_nhds_iff isOpen_setOf_mem_nhds_and_isMaxOn_norm ContinuousOn.isOpen_inter_preimage ContinuousOn.norm DifferentiableOn.continuousOn IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul isOpen_ne T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace Set.disjoint_left LE.le.trans_eq Membership.mem.out eq_or_ne IsPreconnected.subset_left_of_subset_union
norm_eq_norm_of_isMaxOn_of_ball_subset 📖	—	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField IsMaxOn Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm Set Set.instHasSubset Metric.ball SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Dist.dist PseudoMetricSpace.toDist	—	—	norm_eqOn_closedBall_of_isMaxOn DiffContOnCl.mono IsMaxOn.on_subset Metric.mem_closedBall le_rfl
norm_eventually_eq_of_isLocalMax 📖	—	Filter.Eventually DifferentiableAt Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule instNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace nhds IsLocalMax Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm	—	—	Filter.HasBasis.eventually_iff Metric.nhds_basis_closedBall Filter.Eventually.and norm_eqOn_closedBall_of_isMaxOn DifferentiableOn.diffContOnCl DifferentiableAt.differentiableWithinAt Metric.closure_ball_subset_closedBall Metric.ball_subset_closedBall
norm_le_of_forall_mem_frontier_norm_le 📖	—	Bornology.IsBounded PseudoMetricSpace.toBornology SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField Real Real.instLE Norm.norm NormedAddCommGroup.toNorm Set Set.instMembership closure UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	—	—	Set.mem_union Set.union_comm closure_eq_self_union_frontier exists_ne Differentiable.add_const Differentiable.smul_const NormedSpace.toIsBoundedSMul IsScalarTower.left differentiable_id antilipschitzWith_lineMap DiffContOnCl.comp Differentiable.diffContOnCl Set.mapsTo_preimage AffineMap.lineMap_apply_zero exists_mem_frontier_isMaxOn_norm instNontrivial Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self AntilipschitzWith.isBounded_preimage subset_closure Continuous.frontier_preimage_subset Differentiable.continuous IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul
norm_max_aux₁ 📖	—	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField instNormedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Metric.ball SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Dist.dist PseudoMetricSpace.toDist IsMaxOn Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm Metric.closedBall	—	—	Metric.mem_closedBall le_rfl LE.le.antisymm isMaxOn_iff not_lt dist_pos LT.lt.ne Nat.instAtLeastTwoHAddOfNat Metric.sphere_subset_closedBall circleIntegral.norm_integral_lt_of_norm_le_const_of_lt ContinuousOn.smul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ContinuousOn.inv₀ IsTopologicalDivisionRing.toContinuousInv₀ NormedDivisionRing.to_isTopologicalDivisionRing ContinuousOn.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup continuousOn_id continuousOn_const sub_ne_zero Metric.ne_of_mem_sphere LT.lt.ne' ContinuousOn.mono DiffContOnCl.continuousOn_ball le_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing norm_smul NormedSpace.toNormSMulClass norm_inv mul_comm mul_inv_cancel_left₀ div_eq_inv_mul div_lt_div_iff_of_pos_right mul_div_cancel₀ mul_assoc DiffContOnCl.circleIntegral_sub_inv_smul Metric.mem_ball_self norm_mul norm_ofNat norm_real norm_I mul_one IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero Real.instIsDomain IsCancelMulZero.toIsLeftCancelMulZero Real.instIsOrderedAddMonoid LT.lt.le Real.pi_pos RCLike.charZero_rclike
norm_max_aux₂ 📖	—	DiffContOnCl Complex DenselyNormedField.toNontriviallyNormedField instDenselyNormedField instNormedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Metric.ball SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField Dist.dist PseudoMetricSpace.toDist IsMaxOn Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm Metric.closedBall	—	—	SeminormedAddCommGroup.to_isUniformAddGroup IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul UniformSpace.Completion.norm_coe norm_max_aux₁ UniformSpace.Completion.completeSpace Differentiable.comp_diffContOnCl ContinuousLinearMap.differentiable
norm_max_aux₃ 📖	—	Dist.dist Complex PseudoMetricSpace.toDist SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField DiffContOnCl DenselyNormedField.toNontriviallyNormedField instDenselyNormedField instNormedAddCommGroup InnerProductSpace.toNormedSpace instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Metric.ball IsMaxOn Real Real.instPreorder Norm.norm NormedAddCommGroup.toNorm	—	—	eq_or_ne norm_max_aux₂ IsMaxOn.closure HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid ContinuousOn.norm DiffContOnCl.continuousOn closure_ball dist_ne_zero

---

← Back to Index