MellinInversion

📁 Source: Mathlib/Analysis/MellinInversion.lean

Statistics

Metric	Count
Definitions	0
Theorems mellinInv_eq_fourierIntegralInv, mellinInv_eq_fourierInv, mellinInv_mellin_eq, mellin_eq_fourier, mellin_eq_fourierIntegral, mellin_inversion	6
Total	6

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mellinInv_eq_fourierIntegralInv 📖	mathematical	Real Real.instLT Real.instZero	mellinInv Complex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Complex.instNormedField Complex.instPow Complex.ofReal Complex.instNeg FourierTransformInv.fourierInv Real.instFourierTransformInv Real.normedAddCommGroup RCLike.toInnerProductSpaceReal Real.instRCLike Real.measurableSpace Real.borelSpace FiniteDimensional.rclike_to_real Complex.instAdd Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi Complex.I Real.instNeg Real.log	—	mellinInv_eq_fourierInv
mellinInv_eq_fourierInv 📖	mathematical	Real Real.instLT Real.instZero	mellinInv Complex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Complex.instNormedField Complex.instPow Complex.ofReal Complex.instNeg FourierTransformInv.fourierInv Real.instFourierTransformInv Real.normedAddCommGroup RCLike.toInnerProductSpaceReal Real.instRCLike Real.measurableSpace Real.borelSpace FiniteDimensional.rclike_to_real Complex.instAdd Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi Complex.I Real.instNeg Real.log	—	Nat.instAtLeastTwoHAddOfNat Real.borelSpace FiniteDimensional.rclike_to_real mellinInv.eq_1 one_div abs_of_pos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mul_inv_rev IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Real.instIsOrderedRing Real.instNontrivial Complex.ofReal_ne_zero ne_of_gt neg_add Complex.cpow_add SemigroupAction.mul_smul MeasureTheory.integral_smul NormedSpace.toNormSMulClass SMulCommClass.complexToReal smulCommClass_self SMulCommClass.smul_comm MeasureTheory.Measure.integral_comp_mul_left Complex.cpow_def_of_ne_zero Complex.ofReal_log LT.lt.le Complex.ofReal_mul Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo 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.mul_pf_left 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.one_mul Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg Mathlib.Tactic.RingNF.mul_assoc_rev add_zero Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_gt mul_one mul_neg neg_mul Real.fourierInv_eq' conj_trivial instTrivialStarReal mul_comm Complex.ofReal_neg
mellinInv_mellin_eq 📖	mathematical	Real Real.instLT Real.instZero MellinConvergent Complex.ofReal Complex.VerticalIntegrable mellin MeasureTheory.MeasureSpace.volume Real.measureSpace ContinuousAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	mellinInv	—	neg_mul abs_neg Real.abs_exp Complex.ofReal_exp Complex.ofReal_neg MeasureTheory.integrableOn_image_iff_integrableOn_abs_deriv_smul MeasurableSet.univ MellinConvergent.eq_1 Real.borelSpace FiniteDimensional.rclike_to_real Nat.instAtLeastTwoHAddOfNat NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass RCLike.charZero_rclike Complex.ofReal_mul mellin_eq_fourier MulZeroClass.mul_zero sub_zero MulZeroClass.zero_mul add_zero mul_one sub_self zero_add mul_div_cancel_right₀ EuclideanDomain.toMulDivCancelClass MeasureTheory.Integrable.comp_mul_right' neg_mul_eq_neg_mul ContinuousAt.smul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ContinuousAt.rexp ContinuousAt.fun_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuousAt_const continuousAt_id' ContinuousAt.comp neg_neg Real.exp_log ContinuousAt.neg IsTopologicalRing.toContinuousNeg one_div mul_inv_rev neg_add_rev mellinInv_eq_fourierInv MeasureTheory.Integrable.fourierInv_fourier_eq mul_div_cancel_left₀ mul_neg mul_comm Real.rpow_def_of_pos Complex.ofReal_cpow LT.lt.le smul_assoc IsScalarTower.left smul_eq_mul Real.rpow_neg inv_mul_cancel₀ ne_of_gt Real.rpow_pos_of_pos one_smul
mellin_eq_fourier 📖	mathematical	—	mellin FourierTransform.fourier Real.instFourierTransform Real Real.normedAddCommGroup RCLike.toInnerProductSpaceReal Real.instRCLike Real.measurableSpace Real.borelSpace FiniteDimensional.rclike_to_real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField NormedSpace.complexToReal Real.exp Real.instMul Real.instNeg Complex.re DivInvMonoid.toDiv Real.instDivInvMonoid Complex.im instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi	—	Nat.instAtLeastTwoHAddOfNat Real.borelSpace FiniteDimensional.rclike_to_real mellin.eq_1 MeasureTheory.integral_image_eq_integral_abs_deriv_smul MeasurableSet.univ MeasureTheory.Measure.restrict_univ abs_neg Real.abs_exp Complex.ofReal_exp Complex.ofReal_neg neg_mul Complex.re_add_im neg_add add_mul Distrib.rightDistribClass Complex.exp_add mul_comm smul_eq_mul smul_assoc IsScalarTower.left Complex.ofReal_mul Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_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.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.mul_one 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 Complex.ofReal_div 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.mul_eq_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 div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval 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.eval_mul_eval_cons_zero 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 one_ne_zero NeZero.one GroupWithZero.toNontrivial Real.fourier_eq' conj_trivial instTrivialStarReal
mellin_eq_fourierIntegral 📖	mathematical	—	mellin FourierTransform.fourier Real.instFourierTransform Real Real.normedAddCommGroup RCLike.toInnerProductSpaceReal Real.instRCLike Real.measurableSpace Real.borelSpace FiniteDimensional.rclike_to_real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField NormedSpace.complexToReal Real.exp Real.instMul Real.instNeg Complex.re DivInvMonoid.toDiv Real.instDivInvMonoid Complex.im instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi	—	mellin_eq_fourier
mellin_inversion 📖	mathematical	Real Real.instLT Real.instZero MellinConvergent Complex.ofReal Complex.VerticalIntegrable mellin MeasureTheory.MeasureSpace.volume Real.measureSpace ContinuousAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	mellinInv	—	mellinInv_mellin_eq

---

← Back to Index