MellinEqDirichlet

📁 Source: Mathlib/NumberTheory/LSeries/MellinEqDirichlet.lean

Statistics

Metric	Count
Definitions	0
Theorems hasSum_mellin, hasSum_mellin_pi_mul, hasSum_mellin_pi_mul_sq, hasSum_mellin_pi_mul_sq', hasSum_mellin_pi_mul₀	5
Total	5

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasSum_mellin 📖	mathematical	Complex Complex.instZero Real Real.instLT Real.instZero Complex.re HasSum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Complex.instMul Complex.ofReal Real.exp Real.instMul Real.instNeg SummationFilter.unconditional Summable Real.instAddCommMonoid Real.pseudoMetricSpace DivInvMonoid.toDiv Real.instDivInvMonoid Norm.norm Complex.instNorm Real.instPow	Complex.instDivInvMonoid Complex.Gamma Complex.instPow mellin InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace	—	MeasureTheory.setIntegral_congr_fun measurableSet_Ioi BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid HasSum.tsum_eq Complex.instT2Space SummationFilter.instNeBotUnconditional IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing mul_comm mul_assoc mul_div_assoc MeasureTheory.integral_const_mul MulZeroClass.zero_mul Complex.integral_cpow_mul_exp_neg_mul_Ioi neg_mul one_div Complex.inv_cpow LT.lt.ne Real.pi_pos Complex.arg_ofReal_of_nonneg LT.lt.le div_eq_inv_mul MeasureTheory.hasSum_integral_of_summable_integral_norm Complex.ofReal_exp Complex.ofReal_neg Complex.ofReal_mul MulZeroClass.mul_zero Complex.GammaIntegral_convergent MeasureTheory.Integrable.const_mul MeasureTheory.IntegrableOn.congr_fun MeasureTheory.integrableOn_Ioi_comp_mul_left_iff Complex.mul_cpow_ofReal_nonneg inv_mul_cancel₀ Complex.cpow_eq_zero_iff not_and_or Complex.ofReal_ne_zero LT.lt.ne' one_mul Summable.of_norm Real.instCompleteSpace norm_mul NormedDivisionRing.toNormMulClass norm_norm norm_zero Complex.norm_mul Real.integral_rpow_mul_exp_neg_mul_Ioi Real.norm_of_nonneg MeasureTheory.integral_nonneg IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing instClosedIciTopology norm_nonneg Real.inv_rpow Complex.norm_real Real.norm_eq_abs Real.abs_exp Complex.norm_cpow_eq_rpow_re_of_pos Complex.sub_re Complex.one_re Summable.mul_left instIsTopologicalRingReal
hasSum_mellin_pi_mul 📖	mathematical	Complex Complex.instZero Real Real.instLT Real.instZero Complex.re HasSum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Complex.instMul Complex.ofReal Real.exp Real.instMul Real.instNeg Real.pi SummationFilter.unconditional Summable Real.instAddCommMonoid Real.pseudoMetricSpace DivInvMonoid.toDiv Real.instDivInvMonoid Norm.norm Complex.instNorm Real.instPow	Complex.instDivInvMonoid Complex.instPow Complex.instNeg Complex.Gamma mellin InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace	—	IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Complex.ofReal_mul zero_div MulZeroClass.mul_zero Complex.mul_cpow_ofReal_nonneg LT.lt.le Real.pi_pos div_div Complex.cpow_neg div_eq_inv_mul mul_div_assoc Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf 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.one_mul 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.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one Mathlib.Tactic.RingNF.mul_assoc_rev add_zero hasSum_mellin neg_mul Complex.ofReal_exp Complex.ofReal_neg norm_zero Real.mul_rpow Real.rpow_neg Summable.mul_left IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal
hasSum_mellin_pi_mul_sq 📖	mathematical	Real Real.instLT Real.instZero Complex.re HasSum Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Real.decidableEq Complex.instZero Complex.instMul Complex.ofReal Real.exp Real.instMul Real.instNeg Real.pi Monoid.toNatPow Real.instMonoid SummationFilter.unconditional Summable Real.instAddCommMonoid Real.pseudoMetricSpace DivInvMonoid.toDiv Real.instDivInvMonoid Norm.norm Complex.instNorm Real.instPow abs Real.lattice Real.instAddGroup	Complex.instDivInvMonoid Complex.Gammaℝ Complex.instPow mellin InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Complex.div_ofNat_re div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo neg_div Complex.Gammaℝ_def sq_abs Complex.ofReal_pow Complex.cpow_nat_mul' Complex.arg_ofReal_of_nonneg abs_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add 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 Mathlib.Meta.NormNum.isNat_natCast Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_zero_add 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.sub_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt Real.pi_pos le_of_not_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Ring.atom_pf' 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 Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pf_right 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.RingNF.nat_rawCast_1 pow_one mul_one add_zero hasSum_mellin_pi_mul₀ sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono sq_eq_zero_iff isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Real.rpow_natCast_mul Nat.cast_ofNat mul_div_cancel₀ LT.lt.ne' two_pos Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike
hasSum_mellin_pi_mul_sq' 📖	mathematical	Real Real.instLT Real.instZero Complex.re HasSum Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Complex.instMul Complex.ofReal Real.exp Real.instMul Real.instNeg Real.pi Monoid.toNatPow Real.instMonoid SummationFilter.unconditional Summable Real.instAddCommMonoid Real.pseudoMetricSpace DivInvMonoid.toDiv Real.instDivInvMonoid Norm.norm Complex.instNorm Real.instPow abs Real.lattice Real.instAddGroup	Complex.instDivInvMonoid Complex.Gammaℝ Complex.instAdd Complex.instOne SignType.cast Complex.instZero Complex.instNeg DFunLike.coe OrderHom SignType Real.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Real.decidableLT Complex.instPow mellin InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	lt_irrefl Complex.zero_re Complex.add_re Complex.one_re add_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one MulZeroClass.mul_zero zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat MulZeroClass.zero_mul Real.exp_zero mul_one neg_mul Complex.ofReal_exp Complex.ofReal_neg Complex.ofReal_mul Complex.ofReal_pow eq_or_ne abs_zero Complex.ofReal_zero Complex.zero_cpow div_zero Complex.cpow_add Complex.ofReal_ne_zero abs_ne_zero covariant_swap_add_of_covariant_add Complex.cpow_one sign_mul_abs Real.instIsStrictOrderedRing Complex.ofRealHom_eq_coe SignType.map_cast DistribMulActionSemiHomClass.toAddMonoidHomClass RCLike.charZero_rclike Complex.instCharZero SemilinearMapClass.distribMulActionSemiHomClass RingHomClass.toLinearMapClassNNRat RingHom.instRingHomClass MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul 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₃ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one 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.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.atom_pf 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.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul hasSum_mellin_pi_mul_sq Real.zero_rpow LT.lt.ne' Real.rpow_add abs_pos Real.rpow_one norm_mul NormedDivisionRing.toNormMulClass Complex.norm_real Real.norm_eq_abs div_div div_right_comm mul_div_cancel_right₀ EuclideanDomain.toMulDivCancelClass
hasSum_mellin_pi_mul₀ 📖	mathematical	Real Real.instLE Real.instZero Real.instLT Complex.re HasSum Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Real.decidableEq Complex.instZero Complex.instMul Complex.ofReal Real.exp Real.instMul Real.instNeg Real.pi SummationFilter.unconditional Summable Real.instAddCommMonoid Real.pseudoMetricSpace DivInvMonoid.toDiv Real.instDivInvMonoid Norm.norm Complex.instNorm Real.instPow	Complex.instDivInvMonoid Complex.instPow Complex.instNeg Complex.Gamma mellin InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace	—	lt_irrefl Complex.zero_re lt_of_le_of_ne neg_mul Complex.ofReal_exp Complex.ofReal_neg Complex.ofReal_mul ite_mul MulZeroClass.zero_mul eq_or_ne Complex.zero_cpow div_zero MulZeroClass.mul_zero hasSum_mellin_pi_mul Summable.of_norm_bounded Real.instCompleteSpace norm_zero zero_div div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing norm_nonneg Real.rpow_nonneg ge_of_eq Real.norm_of_nonneg Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos Real.rpow_pos_of_pos lt_of_le_of_ne' le_refl

---

← Back to Index