EulerSineProd

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

Statistics

Metric	Count
Definitions	0
Theorems tendsto_euler_sin_prod, antideriv_cos_comp_const_mul, antideriv_sin_comp_const_mul, integral_cos_mul_cos_pow, integral_cos_mul_cos_pow_aux, integral_cos_mul_cos_pow_even, integral_cos_pow_eq, integral_cos_pow_pos, integral_sin_mul_sin_mul_cos_pow_eq, sin_pi_mul_eq, tendsto_integral_cos_pow_mul_div, tendsto_euler_sin_prod	12
Total	12

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendsto_euler_sin_prod 📖	mathematical	—	Filter.Tendsto Complex instMul ofReal Real.pi Finset.prod CommRing.toCommMonoid commRing Finset.range instSub instOne DivInvMonoid.toDiv instDivInvMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiring instAdd instNatCast Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing instNormedField sin	—	Nat.instAtLeastTwoHAddOfNat Filter.Tendsto.congr EulerSine.sin_pi_mul_eq tendsto_const_nhds mul_one Filter.tendsto_mul_iff_of_ne_zero IsTopologicalDivisionRing.toContinuousInv₀ NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace Continuous.comp_continuousOn' continuous_cos ContinuousOn.fun_mul continuousOn_const Continuous.continuousOn continuous_ofReal mul_comm ofReal_zero MulZeroClass.mul_zero cos_zero EulerSine.tendsto_integral_cos_pow_mul_div Filter.Tendsto.comp Filter.Tendsto.const_mul_atTop' Nat.instIsStrictOrderedRing instArchimedeanNat zero_lt_two Nat.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Filter.tendsto_id one_ne_zero NeZero.charZero_one instCharZero mul_div_assoc

EulerSine

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antideriv_cos_comp_const_mul 📖	mathematical	—	HasDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Complex Complex.addCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField InnerProductSpace.toNormedSpace Real.instRCLike instInnerProductSpaceRealComplex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero Complex.instZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.sin Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Complex.cos	—	IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Nat.instAtLeastTwoHAddOfNat hasDerivAt_mul_const HasDerivAt.comp Complex.hasDerivAt_sin IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul HasDerivAt.div_const HasDerivAt.comp_ofReal HasDerivAt.congr_simp mul_rotate Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq 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 one_mul Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Meta.NormNum.isNat_eq_false Complex.instCharZero Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero
antideriv_sin_comp_const_mul 📖	mathematical	—	HasDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Complex Complex.addCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField InnerProductSpace.toNormedSpace Real.instRCLike instInnerProductSpaceRealComplex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing IsBoundedSMul.continuousSMul Real.pseudoMetricSpace Real.instZero Complex.instZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instNeg Complex.cos Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Complex.sin	—	IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Nat.instAtLeastTwoHAddOfNat hasDerivAt_mul_const HasDerivAt.comp Complex.hasDerivAt_cos IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul HasDerivAt.fun_neg HasDerivAt.div_const HasDerivAt.comp_ofReal HasDerivAt.congr_simp neg_div Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_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.eval_cons_eq_eval_of_eq_of_eq Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' div_one Mathlib.Tactic.FieldSimp.NF.eval_cons one_mul Mathlib.Tactic.FieldSimp.zpow'_one mul_rotate Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst neg_neg Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Meta.NormNum.isNat_eq_false Complex.instCharZero Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero neg_mul
integral_cos_mul_cos_pow 📖	mathematical	—	Complex Complex.instMul Complex.instSub Complex.instOne DivInvMonoid.toDiv Complex.instDivInvMonoid instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring intervalIntegral Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex Complex.cos Complex.ofReal Real.cos Real.instZero Real.instDivInvMonoid Real.pi Real.instNatCast MeasureTheory.MeasureSpace.volume Real.measureSpace	—	Mathlib.Tactic.Contrapose.contrapose₃ Nat.cast_eq_zero Complex.instCharZero zero_lt_two Nat.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instAtLeastTwoHAddOfNat integral_cos_mul_cos_pow_aux 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.subst_sub Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg one_mul 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'_ofNat Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.zpow'_one neg_mul neg_div Mathlib.Meta.NormNum.isNat_eq_false Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero mul_neg Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos 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.mul_pf_right Mathlib.Tactic.Ring.mul_one 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.neg_congr Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.IsInt.to_isNat neg_neg Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Nat.cast_one sub_eq_iff_eq_add mul_add Distrib.leftDistribClass sub_eq_neg_add integral_sin_mul_sin_mul_cos_pow_eq
integral_cos_mul_cos_pow_aux 📖	mathematical	—	intervalIntegral Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex Complex.instMul Complex.cos instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Real.cos Real.instZero DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi Real.instNatCast MeasureTheory.MeasureSpace.volume Real.measureSpace Complex.instDivInvMonoid Complex.sin Real.sin	—	Nat.instAtLeastTwoHAddOfNat IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul HasDerivAt.congr_simp Complex.ofReal_cos Complex.ofReal_sin Complex.ofReal_neg HasDerivAt.ofReal_comp Real.hasDerivAt_cos Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.atom_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_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right 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.pow_congr 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 HasDerivAt.comp hasDerivAt_pow mul_comm Complex.ofReal_zero MulZeroClass.mul_zero Complex.sin_zero zero_div sub_zero Real.cos_pi_div_two zero_pow ne_of_gt lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat MulZeroClass.zero_mul zero_sub intervalIntegral.integral_neg intervalIntegral.integral_const_mul intervalIntegral.integral_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz intervalIntegral.integral_mul_deriv_eq_deriv_mul Complex.instCompleteSpace antideriv_cos_comp_const_mul Continuous.intervalIntegrable Real.locallyFinite_volume Continuous.comp' continuous_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Continuous.prodMk Continuous.fun_mul continuous_const continuous_id' Complex.continuous_ofReal Real.continuous_sin Continuous.pow Real.continuous_cos Complex.continuous_cos
integral_cos_mul_cos_pow_even 📖	mathematical	—	Complex Complex.instMul Complex.instSub Complex.instOne DivInvMonoid.toDiv Complex.instDivInvMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instAdd Complex.instNatCast intervalIntegral Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex Complex.cos instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.cos Real.instZero Real.instDivInvMonoid Real.pi Real.instNatCast MeasureTheory.MeasureSpace.volume Real.measureSpace	—	Nat.instAtLeastTwoHAddOfNat Nat.cast_add Nat.cast_mul mul_one mul_add Distrib.leftDistribClass mul_pow div_div Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat 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_congr Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.Ring.mul_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf 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.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add integral_cos_mul_cos_pow
integral_cos_pow_eq 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Monoid.toNatPow Real.instMonoid Real.cos Real.instZero DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instMul Real.instOne Real.sin	—	Nat.instAtLeastTwoHAddOfNat mul_comm div_eq_iff one_div_ne_zero two_ne_zero' CharZero.NeZero.two RCLike.charZero_rclike div_mul div_one mul_two Continuous.intervalIntegrable Real.locallyFinite_volume Continuous.pow IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Real.continuous_sin intervalIntegral.integral_add_adjacent_intervals Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.instAtLeastTwo 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.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Meta.NormNum.isRat_add Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz Mathlib.Tactic.Ring.add_pf_zero_add intervalIntegral.integral_comp_sub_left intervalIntegral.integral_congr Real.cos_pi_div_two_sub Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_add intervalIntegral.integral_comp_add_right Real.sin_add_pi_div_two
integral_cos_pow_pos 📖	mathematical	—	Real Real.instLT Real.instZero intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Monoid.toNatPow Real.instMonoid Real.cos DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat MeasureTheory.MeasureSpace.volume Real.measureSpace	—	Nat.instAtLeastTwoHAddOfNat mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing one_half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE integral_sin_pow_pos integral_cos_pow_eq
integral_sin_mul_sin_mul_cos_pow_eq 📖	mathematical	—	intervalIntegral Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex Complex.instMul Complex.sin instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.sin Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Real.cos Real.instZero DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi Real.instNatCast MeasureTheory.MeasureSpace.volume Real.measureSpace Complex.instSub Complex.instDivInvMonoid Complex.cos Complex.instOne	—	Nat.instAtLeastTwoHAddOfNat IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul HasDerivAt.comp hasDerivAt_pow Complex.hasDerivAt_cos Complex.ofReal_sin Complex.ofReal_cos mul_neg sub_eq_add_neg pow_succ' Nat.cast_sub LE.le.trans one_le_two Nat.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.cast_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.sub_pf 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.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.pow_congr 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.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add HasDerivAt.comp_ofReal HasDerivAt.fun_mul Complex.hasDerivAt_sin intervalIntegral.integral_congr Mathlib.Tactic.Ring.atom_pf' Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.mul_assoc_rev add_zero mul_one Real.sin_zero Real.cos_pi_div_two Complex.ofReal_zero zero_pow MulZeroClass.zero_mul MulZeroClass.mul_zero sub_zero zero_sub intervalIntegral.integral_neg intervalIntegral.integral_const_mul intervalIntegral.integral_sub Continuous.intervalIntegrable Real.locallyFinite_volume Continuous.comp' Continuous.fun_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing continuous_const continuous_id' continuous_mul Continuous.prodMk Complex.continuous_cos Complex.continuous_ofReal Continuous.pow Real.continuous_cos Complex.sin_sq mul_div_right_comm sub_div mul_div neg_div pow_add Mathlib.Tactic.Ring.neg_mul Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add intervalIntegral.integral_mul_deriv_eq_deriv_mul Complex.instCompleteSpace antideriv_sin_comp_const_mul Continuous.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup Real.continuous_sin Complex.continuous_sin
sin_pi_mul_eq 📖	mathematical	—	Complex.sin Complex Complex.instMul Complex.ofReal Real.pi DivInvMonoid.toDiv Complex.instDivInvMonoid Finset.prod CommRing.toCommMonoid Complex.commRing Finset.range Complex.instSub Complex.instOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instAdd Complex.instNatCast intervalIntegral Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex Complex.cos instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat Real.cos Real.instZero Real.instDivInvMonoid Real.instNatCast MeasureTheory.MeasureSpace.volume Real.measureSpace Real.normedAddCommGroup RCLike.toInnerProductSpaceReal Real.instMonoid	—	Nat.instAtLeastTwoHAddOfNat eq_or_ne MulZeroClass.mul_zero Complex.sin_zero Finset.prod_congr zero_pow Nat.instCharZero zero_div sub_zero Finset.prod_const_one mul_one MulZeroClass.zero_mul Complex.cos_zero Complex.ofReal_cos one_mul pow_zero Finset.prod_range_zero integral_one integral_cos_mul_complex mul_ne_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass two_ne_zero CharZero.NeZero.two Complex.instCharZero Complex.ofReal_zero Complex.ofReal_div 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.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right 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.div_congr 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.mul_pf_left Mathlib.Tactic.Ring.one_mul 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 Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons 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.div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Meta.NormNum.isNat_eq_false Nat.cast_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Finset.prod_range_succ mul_add Distrib.leftDistribClass integral_cos_pow_eq integral_sin_pow Real.sin_zero Real.sin_pi pow_succ' zero_add mul_assoc mul_comm Nat.cast_mul Nat.cast_ofNat Nat.cast_succ integral_cos_mul_cos_pow_even Complex.ofReal_mul Complex.ofReal_ne_zero LT.lt.ne' integral_cos_pow_pos Nat.cast_add_one_ne_zero Complex.ofReal_add Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.cons_ne_zero
tendsto_integral_cos_pow_mul_div 📖	mathematical	ContinuousOn Real Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Set.Icc Real.instPreorder Real.instZero DivInvMonoid.toDiv Real.instDivInvMonoid Real.pi instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	Filter.Tendsto Complex.instDivInvMonoid intervalIntegral Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex Complex.instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.ofReal Real.cos MeasureTheory.MeasureSpace.volume Real.measureSpace Real.normedAddCommGroup RCLike.toInnerProductSpaceReal Real.instMonoid Filter.atTop Nat.instPreorder nhds	—	Nat.instAtLeastTwoHAddOfNat div_eq_inv_mul intervalIntegral.integral_of_le LT.lt.le Real.pi_div_two_pos Real.noAtoms_volume Real.cos_lt_cos_of_nonneg_of_le_pi_div_two le_refl lt_of_le_of_ne Real.cos_nonneg_of_mem_Icc Set.Icc_subset_Icc_left neg_nonpos_of_nonneg Real.instIsOrderedAddMonoid Real.cos_zero zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike interior_Icc instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial instNoMaxOrderOfNontrivial closure_Ioo LT.lt.ne Set.left_mem_Icc tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn Real.borelSpace Complex.instCompleteSpace EMetricSpace.metrizableSpace Real.locallyFinite_volume MeasureTheory.Measure.IsAddHaarMeasure.toIsOpenPosMeasure instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real CompactIccSpace.isCompact_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace Real.continuousOn_cos

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendsto_euler_sin_prod 📖	mathematical	—	Filter.Tendsto Real instMul pi Finset.prod instCommMonoid Finset.range instSub instOne DivInvMonoid.toDiv instDivInvMonoid Monoid.toNatPow instMonoid instAdd instNatCast Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace sin	—	Complex.ofReal_mul Complex.re_ofReal_mul Complex.ofReal_prod Finset.prod_congr Nat.cast_one Nat.cast_pow Nat.cast_add Complex.ofReal_pow Complex.ofReal_add Complex.ofReal_re Complex.ofReal_sin Filter.Tendsto.comp Continuous.tendsto Complex.continuous_re Complex.tendsto_euler_sin_prod

---

← Back to Index