Documentation Verification Report

Extremal

📁 Source: Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/Extremal.lean

Statistics

Metric	Count
Definitions `node`, `sumNodes`	2
Theorems `coeff_eq_iff_of_forall_abs_le_one`, `coeff_le_of_forall_abs_le_one`, `eval_T_real_node`, `eval_iterate_derivative_eq_iff_of_bounded`, `eval_iterate_derivative_le_of_forall_abs_le_one`, `leadingCoeff_eq_iff_of_forall_abs_le_one`, `leadingCoeff_le_of_forall_abs_le_one`, `node_eq_neg_one`, `node_eq_one`, `node_lt`, `node_mem_Icc`, `strictAntiOn_node`, `sumNodes_eq_sumNodes_T_iff`, `sumNodes_le_sumNodes_T`, `zero_lt_prod_node_sub_node`	15
Total	17

Polynomial.Chebyshev

Definitions

Name	Category	Theorems
`node` 📖	CompOp	7 math math: `zero_lt_prod_node_sub_node`, `eval_T_real_node`, `strictAntiOn_node`, `node_eq_neg_one`, `node_mem_Icc`, `node_lt`, `node_eq_one`
`sumNodes` 📖	CompOp	2 math math: `sumNodes_le_sumNodes_T`, `sumNodes_eq_sumNodes_T_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_eq_iff_of_forall_abs_le_one` 📖	mathematical	`WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `Polynomial.degree` `Real` `Real.semiring` `WithBot.natCast` `Real.instLE` `abs` `Real.lattice` `Real.instAddGroup` `Polynomial.eval` `Real.instOne`	`Polynomial.coeff` `Real` `Real.semiring` `Monoid.toPow` `Real.instMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `T` `Real.commRing`	—	`Nat.instAtLeastTwoHAddOfNat` `sumNodes_eq_sumNodes_T_iff`
`coeff_le_of_forall_abs_le_one` 📖	mathematical	`WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `Polynomial.degree` `Real` `Real.semiring` `WithBot.natCast` `Real.instLE` `abs` `Real.lattice` `Real.instAddGroup` `Polynomial.eval` `Real.instOne`	`Real` `Real.instLE` `Polynomial.coeff` `Real.semiring` `Monoid.toPow` `Real.instMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `sumNodes_le_sumNodes_T` `le_of_lt`
`eval_T_real_node` 📖	mathematical	`Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.Iic` `Nat.instPreorder` `LocallyFiniteOrder.toLocallyFiniteOrderBot` `Nat.instOrderBot` `Nat.instLocallyFiniteOrder`	`Polynomial.eval` `Real` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Real.commRing` `node` `T` `Monoid.toPow` `Real.instMonoid` `Real.instNeg` `Real.instOne`	—	`eq_or_ne` `CharP.cast_eq_zero` `CharP.ofCharZero` `Int.instCharZero` `T_zero` `Polynomial.eval_one` `pow_zero` `Int.cast_natCast` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `one_mul` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `lt_of_le_of_ne'` `zero_le` `Nat.instCanonicallyOrderedAdd` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `Real.pi_pos` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.atom_pf` `node.eq_1` `T_real_cos` `Real.cos_nat_mul_pi`
`eval_iterate_derivative_eq_iff_of_bounded` 📖	mathematical	`Real` `Real.instLE` `Real.instOne` `WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `Polynomial.degree` `Real.semiring` `WithBot.natCast` `abs` `Real.lattice` `Real.instAddGroup` `Polynomial.eval`	`Polynomial.eval` `Real` `Real.semiring` `Nat.iterate` `Polynomial` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.semiring` `Polynomial.module` `Semiring.toModule` `LinearMap.instFunLike` `Polynomial.derivative` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Real.commRing` `T`	—	`le_of_eq` `degree_T` `Real.instIsDomain` `ZeroLEOneClass.neZero.two` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `sumNodes_eq_sumNodes_T_iff`
`eval_iterate_derivative_le_of_forall_abs_le_one` 📖	mathematical	`Real` `Real.instLE` `Real.instOne` `WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `Polynomial.degree` `Real.semiring` `WithBot.natCast` `abs` `Real.lattice` `Real.instAddGroup` `Polynomial.eval`	`Real` `Real.instLE` `Polynomial.eval` `Real.semiring` `Nat.iterate` `Polynomial` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.semiring` `Polynomial.module` `Semiring.toModule` `LinearMap.instFunLike` `Polynomial.derivative` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Real.commRing` `T`	—	`Polynomial.iterate_derivative_eq_zero_of_degree_lt` `lt_imp_lt_of_le_of_le` `le_refl` `WithBot.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithBot.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithBot.charZero` `Nat.instCharZero` `degree_T` `Real.instIsDomain` `ZeroLEOneClass.neZero.two` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Real.instIsOrderedAddMonoid` `le_of_eq` `sumNodes_le_sumNodes_T`
`leadingCoeff_eq_iff_of_forall_abs_le_one` 📖	mathematical	`WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `Polynomial.degree` `Real` `Real.semiring` `WithBot.natCast` `Real.instLE` `abs` `Real.lattice` `Real.instAddGroup` `Polynomial.eval` `Real.instOne`	`Polynomial.leadingCoeff` `Real` `Real.semiring` `Monoid.toPow` `Real.instMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `T` `Real.commRing`	—	`Nat.instAtLeastTwoHAddOfNat` `coeff_eq_iff_of_forall_abs_le_one` `CanLift.prf` `WithBot.canLift` `Mathlib.Tactic.Contrapose.contrapose₃` `Polynomial.degree_eq_bot` `Polynomial.leadingCoeff_zero` `ne_of_lt` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `ge_of_eq` `Mathlib.Tactic.Contrapose.contrapose₁` `leadingCoeff_le_of_forall_abs_le_one` `le_of_eq` `pow_lt_pow_right₀` `Real.instZeroLEOneClass` `Mathlib.Meta.NormNum.isNat_lt_true` `RCLike.charZero_rclike` `Nat.cast_one` `eq_of_le_of_ge` `Polynomial.natDegree_eq_of_degree_eq_some` `Polynomial.leadingCoeff.eq_1` `leadingCoeff_T` `Real.instIsDomain` `ZeroLEOneClass.neZero.two` `NeZero.charZero_one` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`leadingCoeff_le_of_forall_abs_le_one` 📖	mathematical	`WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `Polynomial.degree` `Real` `Real.semiring` `WithBot.natCast` `Real.instLE` `abs` `Real.lattice` `Real.instAddGroup` `Polynomial.eval` `Real.instOne`	`Real` `Real.instLE` `Polynomial.leadingCoeff` `Real.semiring` `Monoid.toPow` `Real.instMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `Real.instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `CanLift.prf` `WithBot.canLift` `Polynomial.degree_ne_bot` `WithBot.coe_le` `Polynomial.leadingCoeff.eq_1` `Polynomial.natDegree_eq_of_degree_eq_some` `le_imp_le_of_le_of_le` `coeff_le_of_forall_abs_le_one` `le_of_eq` `le_refl` `pow_le_pow_right₀` `Mathlib.Meta.NormNum.isNat_le_true` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Meta.NormNum.instAtLeastTwo`
`node_eq_neg_one` 📖	mathematical	—	`node` `Real` `Real.instNeg` `Real.instOne`	—	`mul_div_cancel_left₀` `EuclideanDomain.toMulDivCancelClass` `RCLike.charZero_rclike` `Real.cos_pi`
`node_eq_one` 📖	mathematical	—	`node` `Real` `Real.instOne`	—	`CharP.cast_eq_zero` `CharP.ofCharZero` `RCLike.charZero_rclike` `MulZeroClass.zero_mul` `zero_div` `Real.cos_zero`
`node_lt` 📖	mathematical	—	`Real` `Real.instLT` `node`	—	`strictAntiOn_node` `Finset.mem_coe` `Finset.mem_range_succ_iff`
`node_mem_Icc` 📖	mathematical	—	`Real` `Set` `Set.instMembership` `Set.Icc` `Real.instPreorder` `Real.instNeg` `Real.instOne` `node`	—	`Set.mem_Icc` `Real.neg_one_le_cos` `Real.cos_le_one`
`strictAntiOn_node` 📖	mathematical	—	`StrictAntiOn` `Real` `Nat.instPreorder` `Real.instPreorder` `node` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.range`	—	`eq_or_ne` `zero_add` `Finset.coe_singleton` `StrictAntiOn.comp_strictMonoOn` `Real.strictAntiOn_cos` `StrictMono.strictMonoOn` `StrictMono.mul_const` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `Nat.strictMono_cast` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `Real.pi_pos` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Nat.cast_pos'` `NeZero.charZero_one` `lt_of_le_of_ne'` `zero_le` `Nat.instCanonicallyOrderedAdd` `Set.mem_Icc` `Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `Nat.cast_nonneg'` `le_of_lt` `mul_div_assoc` `mul_div_cancel₀` `Nat.cast_ne_zero` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Nat.cast_le` `Finset.mem_range_succ_iff` `Finset.mem_coe` `div_pos`
`sumNodes_eq_sumNodes_T_iff` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Real.instMul` `Monoid.toPow` `Real.instMonoid` `Real.instNeg` `Real.instOne` `WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `Polynomial.degree` `Real.semiring` `WithBot.natCast` `Real.instLE` `abs` `Real.lattice` `Real.instAddGroup` `Polynomial.eval`	`sumNodes` `T` `Real` `Real.commRing`	—	`Polynomial.eq_of_degrees_lt_of_eval_finset_eq` `Real.instIsDomain` `lt_of_le_of_lt` `Nat.cast_lt` `WithBot.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithBot.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithBot.charZero` `Nat.instCharZero` `Finset.card_image_of_injOn` `StrictAntiOn.injOn` `strictAntiOn_node` `Finset.card_range` `le_refl` `degree_T` `ZeroLEOneClass.neZero.two` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Real.instIsOrderedAddMonoid` `ge_of_eq` `sumNodes.eq_1` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `Finset.mem_image` `Finset.mem_Iic` `Finset.mem_range_succ_iff` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `eval_T_real_node` `neg_pow'` `neg_neg` `one_pow` `node_mem_Icc` `le_of_lt` `Finset.sum_lt_sum` `Real.instIsOrderedCancelAddMonoid` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `lt_of_le_of_ne` `ne_of_lt` `Finset.sum_congr`
`sumNodes_le_sumNodes_T` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instMul` `Monoid.toPow` `Real.instMonoid` `Real.instNeg` `Real.instOne` `abs` `Real.lattice` `Real.instAddGroup` `Polynomial.eval` `Real.semiring`	`Real` `Real.instLE` `sumNodes` `T` `Real.commRing`	—	`sumNodes.eq_1` `Finset.sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `node_mem_Icc` `Finset.mem_Iic` `eval_T_real_node` `one_mul`
`zero_lt_prod_node_sub_node` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `Real.instMul` `Monoid.toPow` `Real.instMonoid` `Real.instNeg` `Real.instOne` `Finset.prod` `Real.instCommMonoid` `Finset.erase` `Finset.range` `Real.instSub` `node`	—	`eq_or_ne` `pow_zero` `Finset.prod_congr` `zero_add` `Finset.erase_singleton` `mul_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Finset.prod_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.instNontrivial` `mul_pos_of_neg_of_neg` `AddGroup.existsAddOfLE` `IsStrictOrderedRing.toMulPosStrictMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Real.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `neg_one_lt_zero` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `sub_neg` `node_lt` `Finset.mem_range` `sub_pos` `Finset.mem_Ioc` `Finset.prod_union` `mul_assoc` `mul_pos` `Finset.card_range` `Finset.prod_const` `Finset.prod_mul_distrib`

---

← Back to Index