LagrangeMultipliers

📁 Source: Mathlib/Analysis/Calculus/LagrangeMultipliers.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_linear_map_of_hasStrictFDerivAt, exists_multipliers_of_hasStrictFDerivAt, exists_multipliers_of_hasStrictFDerivAt_1d, linear_dependent_of_hasStrictFDerivAt, range_ne_top_of_hasStrictFDerivAt	5
Total	5

IsLocalExtrOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_linear_map_of_hasStrictFDerivAt 📖	mathematical	IsLocalExtrOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instPreorder setOf HasStrictFDerivAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField Real.instAddCommGroup Semiring.toModule Real.semiring Real.pseudoMetricSpace	Real.instAdd DFunLike.coe Module.Dual ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring RingHom.id ContinuousLinearMap ContinuousLinearMap.funLike Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id StrongDual Real.instZero	—	RingHomSurjective.ids Submodule.exists_le_ker_of_lt_top lt_top_iff_ne_top range_ne_top_of_hasStrictFDerivAt RingHomInvPair.ids Algebra.to_smulCommClass RingHomCompTriple.ids LinearEquiv.surjective LinearEquiv.map_ne_zero_iff mul_comm LinearMap.congr_fun LinearMap.range_le_ker_iff
exists_multipliers_of_hasStrictFDerivAt 📖	mathematical	IsLocalExtrOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instPreorder setOf HasStrictFDerivAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField Real.instAddCommGroup Semiring.toModule Real.semiring Real.pseudoMetricSpace	StrongDual ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.add RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Finset.sum ContinuousLinearMap.addCommMonoid Finset.univ ContinuousLinearMap.instSMul NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass Ring.uniformContinuousConstSMul Real.instRing instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing ContinuousLinearMap.zero	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul exists_linear_map_of_hasStrictFDerivAt Pi.complete Real.instCompleteSpace hasStrictFDerivAt_pi Finite.of_fintype RingHomInvPair.ids LinearEquiv.surjective ContinuousLinearMap.ext ContinuousLinearMap.coe_sum' Finset.sum_congr Finset.sum_apply LinearEquiv.piRing_symm_apply mul_comm
exists_multipliers_of_hasStrictFDerivAt_1d 📖	mathematical	IsLocalExtrOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instPreorder setOf HasStrictFDerivAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField Real.instAddCommGroup Semiring.toModule Real.semiring Real.pseudoMetricSpace	StrongDual ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.add RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousLinearMap.instSMul NonUnitalNonAssocSemiring.toDistribSMul Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass Ring.uniformContinuousConstSMul Real.instRing instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing ContinuousLinearMap.zero	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul exists_linear_map_of_hasStrictFDerivAt Real.instCompleteSpace Mathlib.Tactic.Contrapose.contrapose₄ LinearMap.ext mul_one MulZeroClass.mul_zero LinearMap.map_smul ContinuousLinearMap.ext mul_comm
linear_dependent_of_hasStrictFDerivAt 📖	mathematical	IsLocalExtrOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instPreorder setOf HasStrictFDerivAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField Real.instAddCommGroup Semiring.toModule Real.semiring Real.pseudoMetricSpace	LinearIndependent StrongDual ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Option.elim' ContinuousLinearMap.addCommMonoid RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousLinearMap.module NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Ring.uniformContinuousConstSMul Real.instRing instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	nonempty_fintype IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul instIsTopologicalAddGroupReal Fintype.linearIndependent_iff Mathlib.Tactic.Push.not_forall_eq exists_multipliers_of_hasStrictFDerivAt Fintype.sum_option Finset.sum_congr add_comm
range_ne_top_of_hasStrictFDerivAt 📖	—	IsLocalExtrOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.instPreorder setOf HasStrictFDerivAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField Real.instAddCommGroup Semiring.toModule Real.semiring Real.pseudoMetricSpace	—	—	RingHomSurjective.ids Filter.map_map nhdsWithin.eq_1 Filter.map_inf_principal_preimage HasStrictFDerivAt.map_nhds_eq_of_surj CompleteSpace.prod Real.instCompleteSpace HasStrictFDerivAt.prodMk map_snd_nhdsWithin not_nhds_le_map nhdsLT_neBot instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial nhdsGT_neBot instNoMaxOrderOfNontrivial Eq.ge

---

← Back to Index