MellinTransform

📁 Source: Mathlib/Analysis/MellinTransform.lean

Statistics

Metric	Count
Definitions VerticalIntegrable, HasMellin, MellinConvergent, mellin, mellinInv	5
Theorems comp_mul_left, comp_rpow, const_smul, cpow_smul, div_const, hasMellin_add, hasMellin_const_smul, hasMellin_cpow_Ioc, hasMellin_one_Ioc, hasMellin_sub, isBigO_rpow_top_log_smul, isBigO_rpow_zero_log_smul, mellinConvergent_of_isBigO_rpow, mellinConvergent_of_isBigO_rpow_exp, mellin_comp_inv, mellin_comp_mul_left, mellin_comp_mul_right, mellin_comp_rpow, mellin_const_smul, mellin_convergent_iff_norm, mellin_convergent_of_isBigO_scalar, mellin_convergent_top_of_isBigO, mellin_convergent_zero_of_isBigO, mellin_cpow_smul, mellin_differentiableAt_of_isBigO_rpow, mellin_differentiableAt_of_isBigO_rpow_exp, mellin_div_const, mellin_hasDerivAt_of_isBigO_rpow	28
Total	33

Complex

Definitions

Name	Category	Theorems
VerticalIntegrable 📖	MathDef	—

MellinConvergent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_mul_left 📖	mathematical	Real Real.instLT Real.instZero	MellinConvergent Real.instMul	—	MeasureTheory.integrableOn_Ioi_comp_mul_left_iff Complex.ofReal_mul Complex.mul_cpow_ofReal_nonneg LT.lt.le le_of_lt SemigroupAction.mul_smul Complex.cpow_eq_zero_iff not_and_or Complex.ofReal_eq_zero LT.lt.ne' eq_1 MulZeroClass.mul_zero MeasureTheory.integrableOn_congr_fun measurableSet_Ioi BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid MeasureTheory.IntegrableOn.eq_1 MeasureTheory.integrable_smul_iff NormedSpace.toIsBoundedSMul
comp_rpow 📖	mathematical	—	MellinConvergent Real Real.instPow Complex DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.ofReal	—	eq_1 MeasureTheory.integrableOn_congr_fun Complex.coe_smul SemigroupAction.mul_smul Complex.cpow_mul_ofReal_nonneg le_of_lt Complex.ofReal_cpow Complex.cpow_add Complex.ofReal_ne_zero ne_of_gt Complex.ofReal_sub Complex.ofReal_one mul_sub mul_div_cancel₀ mul_one add_comm add_sub_assoc sub_add_cancel measurableSet_Ioi BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid MeasureTheory.integrableOn_Ioi_comp_rpow_iff'
const_smul 📖	mathematical	MellinConvergent	SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	SMulCommClass.smul_comm MeasureTheory.Integrable.smul
cpow_smul 📖	mathematical	—	MellinConvergent 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.instAdd	—	MeasureTheory.integrableOn_congr_fun Complex.cpow_add Complex.ofReal_ne_zero ne_of_gt SemigroupAction.mul_smul measurableSet_Ioi BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid
div_const 📖	mathematical	MellinConvergent Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace	DivInvMonoid.toDiv Complex.instDivInvMonoid	—	MeasureTheory.Integrable.div_const

(root)

Definitions

Name	Category	Theorems
HasMellin 📖	MathDef	7 math math: hasMellin_sub, hasMellin_add, hasMellin_one_Ioc, StrongFEPair.hasMellin, WeakFEPair.hasMellin, hasMellin_cpow_Ioc, hasMellin_const_smul
MellinConvergent 📖	MathDef	6 math math: mellinConvergent_of_isBigO_rpow_exp, mellin_hasDerivAt_of_isBigO_rpow, MellinConvergent.comp_mul_left, MellinConvergent.comp_rpow, mellinConvergent_of_isBigO_rpow, MellinConvergent.cpow_smul
mellin 📖	CompOp	24 math math: hasSum_mellin_pi_mul_sq', mellin_eq_fourier, Complex.GammaIntegral_eq_mellin, mellin_div_const, hasMellin_sub, hasMellin_add, mellin_hasDerivAt_of_isBigO_rpow, hasSum_mellin, StrongFEPair.Λ_eq, hasSum_mellin_pi_mul, mellin_eq_fourierIntegral, mellin_comp_inv, mellin_comp_rpow, hasSum_mellin_pi_mul₀, mellin_const_smul, mellin_differentiableAt_of_isBigO_rpow_exp, StrongFEPair.symm_Λ_eq, mellin_differentiableAt_of_isBigO_rpow, WeakFEPair.f_modif_aux2, mellin_cpow_smul, hasMellin_const_smul, hasSum_mellin_pi_mul_sq, mellin_comp_mul_left, mellin_comp_mul_right
mellinInv 📖	CompOp	4 math math: mellinInv_eq_fourierIntegralInv, mellin_inversion, mellinInv_eq_fourierInv, mellinInv_mellin_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasMellin_add 📖	mathematical	MellinConvergent	HasMellin AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid mellin	—	smul_add MeasureTheory.Integrable.add IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.integral_add
hasMellin_const_smul 📖	mathematical	MellinConvergent	HasMellin 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 Ring.toSemiring NormedRing.toRing Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid mellin	—	MellinConvergent.const_smul SMulCommClass.smul_comm MeasureTheory.Integrable.integral_smul SMulCommClass.complexToReal
hasMellin_cpow_Ioc 📖	mathematical	Real Real.instLT Real.instZero Real.instAdd Complex.re	HasMellin Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Set.indicator Complex.instZero Set.Ioc Real.instPreorder Real.instOne Complex.instPow Complex.ofReal DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Complex.instAdd	—	hasMellin_one_Ioc Complex.add_re mul_one
hasMellin_one_Ioc 📖	mathematical	Real Real.instLT Real.instZero Complex.re	HasMellin Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace Set.indicator Complex.instZero Set.Ioc Real.instPreorder Real.instOne Complex.instOne DivInvMonoid.toDiv Complex.instDivInvMonoid	—	sub_eq_add_neg lt_add_of_pos_left IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Tactic.Contrapose.contrapose₃ Complex.zero_re le_refl measurableSet_Ioc BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal MeasureTheory.integrable_indicator_iff MeasureTheory.integral_indicator mul_one MeasureTheory.Measure.restrict_restrict_of_subset Set.Ioc_subset_Ioi_self MeasureTheory.IntegrableOn.eq_1 intervalIntegrable_iff_integrableOn_Ioc_of_le PseudoEMetricSpace.pseudoMetrizableSpace zero_le_one Real.instZeroLEOneClass intervalIntegral.intervalIntegrable_cpow' intervalIntegral.integral_of_le integral_cpow sub_add_cancel Complex.ofReal_zero Complex.ofReal_one Complex.one_cpow Complex.zero_cpow sub_zero
hasMellin_sub 📖	mathematical	MellinConvergent	HasMellin SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup mellin	—	smul_sub MeasureTheory.Integrable.sub MeasureTheory.integral_sub
isBigO_rpow_top_log_smul 📖	mathematical	Real Real.instLT Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm Filter.atTop Real.instPreorder Real.instPow Real.instNeg	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 Real.log	—	Asymptotics.IsBigO.congr' Asymptotics.IsBigO.smul NormedSpace.toIsBoundedSMul NormedSpace.toNormSMulClass Asymptotics.IsLittleO.isBigO isLittleO_log_rpow_atTop sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Filter.Eventually.of_forall Filter.Eventually.mp Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial smul_eq_mul Real.rpow_add sub_eq_add_neg add_sub_cancel_left
isBigO_rpow_zero_log_smul 📖	mathematical	Real Real.instLT Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero Set.Ioi Real.instPreorder Real.instPow Real.instNeg	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid 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 Real.log	—	Asymptotics.IsLittleO.congr' Asymptotics.IsLittleO.comp_tendsto Asymptotics.IsLittleO.neg_left isLittleO_log_rpow_atTop sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid tendsto_inv_nhdsGT_zero Real.instIsStrictOrderedRing instOrderTopologyReal Filter.Eventually.of_forall Real.log_inv neg_neg Filter.Eventually.mono eventually_mem_nhdsWithin Real.inv_rpow le_of_lt Real.rpow_neg neg_sub Asymptotics.IsBigO.congr' Asymptotics.IsBigO.smul NormedSpace.toIsBoundedSMul NormedSpace.toNormSMulClass Asymptotics.IsLittleO.isBigO eventually_nhdsWithin_iff Real.rpow_add Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isInt_neg add_zero Mathlib.Tactic.Abel.zero_termg
mellinConvergent_of_isBigO_rpow 📖	mathematical	MeasureTheory.LocallyIntegrableOn Real Real.measurableSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Set.Ioi Real.instPreorder Real.instZero MeasureTheory.MeasureSpace.volume Real.measureSpace Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm Filter.atTop Real.instPow Real.instNeg Real.instLT Complex.re nhdsWithin	MellinConvergent	—	MellinConvergent.eq_1 mellin_convergent_iff_norm Set.Subset.rfl measurableSet_Ioi BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid MeasureTheory.LocallyIntegrableOn.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal mellin_convergent_of_isBigO_scalar MeasureTheory.LocallyIntegrableOn.norm Asymptotics.IsBigO.norm_left
mellinConvergent_of_isBigO_rpow_exp 📖	mathematical	Real Real.instLT Real.instZero MeasureTheory.LocallyIntegrableOn Real.measurableSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Set.Ioi Real.instPreorder MeasureTheory.MeasureSpace.volume Real.measureSpace Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm Filter.atTop Real.exp Real.instMul Real.instNeg nhdsWithin Real.instPow Complex.re	MellinConvergent	—	mellinConvergent_of_isBigO_rpow Asymptotics.IsBigO.trans Asymptotics.IsLittleO.isBigO isLittleO_exp_neg_mul_rpow_atTop lt_add_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
mellin_comp_inv 📖	mathematical	—	mellin Real Real.instInv Complex Complex.instNeg	—	mellin_comp_rpow abs_neg abs_one Real.instIsOrderedRing inv_one one_smul Complex.ofReal_neg div_neg div_one
mellin_comp_mul_left 📖	mathematical	Real Real.instLT Real.instZero	mellin Real.instMul 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	—	Complex.ofReal_mul Complex.mul_cpow_ofReal_nonneg LT.lt.le le_of_lt SemigroupAction.mul_smul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one 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.neg_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Complex.cpow_neg inv_mul_cancel_left₀ Complex.cpow_eq_zero_iff Complex.ofReal_eq_zero not_and_or LT.lt.ne' MeasureTheory.setIntegral_congr_fun measurableSet_Ioi BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid MeasureTheory.integral_smul NormedSpace.toNormSMulClass SMulCommClass.complexToReal smulCommClass_self MeasureTheory.integral_comp_mul_left_Ioi MulZeroClass.mul_zero Complex.coe_smul sub_eq_add_neg Complex.cpow_add Complex.ofReal_ne_zero Complex.cpow_one Complex.ofReal_inv mul_assoc mul_comm inv_mul_cancel_right₀
mellin_comp_mul_right 📖	mathematical	Real Real.instLT Real.instZero	mellin Real.instMul 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	—	mul_comm mellin_comp_mul_left
mellin_comp_rpow 📖	mathematical	—	mellin Real Real.instPow 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.instInv abs Real.lattice Real.instAddGroup Complex DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.ofReal	—	eq_or_ne Real.rpow_zero integral_smul_const setIntegral_Ioi_zero_cpow zero_smul abs_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid inv_zero div_zero zero_sub MeasureTheory.integral_def smul_zero MeasureTheory.integral_comp_rpow_Ioi MeasureTheory.integral_smul NormedSpace.toNormSMulClass smulCommClass_self MeasureTheory.setIntegral_congr_fun measurableSet_Ioi BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal SemigroupAction.mul_smul mul_assoc inv_mul_cancel₀ abs_eq_zero covariant_swap_add_of_covariant_add one_mul smul_assoc IsScalarTower.complexToReal IsScalarTower.left Complex.real_smul Complex.ofReal_cpow le_of_lt Complex.cpow_mul_ofReal_nonneg Complex.cpow_add Complex.ofReal_ne_zero ne_of_gt Complex.ofReal_sub Complex.ofReal_one mul_sub mul_div_cancel₀ add_comm add_sub_assoc mul_one sub_add_cancel
mellin_const_smul 📖	mathematical	—	mellin 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 DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule	—	SMulCommClass.smul_comm MeasureTheory.integral_smul NormedSpace.toNormSMulClass SMulCommClass.complexToReal
mellin_convergent_iff_norm 📖	mathematical	Set Real Set.instHasSubset Set.Ioi Real.instPreorder Real.instZero MeasurableSet Real.measurableSpace MeasureTheory.AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume	MeasureTheory.IntegrableOn SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Complex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid 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.instSub Complex.instOne Real.pseudoMetricSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.instMul Real.instPow Real.instSub Complex.re Real.instOne Norm.norm NormedAddCommGroup.toNorm	—	MeasureTheory.AEStronglyMeasurable.smul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul ContinuousOn.aestronglyMeasurable secondCountableTopologyEither_of_right secondCountable_of_proper Complex.instProperSpace BorelSpace.opensMeasurable Real.borelSpace PseudoEMetricSpace.pseudoMetrizableSpace continuousOn_of_forall_continuousAt Complex.continuousAt_ofReal_cpow_const ne_of_gt MeasureTheory.AEStronglyMeasurable.mono_set MeasureTheory.IntegrableOn.eq_1 MeasureTheory.integrable_norm_iff MeasureTheory.integrableOn_congr_fun norm_smul NormedSpace.toNormSMulClass Complex.norm_cpow_eq_rpow_re_of_pos
mellin_convergent_of_isBigO_scalar 📖	mathematical	MeasureTheory.LocallyIntegrableOn Real Real.measurableSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Set.Ioi Real.instPreorder Real.instZero MeasureTheory.MeasureSpace.volume Real.measureSpace Asymptotics.IsBigO Real.norm Filter.atTop Real.instPow Real.instNeg Real.instLT nhdsWithin	MeasureTheory.IntegrableOn MeasureTheory.MeasureSpace.toMeasurableSpace Real.instMul Real.instSub Real.instOne	—	mellin_convergent_top_of_isBigO MeasureTheory.LocallyIntegrableOn.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal mellin_convergent_zero_of_isBigO Set.union_assoc Set.Ioc_union_Ioi le_max_right LE.le.trans min_le_left min_eq_left LT.lt.le lt_min MeasureTheory.integrableOn_union integrableOn_Icc_iff_integrableOn_Ioc instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable Real.borelSpace TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Real.noAtoms_volume enorm_ne_top MeasureTheory.LocallyIntegrableOn.integrableOn_compact_subset MeasureTheory.LocallyIntegrableOn.continuousOn_mul locallyCompact_of_proper instProperSpaceReal secondCountableTopologyEither_of_right continuousOn_of_forall_continuousAt Real.continuousAt_rpow_const ne_of_gt IsOpen.isLocallyClosed isOpen_Ioi instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid LT.lt.trans_le CompactIccSpace.isCompact_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal
mellin_convergent_top_of_isBigO 📖	mathematical	MeasureTheory.AEStronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.measurableSpace MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Ioi Real.instPreorder Real.instZero Asymptotics.IsBigO Real.norm Filter.atTop Real.instPow Real.instNeg Real.instLT	MeasureTheory.IntegrableOn SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.instMul Real.instSub Real.instOne	—	Asymptotics.IsBigO.isBigOWith instIsDirectedOrder Real.instIsOrderedRing Real.instArchimedean Asymptotics.IsBigOWith_def LT.lt.trans_le zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike le_max_right MeasureTheory.AEStronglyMeasurable.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousOn.aestronglyMeasurable secondCountableTopologyEither_of_right instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace PseudoEMetricSpace.pseudoMetrizableSpace continuousOn_of_forall_continuousAt Real.continuousAt_rpow_const LT.lt.ne' LT.lt.trans measurableSet_Ioi instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid MeasureTheory.AEStronglyMeasurable.mono_set Set.Ioi_subset_Ioi LT.lt.le MeasureTheory.Measure.instOuterMeasureClass Filter.Eventually.mono MeasureTheory.ae_restrict_mem norm_mul NormedDivisionRing.toNormMulClass Real.rpow_add Real.norm_of_nonneg Real.rpow_nonneg mul_assoc mul_comm mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono LE.le.trans_lt le_max_left le_of_lt Real.rpow_pos_of_pos MeasureTheory.HasFiniteIntegral.mono' MeasureTheory.HasFiniteIntegral.mul_const MeasureTheory.Integrable.hasFiniteIntegral integrableOn_Ioi_rpow_of_lt 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.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.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat 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 Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Tactic.Linarith.sub_nonpos_of_le
mellin_convergent_zero_of_isBigO 📖	mathematical	MeasureTheory.AEStronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.measurableSpace MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Ioi Real.instPreorder Real.instZero Asymptotics.IsBigO Real.norm nhdsWithin Real.instPow Real.instNeg Real.instLT	MeasureTheory.IntegrableOn SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.instMul Real.instSub Real.instOne Set.Ioc	—	Asymptotics.IsBigO.exists_pos Asymptotics.IsBigOWith_def integrableOn_Ioc_iff_integrableOn_Ioo instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable Real.borelSpace instSecondCountableTopologyReal TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace PseudoEMetricSpace.pseudoMetrizableSpace Real.noAtoms_volume enorm_ne_top MeasureTheory.AEStronglyMeasurable.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousOn.aestronglyMeasurable secondCountableTopologyEither_of_right continuousOn_of_forall_continuousAt Real.continuousAt_rpow_const LT.lt.ne' measurableSet_Ioo HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid MeasureTheory.AEStronglyMeasurable.mono_set Set.Ioo_subset_Ioi_self MeasureTheory.HasFiniteIntegral.mono' MeasureTheory.HasFiniteIntegral.const_mul MeasureTheory.Integrable.hasFiniteIntegral MeasureTheory.IntegrableOn.eq_1 intervalIntegrable_iff_integrableOn_Ioc_of_le LT.lt.le intervalIntegral.intervalIntegrable_rpow' 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.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.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_congr Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat 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 Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_restrict_iff' Filter.Eventually.of_forall mul_comm norm_mul NormedDivisionRing.toNormMulClass mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono dist_eq_norm sub_zero Real.norm_of_nonneg le_of_lt norm_nonneg Real.rpow_nonneg mul_assoc Real.rpow_add Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg add_zero
mellin_cpow_smul 📖	mathematical	—	mellin 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.instAdd	—	MeasureTheory.setIntegral_congr_fun measurableSet_Ioi BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Complex.cpow_add Complex.ofReal_ne_zero ne_of_gt SemigroupAction.mul_smul
mellin_differentiableAt_of_isBigO_rpow 📖	mathematical	MeasureTheory.LocallyIntegrableOn Real Real.measurableSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Set.Ioi Real.instPreorder Real.instZero MeasureTheory.MeasureSpace.volume Real.measureSpace Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm Filter.atTop Real.instPow Real.instNeg Real.instLT Complex.re nhdsWithin	DifferentiableAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule mellin	—	HasDerivAt.differentiableAt IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul mellin_hasDerivAt_of_isBigO_rpow
mellin_differentiableAt_of_isBigO_rpow_exp 📖	mathematical	Real Real.instLT Real.instZero MeasureTheory.LocallyIntegrableOn Real.measurableSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Set.Ioi Real.instPreorder MeasureTheory.MeasureSpace.volume Real.measureSpace Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm Filter.atTop Real.exp Real.instMul Real.instNeg nhdsWithin Real.instPow Complex.re	DifferentiableAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule mellin	—	mellin_differentiableAt_of_isBigO_rpow Asymptotics.IsBigO.trans Asymptotics.IsLittleO.isBigO isLittleO_exp_neg_mul_rpow_atTop lt_add_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
mellin_div_const 📖	mathematical	—	mellin Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace DivInvMonoid.toDiv Complex.instDivInvMonoid	—	MeasureTheory.integral_div
mellin_hasDerivAt_of_isBigO_rpow 📖	mathematical	MeasureTheory.LocallyIntegrableOn Real Real.measurableSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup Set.Ioi Real.instPreorder Real.instZero MeasureTheory.MeasureSpace.volume Real.measureSpace Asymptotics.IsBigO NormedAddCommGroup.toNorm Real.norm Filter.atTop Real.instPow Real.instNeg Real.instLT Complex.re nhdsWithin	MellinConvergent SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid 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.log HasDerivAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField NormedAddCommGroup.toAddCommGroup Complex.instNormedField IsBoundedSMul.continuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField AddCommGroup.toAddCommMonoid NormedSpace.toIsBoundedSMul mellin	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul exists_between LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid lt_min LE.le.trans_lt min_le_right min_le_left Filter.Eventually.of_forall MeasureTheory.AEStronglyMeasurable.smul ContinuousOn.aestronglyMeasurable secondCountableTopologyEither_of_right secondCountable_of_proper Complex.instProperSpace BorelSpace.opensMeasurable Real.borelSpace PseudoEMetricSpace.pseudoMetrizableSpace continuousOn_of_forall_continuousAt Complex.continuousAt_ofReal_cpow_const ne_of_gt measurableSet_Ioi instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal MeasureTheory.LocallyIntegrableOn.aestronglyMeasurable instSecondCountableTopologyReal mellinConvergent_of_isBigO_rpow MeasureTheory.LocallyIntegrableOn.continuousOn_smul locallyCompact_of_proper instProperSpaceReal TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace UniformSpace.secondCountable_of_separable EMetric.instIsCountablyGeneratedUniformity TopologicalSpace.SecondCountableTopology.to_separableSpace NormedSpace.toNormSMulClass IsOpen.isLocallyClosed isOpen_Ioi ContinuousOn.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Continuous.comp_continuousOn Complex.continuous_ofReal ContinuousOn.mono Real.continuousOn_log Set.subset_compl_singleton_iff Set.self_notMem_Ioi MeasureTheory.Measure.instOuterMeasureClass Filter.Eventually.mono MeasureTheory.ae_restrict_mem norm_smul norm_mul NormedDivisionRing.toNormMulClass Complex.norm_real mul_assoc mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing Complex.norm_cpow_eq_rpow_re_of_pos le_or_gt le_add_of_le_of_nonneg Real.rpow_le_rpow_of_exponent_le Complex.sub_re Complex.one_re sub_le_sub_iff_right LE.le.trans Complex.re_le_norm LT.lt.le mem_ball_iff_norm sub_le_iff_le_add' Real.rpow_nonneg zero_le_one Real.instZeroLEOneClass le_add_of_nonneg_of_le Real.rpow_pos_of_pos Real.rpow_le_rpow_of_exponent_ge sub_le_iff_le_add sub_add_cancel mem_ball_iff_norm' mul_nonneg IsOrderedRing.toPosMulMono abs_nonneg norm_nonneg add_mul Distrib.rightDistribClass mellin_convergent_of_isBigO_scalar mul_comm MeasureTheory.LocallyIntegrableOn.mul_continuousOn MeasureTheory.LocallyIntegrableOn.norm continuous_abs instOrderTopologyReal Asymptotics.IsBigO.congr_left Asymptotics.IsBigO.norm_left isBigO_rpow_top_log_smul isBigO_rpow_zero_log_smul MeasureTheory.Integrable.add IsTopologicalSemiring.toContinuousAdd instIsTopologicalRingReal lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_zero 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_zero_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le 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 Mathlib.Tactic.Linarith.sub_nonpos_of_le Complex.ofReal_ne_zero IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology ContinuousMul.to_continuousSMul Complex.ofReal_log le_of_lt Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Nat.cast_one HasDerivAt.const_cpow HasDerivAt.sub_const hasDerivAt_id' HasDerivAt.smul_const IsScalarTower.left hasDerivAt_integral_of_dominated_loc_of_deriv_le Metric.ball_mem_nhds SemigroupAction.mul_smul HasDerivAt.congr_simp

---

← Back to Index