MultipliableUniformlyOn

📁 Source: Mathlib/Analysis/Normed/Module/MultipliableUniformlyOn.lean

Statistics

Metric	Count
Definitions	0
Theorems hasProdLocallyUniformlyOn_nat_one_add, hasProdLocallyUniformlyOn_one_add, hasProdUniformlyOn_nat_one_add, hasProdUniformlyOn_one_add, hasSumUniformlyOn_log_one_add, multipliableLocallyUniformlyOn_nat_one_add, multipliableLocallyUniformlyOn_one_add, multipliableUniformlyOn_nat_one_add, multipliableUniformlyOn_one_add, tendstoUniformlyOn_tsum_nat_log_one_add, comp_cexp, hasProdUniformlyOn_of_clog, multipliableUniformlyOn_of_clog	13
Total	13

Summable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasProdLocallyUniformlyOn_nat_one_add 📖	mathematical	IsOpen Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional Filter.Eventually Filter.atTop Nat.instPreorder ContinuousOn SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing	HasProdLocallyUniformlyOn CommRing.toCommMonoid NormedCommRing.toCommRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing tprod	—	hasProdLocallyUniformlyOn_one_add Nat.cofinite_eq_atTop
hasProdLocallyUniformlyOn_one_add 📖	mathematical	IsOpen Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional ContinuousOn SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing	HasProdLocallyUniformlyOn CommRing.toCommMonoid NormedCommRing.toCommRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing tprod	—	hasProdLocallyUniformlyOn_of_forall_compact hasProdUniformlyOn_one_add Filter.mp_mem Filter.univ_mem' ContinuousOn.mono
hasProdUniformlyOn_nat_one_add 📖	mathematical	IsCompact Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional Filter.Eventually Filter.atTop Nat.instPreorder ContinuousOn SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing	HasProdUniformlyOn CommRing.toCommMonoid NormedCommRing.toCommRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing tprod	—	hasProdUniformlyOn_one_add Nat.cofinite_eq_atTop
hasProdUniformlyOn_one_add 📖	mathematical	IsCompact Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional ContinuousOn SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing	HasProdUniformlyOn CommRing.toCommMonoid NormedCommRing.toCommRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing tprod	—	Finset.isDirected_le continuousOn_iff_continuous_restrict isCompact_iff_compactSpace Set.nonempty_coe_sort Set.nonempty_iff_ne_empty Filter.mp_mem Filter.univ_mem' IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing IsTopologicalSemiring.toContinuousAdd multipliable_one_add_of_summable ContinuousMap.instNormOneClassOfNonempty ContinuousMap.instCompleteSpaceOfCompactlyCoherentSpace CompactlyCoherentSpace.of_weaklyLocallyCompactSpace instWeaklyLocallyCompactSpaceOfCompactSpace of_norm_bounded_eventually Real.instCompleteSpace norm_norm Finset.prod_congr ContinuousMap.coe_prod Finset.prod_apply ContinuousMap.tprod_apply TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SummationFilter.instNeBotUnconditional ContinuousMap.tendsto_iff_tendstoUniformly Multipliable.hasProd
hasSumUniformlyOn_log_one_add 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional	HasSumUniformlyOn Complex ESeminormedAddCommMonoid.toAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Complex.log Complex.instAdd Complex.instOne tsum	—	tendstoUniformlyOn_tsum_of_cofinite_eventually Complex.instCompleteSpace Nat.instAtLeastTwoHAddOfNat mul_left IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Filter.mp_mem Filter.Tendsto.eventually_le_const instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid one_half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing tendsto_cofinite_zero instIsTopologicalAddGroupReal Filter.univ_mem' LE.le.trans Complex.norm_log_one_add_half_le_self IsOrderedRing.toPosMulMono Real.instIsOrderedRing Real.instNontrivial
multipliableLocallyUniformlyOn_nat_one_add 📖	mathematical	IsOpen Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional Filter.Eventually Filter.atTop Nat.instPreorder ContinuousOn SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing	MultipliableLocallyUniformlyOn CommRing.toCommMonoid NormedCommRing.toCommRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing	—	hasProdLocallyUniformlyOn_nat_one_add
multipliableLocallyUniformlyOn_one_add 📖	mathematical	IsOpen Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional ContinuousOn SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing	MultipliableLocallyUniformlyOn CommRing.toCommMonoid NormedCommRing.toCommRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing	—	hasProdLocallyUniformlyOn_one_add
multipliableUniformlyOn_nat_one_add 📖	mathematical	IsCompact Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional Filter.Eventually Filter.atTop Nat.instPreorder ContinuousOn SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing	MultipliableUniformlyOn CommRing.toCommMonoid NormedCommRing.toCommRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing	—	hasProdUniformlyOn_nat_one_add
multipliableUniformlyOn_one_add 📖	mathematical	IsCompact Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional ContinuousOn SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing	MultipliableUniformlyOn CommRing.toCommMonoid NormedCommRing.toCommRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing	—	hasProdUniformlyOn_one_add
tendstoUniformlyOn_tsum_nat_log_one_add 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SummationFilter.unconditional Filter.Eventually Filter.atTop Nat.instPreorder	TendstoUniformlyOn Complex SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Finset.range Complex.log Complex.instAdd Complex.instOne tsum	—	HasSumUniformlyOn.tendstoUniformlyOn_finsetRange hasSumUniformlyOn_log_one_add Nat.cofinite_eq_atTop

TendstoUniformlyOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_cexp 📖	mathematical	TendstoUniformlyOn Complex PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField BddAbove Real Real.instLE Set.image Complex.re	Complex.exp	—	eventually_forall_le instIsUniformAddGroupReal instOrderTopologyReal IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add lt_add_one Real.instZeroLEOneClass NeZero.one Real.instNontrivial IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd re UniformContinuousOn.comp_tendstoUniformlyOn_eventually LE.le.trans LT.lt.le UniformContinuousOn.cexp

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasProdUniformlyOn_of_clog 📖	mathematical	SummableUniformlyOn Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Complex.log BddAbove Real Real.instLE Set.image Complex.re tsum SummationFilter.unconditional	HasProdUniformlyOn CommRing.toCommMonoid Complex.commRing tprod	—	SummableUniformlyOn.exists TendstoUniformlyOn.congr TendstoUniformlyOn.comp_cexp HasSumUniformlyOn.tendstoUniformlyOn Set.image_congr HasSumUniformlyOn.tsum_eqOn Complex.instT2Space Filter.univ_mem' Complex.exp_sum Finset.prod_congr Complex.exp_log TendstoUniformlyOn.congr_right Set.EqOn.trans Set.EqOn.symm Set.EqOn.comp_left Complex.cexp_tsum_eq_tprod SummableUniformlyOn.summable
multipliableUniformlyOn_of_clog 📖	mathematical	SummableUniformlyOn Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Complex.log BddAbove Real Real.instLE Set.image Complex.re tsum SummationFilter.unconditional	MultipliableUniformlyOn CommRing.toCommMonoid Complex.commRing	—	hasProdUniformlyOn_of_clog

---

← Back to Index