Bounds

📁 Source: Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean

Statistics

Metric	Count
Definitions	0
Theorems abs_cos_sub_cos_le, abs_sin_le_abs, abs_sin_lt_abs, abs_sin_sub_sin_le, cos_le_one_div_sqrt_sq_add_one, cos_le_one_sub_mul_cos_sq, cos_lt_one_div_sqrt_sq_add_one, deriv_tan_sub_id, enorm_exp_I_mul_ofReal_sub_one_le, le_sin, le_sin_mul, le_tan, lipschitzWith_cos, lipschitzWith_sin, lt_sin, lt_sin_mul, lt_tan, mul_abs_le_abs_sin, mul_le_sin, mul_lt_sin, nnnorm_exp_I_mul_ofReal_sub_one_le, norm_exp_I_mul_ofReal_sub_one_le, one_add_mul_le_cos, one_sub_mul_le_cos, one_sub_sq_div_two_le_cos, one_sub_sq_div_two_lt_cos, sin_gt_sub_cube, sin_le, sin_le_mul, sin_lt, sin_sq_le_sq, sin_sq_lt_sq	32
Total	32

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_cos_sub_cos_le 📖	mathematical	—	Real instLE abs lattice instAddGroup instSub cos	—	edist_dist one_mul lipschitzWith_cos
abs_sin_le_abs 📖	mathematical	—	Real instLE abs lattice instAddGroup sin	—	sq_le_sq instIsStrictOrderedRing sin_sq_le_sq
abs_sin_lt_abs 📖	mathematical	—	Real instLT abs lattice instAddGroup sin	—	sq_lt_sq instIsStrictOrderedRing sin_sq_lt_sq
abs_sin_sub_sin_le 📖	mathematical	—	Real instLE abs lattice instAddGroup instSub sin	—	edist_dist one_mul lipschitzWith_sin
cos_le_one_div_sqrt_sq_add_one 📖	mathematical	Real instLE instNeg DivInvMonoid.toDiv instDivInvMonoid instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat pi	cos instOne sqrt instAdd Monoid.toNatPow instMonoid	—	Nat.instAtLeastTwoHAddOfNat eq_or_ne cos_zero zero_pow Nat.instCharZero zero_add sqrt_one div_self NeZero.charZero_one RCLike.charZero_rclike LT.lt.le cos_lt_one_div_sqrt_sq_add_one
cos_le_one_sub_mul_cos_sq 📖	mathematical	Real instLE abs lattice instAddGroup pi	cos instSub instOne instMul DivInvMonoid.toDiv instDivInvMonoid instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat Monoid.toNatPow instMonoid	—	Nat.instAtLeastTwoHAddOfNat div_mul_div_cancel₀' RCLike.charZero_rclike mul_le_sin Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing Mathlib.Meta.Positivity.pos_of_isNat instIsOrderedRing instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Nat.cast_one Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.sub_nonpos_of_le abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Meta.NormNum.isNat_lt_true LE.le.trans_eq pow_le_pow_left₀ IsOrderedRing.toPosMulMono IsOrderedRing.toMulPosMono pi_pos sin_sq_eq_half_sub Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.RingNF.nat_rawCast_1 Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg Mathlib.Tactic.RingNF.mul_assoc_rev add_zero Mathlib.Tactic.RingNF.add_neg Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.neg_congr CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.IsRat.neg_to_eq Mathlib.Meta.NormNum.isRat_div Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isRat_neg CancelDenoms.mul_subst CancelDenoms.pow_subst Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.one_natPow CancelDenoms.add_subst CancelDenoms.neg_subst Mathlib.Tactic.Linarith.mul_nonpos mul_one Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Tactic.Ring.atom_pf' Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz pow_one Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Tactic.RingNF.nnrat_rawCast Mathlib.Tactic.RingNF.rat_rawCast_neg Mathlib.Tactic.Linarith.without_one_mul cos_neg Even.neg_pow abs_neg neg_nonneg le_of_not_ge
cos_lt_one_div_sqrt_sq_add_one 📖	mathematical	Real instLE instNeg DivInvMonoid.toDiv instDivInvMonoid instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat pi	instLT cos instOne sqrt instAdd Monoid.toNatPow instMonoid	—	Nat.instAtLeastTwoHAddOfNat lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le instIsStrictOrderedRing neg_neg_of_pos instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le instIsOrderedRing sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono IsOrderedAddMonoid.toAddLeftMono lt_or_ge cos_pos_of_mem_Ioo Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Meta.NormNum.isNat_lt_true RCLike.charZero_rclike CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.isNat_mul CancelDenoms.neg_subst Mathlib.Tactic.Linarith.mul_nonpos abs_of_nonneg cos_nonneg_of_mem_Icc le_of_not_gt LT.lt.le one_div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono sqrt_nonneg sq_lt_sq div_pow one_pow sq_sqrt lt_one_div pow_pos instZeroLEOneClass inv_one_add_tan_sq LT.lt.ne' one_div inv_inv add_comm add_lt_add_iff_left IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le abs_of_pos tan_nonneg_of_nonneg_of_le_pi_div_two lt_tan lt_of_le_of_lt cos_nonpos_of_pi_div_two_le_of_le Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Linarith.add_lt_of_le_of_neg CancelDenoms.mul_subst CancelDenoms.add_subst one_div_pos sqrt_pos_of_pos lt_or_lt_iff_ne cos_neg neg_sq
deriv_tan_sub_id 📖	mathematical	—	deriv Real DenselyNormedField.toNontriviallyNormedField denselyNormedField instAddCommGroup NormedSpace.toModule normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instSub tan DivInvMonoid.toDiv instDivInvMonoid instOne Monoid.toNatPow instMonoid cos	—	HasDerivAt.deriv IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul HasDerivAt.congr_simp one_div HasDerivAt.add hasDerivAt_tan HasDerivAt.neg hasDerivAt_id
enorm_exp_I_mul_ofReal_sub_one_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENorm.enorm Complex ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SeminormedAddGroup.toContinuousENorm Complex.instSub Complex.exp Complex.instMul Complex.I Complex.ofReal Complex.instOne Real normedCommRing	—	enorm_norm enorm_of_nonneg norm_nonneg ENNReal.ofReal_le_ofReal norm_exp_I_mul_ofReal_sub_one_le
le_sin 📖	mathematical	Real instLE instZero	sin	—	sin_neg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid covariant_swap_add_of_covariant_add sin_le neg_nonneg
le_sin_mul 📖	mathematical	Real instLE instZero instOne	sin instMul DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat sub_add_cancel sin_zero MulZeroClass.mul_zero sin_pi_div_two mul_comm one_mul zero_add StrictConcaveOn.concaveOn strictConcaveOn_sin_Icc le_rfl LT.lt.le pi_pos pi_div_two_pos half_le_self PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid
le_tan 📖	mathematical	Real instLE instZero instLT DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	tan	—	Nat.instAtLeastTwoHAddOfNat eq_or_lt_of_le tan_zero le_refl le_of_lt lt_tan
lipschitzWith_cos 📖	mathematical	—	LipschitzWith Real EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace metricSpace NNReal instOneNNReal cos	—	lipschitzWith_of_nnnorm_deriv_le differentiable_cos deriv_cos' nnnorm_neg abs_sin_le_one
lipschitzWith_sin 📖	mathematical	—	LipschitzWith Real EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace metricSpace NNReal instOneNNReal sin	—	lipschitzWith_of_nnnorm_deriv_le differentiable_sin deriv_sin abs_cos_le_one
lt_sin 📖	mathematical	Real instLT instZero	sin	—	sin_neg IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add sin_lt neg_pos
lt_sin_mul 📖	mathematical	Real instLT instZero instOne	sin instMul DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat sub_add_cancel sin_zero MulZeroClass.mul_zero sin_pi_div_two mul_comm one_mul zero_add strictConcaveOn_sin_Icc le_rfl LT.lt.le pi_pos pi_div_two_pos half_le_self PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing LT.lt.ne sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid
lt_tan 📖	mathematical	Real instLT instZero DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	tan	—	Nat.instAtLeastTwoHAddOfNat interior_Ico instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing instNoMinOrderOfNontrivial instIsOrderedRing instNontrivial div_pos pi_pos two_pos instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid cos_pos_of_mem_Ioo Set.Ico_subset_Ioo_left neg_lt_zero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd sin_pos_of_mem_Ioo Set.Ioo_subset_Ioo_right div_le_self LT.lt.le one_le_two ContinuousOn.mono continuousOn_tan LT.lt.ne' ContinuousOn.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal continuousOn_id interior_subset deriv_tan_sub_id one_div IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add Nat.cast_one lt_of_le_of_ne cos_sq_le_one cos_sq' isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass lt_inv_comm₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono zero_lt_one sq AddGroup.existsAddOfLE contravariant_lt_of_covariant_le inv_one strictMonoOn_of_deriv_pos convex_Ico instIsOrderedCancelAddMonoid IsStrictOrderedModule.toPosSMulStrictMono IsStrictOrderedRing.toIsStrictOrderedModule Set.left_mem_Ico tan_zero sub_zero
mul_abs_le_abs_sin 📖	mathematical	Real instLE abs lattice instAddGroup DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	instMul sin	—	Nat.instAtLeastTwoHAddOfNat abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid LE.le.trans mul_le_sin le_abs_self abs_neg sin_neg neg_nonneg le_of_not_ge
mul_le_sin 📖	mathematical	Real instLE instZero DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	instMul sin	—	Nat.instAtLeastTwoHAddOfNat inv_div mul_inv_cancel_left₀ RCLike.charZero_rclike le_sin_mul mul_nonneg IsOrderedRing.toPosMulMono instIsOrderedRing inv_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing LT.lt.le pi_div_two_pos div_eq_inv_mul div_le_one
mul_lt_sin 📖	mathematical	Real instLT instZero DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	instMul sin	—	Nat.instAtLeastTwoHAddOfNat inv_div mul_inv_cancel_left₀ RCLike.charZero_rclike lt_sin_mul mul_pos IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE pi_div_two_pos div_eq_inv_mul div_lt_one
nnnorm_exp_I_mul_ofReal_sub_one_le 📖	mathematical	—	NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal NNNorm.nnnorm Complex SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instSub Complex.exp Complex.instMul Complex.I Complex.ofReal Complex.instOne Real normedCommRing	—	ENNReal.coe_le_coe enorm_exp_I_mul_ofReal_sub_one_le
norm_exp_I_mul_ofReal_sub_one_le 📖	mathematical	—	Real instLE Norm.norm Complex Complex.instNorm Complex.instSub Complex.exp Complex.instMul Complex.I Complex.ofReal Complex.instOne norm	—	Nat.instAtLeastTwoHAddOfNat Complex.norm_exp_I_mul_ofReal_sub_one norm_mul NormedDivisionRing.toNormMulClass norm_ofNat mul_le_mul_iff_of_pos_left IsOrderedRing.toPosMulMono instIsOrderedRing PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing zero_lt_two instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid abs_sin_le_abs abs_div Nat.abs_ofNat norm_eq_abs Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz
one_add_mul_le_cos 📖	mathematical	Real instLE instNeg DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instZero	instAdd instOne instMul cos	—	Nat.instAtLeastTwoHAddOfNat mul_neg sub_neg_eq_add cos_neg one_sub_mul_le_cos le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Linarith.add_lt_of_le_of_neg instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le instIsOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Nat.cast_one Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Meta.NormNum.IsNat.to_raw_eq CancelDenoms.sub_subst CancelDenoms.neg_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Tactic.Linarith.mul_neg
one_sub_mul_le_cos 📖	mathematical	Real instLE instZero DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	instSub instOne instMul cos	—	Nat.instAtLeastTwoHAddOfNat AddGroup.toOrderedSub covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid mul_sub div_mul_div_cancel₀' RCLike.charZero_rclike div_self LT.lt.ne' pi_pos sin_pi_div_two_sub mul_le_sin IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le
one_sub_sq_div_two_le_cos 📖	mathematical	—	Real instLE instSub instOne DivInvMonoid.toDiv instDivInvMonoid Monoid.toNatPow instMonoid instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat cos	—	Nat.instAtLeastTwoHAddOfNat eq_or_ne zero_pow Nat.instCharZero zero_div sub_zero cos_zero LT.lt.le one_sub_sq_div_two_lt_cos
one_sub_sq_div_two_lt_cos 📖	mathematical	—	Real instLT instSub instOne DivInvMonoid.toDiv instDivInvMonoid Monoid.toNatPow instMonoid instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat cos	—	Nat.instAtLeastTwoHAddOfNat LT.lt.trans_eq' sin_sq_lt_sq Mathlib.Meta.Positivity.div_ne_zero_of_ne_zero_of_pos Mathlib.Meta.Positivity.pos_of_isNat instIsOrderedRing instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo sin_sq_eq_half_sub lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Nat.cast_one Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le instIsStrictOrderedRing CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsRat.neg_to_eq Mathlib.Meta.NormNum.isRat_div Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isRat_neg CancelDenoms.sub_subst CancelDenoms.add_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNat_mul CancelDenoms.mul_subst CancelDenoms.neg_subst CancelDenoms.pow_subst Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.one_natPow Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Tactic.Ring.atom_pf' Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one add_zero Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Tactic.RingNF.nnrat_rawCast Mathlib.Tactic.RingNF.rat_rawCast_neg Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Meta.NormNum.isNNRat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le
sin_gt_sub_cube 📖	mathematical	Real instLT instZero instLE instOne	instSub DivInvMonoid.toDiv instDivInvMonoid Monoid.toNatPow instMonoid instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat sin	—	abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid LT.lt.le Nat.instAtLeastTwoHAddOfNat neg_le_of_abs_le sin_bound lt_of_lt_of_le Mathlib.Meta.NormNum.instAtLeastTwo div_eq_mul_inv Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_sub Mathlib.Meta.NormNum.IsNNRat.to_isRat add_comm sub_add sub_neg_eq_add sub_lt_sub_iff_left IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add lt_sub_iff_add_lt' mul_lt_mul' IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing IsOrderedRing.toMulPosMono instIsOrderedRing pow_le_pow_of_le_one IsOrderedRing.toPosMulMono Mathlib.Meta.NormNum.isNNRat_lt_true instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isRat_le_true Nat.cast_zero pow_pos instZeroLEOneClass le_sub_iff_add_le
sin_le 📖	mathematical	Real instLE instZero	sin	—	LE.le.eq_or_lt sin_zero LT.lt.le sin_lt
sin_le_mul 📖	mathematical	Real instLE instNeg DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instZero	sin instMul	—	Nat.instAtLeastTwoHAddOfNat mul_neg sin_neg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid covariant_swap_add_of_covariant_add mul_le_sin neg_nonneg neg_le
sin_lt 📖	mathematical	Real instLT instZero	sin	—	lt_or_ge LE.le.trans_lt sin_le_one abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid LT.lt.le Nat.instAtLeastTwoHAddOfNat le_of_abs_le sin_bound sub_le_iff_le_add' sub_add sub_lt_self_iff IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add div_eq_mul_inv mul_lt_mul' IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing IsOrderedRing.toMulPosMono instIsOrderedRing pow_le_pow_of_le_one IsOrderedRing.toPosMulMono Mathlib.Meta.NormNum.isNNRat_lt_true instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.isRat_le_true Mathlib.Meta.NormNum.IsNNRat.to_isRat Nat.cast_zero pow_pos instZeroLEOneClass
sin_sq_le_sq 📖	mathematical	—	Real instLE Monoid.toNatPow instMonoid sin	—	eq_or_ne sin_zero zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat LT.lt.le sin_sq_lt_sq
sin_sq_lt_sq 📖	mathematical	—	Real instLT Monoid.toNatPow instMonoid sin	—	le_or_gt pow_lt_pow_left₀ IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing IsOrderedRing.toMulPosMono instIsOrderedRing sin_lt sin_nonneg_of_nonneg_of_le_pi LT.lt.le le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.add_neg neg_neg_of_pos instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt two_le_pi Nat.instCharZero LE.le.trans_lt sin_sq_le_one one_lt_sq_iff₀ instZeroLEOneClass sin_neg Even.neg_pow neg_ne_zero neg_pos_of_neg IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Ne.lt_of_le

---

← Back to Index