Sinc

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

Statistics

Metric	Count
Definitions sinc	1
Theorems abs_sinc_le_one, continuous_sinc, neg_one_le_sinc, sin_div_le_inv_abs, sinc_apply, sinc_eq_dslope, sinc_le_inv_abs, sinc_le_one, sinc_neg, sinc_of_ne_zero, sinc_zero	11
Total	12

Real

Definitions

Name	Category	Theorems
sinc 📖	CompOp	19 math math: abs_sinc_le_one, AEMeasurable.sinc, MeasureTheory.AEStronglyMeasurable.sinc, continuous_sinc, sinc_eq_dslope, measurable_sinc, Measurable.sinc, integrable_sinc, integral_exp_mul_I_eq_sinc, MeasureTheory.integral_charFun_Icc, stronglyMeasurable_sinc, neg_one_le_sinc, sinc_le_one, sinc_zero, MeasureTheory.StronglyMeasurable.sinc, sinc_of_ne_zero, sinc_apply, sinc_neg, sinc_le_inv_abs

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_sinc_le_one 📖	mathematical	—	Real instLE abs lattice instAddGroup sinc instOne	—	sinc_zero abs_one instIsOrderedRing sinc_of_ne_zero abs_div instIsStrictOrderedRing div_le_of_le_mul₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono abs_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid covariant_swap_add_of_covariant_add zero_le_one instZeroLEOneClass one_mul abs_sin_le_abs
continuous_sinc 📖	mathematical	—	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace sinc	—	continuous_iff_continuousAt sinc_eq_dslope continuousAt_dslope_of_ne Continuous.continuousAt continuous_sin
neg_one_le_sinc 📖	mathematical	—	Real instLE instNeg instOne sinc	—	abs_le instIsOrderedAddMonoid abs_sinc_le_one
sin_div_le_inv_abs 📖	mathematical	—	Real instLE DivInvMonoid.toDiv instDivInvMonoid sin instInv abs lattice instAddGroup	—	lt_trichotomy abs_of_nonpos IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid LT.lt.le one_div le_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRing IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd div_eq_mul_inv Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul 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.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.Tactic.Ring.neg_zero Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg mul_one Mathlib.Tactic.RingNF.mul_assoc_rev add_zero mul_assoc mul_inv_cancel₀ LT.lt.ne neg_le covariant_swap_add_of_covariant_add neg_one_le_sin sin_zero div_zero abs_zero inv_zero abs_of_nonneg mul_inv_le_iff₀ inv_mul_cancel₀ LT.lt.ne' sin_le_one
sinc_apply 📖	mathematical	—	sinc Real instZero decidableEq instOne DivInvMonoid.toDiv instDivInvMonoid sin	—	—
sinc_eq_dslope 📖	mathematical	—	sinc dslope Real DenselyNormedField.toNontriviallyNormedField denselyNormedField normedAddCommGroup NormedField.toNormedSpace NontriviallyNormedField.toNormedField sin instZero	—	div_eq_inv_mul Function.update.congr_simp deriv_sin cos_zero Function.update_apply sub_zero sin_zero
sinc_le_inv_abs 📖	mathematical	—	Real instLE sinc instInv abs lattice instAddGroup	—	sinc_of_ne_zero sin_div_le_inv_abs
sinc_le_one 📖	mathematical	—	Real instLE sinc instOne	—	abs_le instIsOrderedAddMonoid abs_sinc_le_one
sinc_neg 📖	mathematical	—	sinc Real instNeg	—	neg_zero sinc_zero sinc_of_ne_zero neg_ne_zero sin_neg neg_div_neg_eq
sinc_of_ne_zero 📖	mathematical	—	sinc Real DivInvMonoid.toDiv instDivInvMonoid sin	—	—
sinc_zero 📖	mathematical	—	sinc Real instZero instOne	—	—

---

← Back to Index