LogMeromorphic

📁 Source: Mathlib/Analysis/SpecialFunctions/Integrability/LogMeromorphic.lean

Statistics

Metric	Count
Definitions	0
Theorems intervalIntegrable_log, circleIntegrable_log_norm_factorizedRational, circleIntegrable_log_norm_meromorphicOn, circleIntegrable_log_norm_meromorphicOn_of_nonneg, circleIntegrable_posLog_norm_meromorphicOn, circleIntegrable_posLog_norm_meromorphicOn_of_nonneg, intervalIntegrable_log_cos, intervalIntegrable_log_norm_meromorphicOn, intervalIntegrable_log_sin, intervalIntegrable_posLog_norm_meromorphicOn	10
Total	10

MeromorphicOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
intervalIntegrable_log 📖	mathematical	MeromorphicOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Set.uIcc Real.lattice	IntervalIntegrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup Real.log MeasureTheory.MeasureSpace.volume Real.measureSpace	—	Real.log_abs intervalIntegrable_log_norm_meromorphicOn

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
circleIntegrable_log_norm_factorizedRational 📖	mathematical	—	CircleIntegrable Real Real.normedAddCommGroup finsum Complex Pi.addCommMonoid Real.instAddCommMonoid Real.instMul Real.instIntCast Real.log Norm.norm Complex.instNorm Complex.instSub	—	CircleIntegrable.finsum CircleIntegrable.const_smul circleIntegrable_log_norm_meromorphicOn AnalyticOnNhd.meromorphicOn AnalyticOnNhd.sub analyticOnNhd_id analyticOnNhd_const
circleIntegrable_log_norm_meromorphicOn 📖	mathematical	MeromorphicOn Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Metric.sphere SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField abs Real Real.lattice Real.instAddGroup	CircleIntegrable Real.normedAddCommGroup Real.log Norm.norm NormedAddCommGroup.toNorm	—	MeromorphicOn.extract_zeros_poles Function.locallyFinsuppWithin.finiteSupport Complex.instT2Space isCompact_sphere Complex.instProperSpace MeromorphicOn.extract_zeros_poles_log CircleIntegrable.congr_codiscreteWithin Filter.EventuallyEq.symm CircleIntegrable.add CircleIntegrable.finsum IntervalIntegrable.const_mul intervalIntegrable_log_norm_meromorphicOn AnalyticOnNhd.meromorphicOn AnalyticOnNhd.sub AnalyticOnNhd.mono analyticOnNhd_circleMap analyticOnNhd_const ContinuousOn.intervalIntegrable Real.locallyFinite_volume ContinuousOn.log ContinuousOn.norm ContinuousOn.comp AnalyticOnNhd.continuousOn Continuous.continuousOn continuous_circleMap circleMap_sub_center norm_circleMap_zero norm_eq_zero circleMap_mem_sphere' Filter.mp_mem Filter.self_mem_codiscreteWithin MeromorphicOn.meromorphicNFAt_mem_codiscreteWithin Filter.univ_mem' MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff MeromorphicOn.exists_meromorphicOrderAt_ne_top_iff_forall isConnected_sphere Nat.instAtLeastTwoHAddOfNat Complex.rank_real_complex Cardinal.addLeftMono IsOrderedRing.toZeroLEOneClass Cardinal.isOrderedRing Cardinal.instCharZero abs_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Int.instIsOrderedAddMonoid circleIntegrable_const
circleIntegrable_log_norm_meromorphicOn_of_nonneg 📖	mathematical	MeromorphicOn Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Metric.sphere SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Real Real.instLE Real.instZero	CircleIntegrable Real.normedAddCommGroup Real.log Norm.norm NormedAddCommGroup.toNorm	—	circleIntegrable_log_norm_meromorphicOn abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
circleIntegrable_posLog_norm_meromorphicOn 📖	mathematical	MeromorphicOn Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Metric.sphere SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField abs Real Real.lattice Real.instAddGroup	CircleIntegrable Real.normedAddCommGroup Real.posLog Norm.norm NormedAddCommGroup.toNorm	—	Nat.instAtLeastTwoHAddOfNat mul_add Distrib.leftDistribClass CircleIntegrable.add IntervalIntegrable.const_mul circleIntegrable_log_norm_meromorphicOn CircleIntegrable.abs
circleIntegrable_posLog_norm_meromorphicOn_of_nonneg 📖	mathematical	MeromorphicOn Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Metric.sphere SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Real Real.instLE Real.instZero	CircleIntegrable Real.normedAddCommGroup Real.posLog Norm.norm NormedAddCommGroup.toNorm	—	circleIntegrable_posLog_norm_meromorphicOn abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid
intervalIntegrable_log_cos 📖	mathematical	—	IntervalIntegrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup Real.normedAddCommGroup Real.log Real.cos MeasureTheory.MeasureSpace.volume Real.measureSpace	—	MeromorphicOn.intervalIntegrable_log AnalyticOnNhd.meromorphicOn Real.analyticOnNhd_cos
intervalIntegrable_log_norm_meromorphicOn 📖	mathematical	MeromorphicOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Set.uIcc Real.lattice	IntervalIntegrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup Real.normedAddCommGroup Real.log Norm.norm NormedAddCommGroup.toNorm MeasureTheory.MeasureSpace.volume Real.measureSpace	—	MeromorphicOn.extract_zeros_poles Function.locallyFinsuppWithin.finiteSupport TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace isCompact_uIcc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal MeromorphicOn.extract_zeros_poles_log intervalIntegrable_congr_codiscreteWithin PseudoEMetricSpace.pseudoMetrizableSpace Real.noAtoms_volume Filter.EventuallyEq.filter_mono Filter.codiscreteWithin.mono Set.uIoc_subset_uIcc IntervalIntegrable.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IntervalIntegrable.finsum IntervalIntegrable.const_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr 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_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add IntervalIntegrable.comp_sub_right Real.log_abs enorm_ne_top ContinuousOn.intervalIntegrable Real.locallyFinite_volume ContinuousOn.log ContinuousOn.norm AnalyticOnNhd.continuousOn Filter.mp_mem Filter.self_mem_codiscreteWithin MeromorphicOn.meromorphicNFAt_mem_codiscreteWithin Filter.univ_mem' MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff MeromorphicOn.exists_meromorphicOrderAt_ne_top_iff_forall isConnected_Icc LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing inf_le_sup Int.instIsOrderedAddMonoid intervalIntegrable_const_iff
intervalIntegrable_log_sin 📖	mathematical	—	IntervalIntegrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup Real.normedAddCommGroup Real.log Real.sin MeasureTheory.MeasureSpace.volume Real.measureSpace	—	MeromorphicOn.intervalIntegrable_log AnalyticOnNhd.meromorphicOn Real.analyticOnNhd_sin
intervalIntegrable_posLog_norm_meromorphicOn 📖	mathematical	MeromorphicOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Set.uIcc Real.lattice	IntervalIntegrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup Real.normedAddCommGroup Real.posLog Norm.norm NormedAddCommGroup.toNorm MeasureTheory.MeasureSpace.volume Real.measureSpace	—	Nat.instAtLeastTwoHAddOfNat mul_add Distrib.leftDistribClass IntervalIntegrable.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IntervalIntegrable.const_mul intervalIntegrable_log_norm_meromorphicOn IntervalIntegrable.abs

---

← Back to Index