QuadraticMap

📁 Source: Mathlib/Analysis/Calculus/LineDeriv/QuadraticMap.lean

Statistics

Metric	Count
Definitions QuadraticMap	1
Theorems hasLineDerivAt, lineDeriv, lineDifferentiableAt	3
Total	4

QuadraticMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasLineDerivAt 📖	mathematical	—	HasLineDerivAt DFunLike.coe QuadraticMap Semifield.toCommSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule instFunLike polar NormedAddCommGroup.toAddCommGroup	—	HasDerivAt.congr_simp map_add map_smul polar_smul_right IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul MulZeroClass.mul_zero smul_zero mul_one add_zero zero_smul one_smul zero_add HasDerivAt.add hasDerivAt_const HasDerivAt.smul IsScalarTower.left HasDerivAt.mul hasDerivAt_id
lineDeriv 📖	mathematical	—	lineDeriv DFunLike.coe QuadraticMap Semifield.toCommSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule instFunLike polar NormedAddCommGroup.toAddCommGroup	—	HasLineDerivAt.lineDeriv hasLineDerivAt
lineDifferentiableAt 📖	mathematical	—	LineDifferentiableAt DFunLike.coe QuadraticMap Semifield.toCommSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule instFunLike	—	HasLineDerivAt.lineDifferentiableAt hasLineDerivAt

(root)

Definitions

Name	Category	Theorems
QuadraticMap 📖	CompData	155 math math: QuadraticMap.polar_zero_left, QuadraticMap.not_anisotropic_iff_exists, QuadraticMap.smul_toBilin, QuadraticMap.lineDeriv, QuadraticMap.sum_polar_sub_repr_sq, QuadraticMap.canLift, LinearMap.BilinMap.polar_toQuadraticMap, QuadraticMap.map_add_self, LinearMap.BilinMap.toQuadraticMap_add, LinearEquiv.congrQuadraticMap_symm, QuadraticMap.Isometry.proj_comp_single_of_same, QuadraticMap.neg_apply, LinearMap.BilinMap.toQuadraticMapAddMonoidHom_apply, QuadraticMap.map_smul_of_tower, LinearMap.BilinMap.toQuadraticMap_zero, QuadraticMap.toBilinHom_apply, QuadraticMap.add_linMulLin, QuadraticMap.associated_eq_self_apply, QuadraticMap.polar_prod, QuadraticMap.associated_rightInverse, QuadraticMap.sum_apply, LinearEquiv.congrQuadraticMap_refl, QuadraticMap.instIsScalarTower, QuadraticMap.linMulLin_apply, QuadraticMap.discr_smul, QuadraticMap.polar_neg_left, QuadraticMap.ofPolar_apply, QuadraticMap.add_toBilin, QuadraticMap.ext_iff, QuadraticMap.associated_prod, QuadraticMap.zero_apply, QuadraticMap.map_smul, LinearMap.BilinMap.toQuadraticMap_eq_zero, QuadraticMap.associated_apply, QuadraticMap.map_zero, QuadraticMap.Isometry.ofEq_rfl, QuadraticMap.map_finsuppSum, QuadraticMap.Isometry.snd_comp_inl, QuadraticMap.polarBilin_injective, QuadraticMap.comp_apply, QuadraticMap.toQuadraticMap_associated, QuadraticMap.IsOrtho.all, QuadraticMap.isOrtho_def, QuadraticMap.polar_add_left, QuadraticMap.proj_apply, QuadraticMap.polar_smul_left_of_tower, QuadraticMap.toBilin_apply, QuadraticMap.associated_left_inverse, QuadraticMap.evalAddMonoidHom_apply, QuadraticMap.polar_self, QuadraticMap.Isometry.snd_apply, QuadraticMap.prod_apply, QuadraticForm.dualProd_apply, LinearMap.compQuadraticMap_polar, QuadraticMap.associated_tmul, QuadraticMap.zeroHomClass, QuadraticMap.associated_toQuadraticMap, QuadraticMap.IsometryEquiv.map_app, QuadraticMap.coeFn_add, QuadraticMap.two_nsmul_associated, QuadraticMap.map_sub, QuadraticMap.associated_left_inverse', QuadraticMap.Isometry.map_app, QuadraticMap.instSMulCommClass, baseChange_ext_iff, QuadraticMap.sub_apply, QuadraticMap.smul_apply, QuadraticMap.PosDef.nonneg, QuadraticMap.Isometry.proj_comp_single_of_ne, QuadraticMap.coeFnAddMonoidHom_apply, QuadraticMap.toQuadraticMap_polarBilin, QuadraticMap.map_finsuppSum', QuadraticMap.sq_apply, LinearMap.BilinMap.toQuadraticMap_smul, LinearMap.BilinMap.toQuadraticMapLinearMap_apply, QuadraticMap.polar_smul_left, QuadraticMap.pi_apply_single, LinearMap.BilinMap.toQuadraticMap_surjective, QuadraticMap.PosDef.le_zero_iff, LinearMap.BilinMap.toQuadraticMap_list_sum, QuadraticForm.toDualProd_apply, LinearMap.compQuadraticMap_apply, QuadraticMap.canLift', QuadraticMap.Isometry.proj_apply, QuadraticMap.Isometry.fst_apply, QuadraticMap.map_add_add_add_map, QuadraticMap.lineDifferentiableAt, QuadraticMap.coeFn_sub, QuadraticMap.Isometry.fst_comp_inl, QuadraticMap.PosDef.add, LinearMap.BilinMap.toQuadraticMap_multiset_sum, QuadraticMap.map_sum', QuadraticMap.map_neg, QuadraticMap.weightedSumSquares_apply, QuadraticMap.coe_associatedHom, QuadraticMap.pi_apply, QuadraticMap.coeFn_neg, LinearEquiv.congrQuadraticMap_symm_apply, LinearMap.compQuadraticMap'_apply, QuadraticMap.Isometry.map_app', QuadraticMap.polar_neg_right, QuadraticMap.polar_sub_right, QuadraticMap.associated_linMulLin, QuadraticForm.associated_isSymm, LinearMap.BilinMap.toQuadraticMap_sum, QuadraticMap.Isometry.fst_comp_inr, QuadraticMap.polar_add_right, QuadraticMap.apply_linearCombination', QuadraticMap.Anisotropic.eq_zero_iff, QuadraticMap.associated_sq, QuadraticMap.associated_comp, QuadraticMap.associated_isOrtho, QuadraticMap.polar_sub_left, QuadraticMap.IsOrtho.polar_eq_zero, QuadraticMap.Ring.associated_pi, QuadraticMap.toFun_eq_coe, QuadraticMap.IsometryEquiv.map_app', QuadraticMap.polar_smul_right_of_tower, QuadraticMap.apply_linearCombination, QuadraticMap.coeFn_sum, CliffordAlgebra.changeForm.associated_neg_proof, QuadraticMap.nonneg_prod_iff, QuadraticMap.PosDef.smul, QuadraticMap.separatingLeft_of_anisotropic, QuadraticMap.nonneg_pi_iff, LinearMap.BilinMap.toQuadraticMap_apply, QuadraticMap.map_sum, QuadraticMap.posDef_iff_nonneg, QuadraticMap.sum_repr_sq_add_sum_repr_mul_polar, LinearEquiv.congrQuadraticMap_apply, QuadraticMap.coeFn_zero, QuadraticMap.coe_mk, QuadraticMap.exists_companion, QuadraticForm.associated_tmul, QuadraticMap.polarSym2_map_smul, QuadraticMap.coeFn_smul, QuadraticMap.tensorDistrib_tmul, QuadraticMap.associated_flip, QuadraticMap.Ring.polar_pi, QuadraticMap.polar_smul_right, QuadraticMap.associated_isSymm, LinearMap.BilinMap.toQuadraticMap_neg, QuadraticForm.associated_baseChange, QuadraticMap.polar_zero_right, QuadraticMap.basisRepr_apply, QuadraticMap.restrictScalars_apply, QuadraticMap.toMatrix'_smul, LinearMap.dualProd.toQuadraticForm, QuadraticMap.polarBilin_apply_apply, LinearMap.BilinMap.toQuadraticMap_sub, QuadraticMap.linMulLin_add, QuadraticMap.add_apply, QuadraticMap.congr_fun, QuadraticMap.Isometry.snd_comp_inr, QuadraticMap.hasLineDerivAt

---

← Back to Index