NormedSpace

📁 Source: Mathlib/Dynamics/BirkhoffSum/NormedSpace.lean

Statistics

Metric	Count
Definitions	0
Theorems tendsto_birkhoffAverage, dist_birkhoffAverage_apply_birkhoffAverage, dist_birkhoffAverage_birkhoffAverage, dist_birkhoffAverage_birkhoffAverage_le, dist_birkhoffSum_apply_birkhoffSum, dist_birkhoffSum_birkhoffSum_le, isClosed_setOf_tendsto_birkhoffAverage, tendsto_birkhoffAverage_apply_sub_birkhoffAverage, tendsto_birkhoffAverage_apply_sub_birkhoffAverage', uniformEquicontinuous_birkhoffAverage	10
Total	10

Function.IsFixedPt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendsto_birkhoffAverage 📖	mathematical	Function.IsFixedPt	Filter.Tendsto birkhoffAverage Filter.atTop Nat.instPreorder nhds	—	Filter.Tendsto.congr' Filter.Eventually.mono Filter.eventually_ne_atTop instNoTopOrderOfNoMaxOrder Nat.instNoMaxOrder birkhoffAverage_eq tendsto_const_nhds

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist_birkhoffAverage_apply_birkhoffAverage 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup birkhoffAverage Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real DivInvMonoid.toDiv Real.instDivInvMonoid Nat.iterate Real.instNatCast	—	dist_birkhoffAverage_birkhoffAverage dist_birkhoffSum_apply_birkhoffSum
dist_birkhoffAverage_birkhoffAverage 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup birkhoffAverage Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real DivInvMonoid.toDiv Real.instDivInvMonoid birkhoffSum Real.instNatCast	—	dist_smul₀ NormedSpace.toNormSMulClass norm_inv RCLike.norm_natCast div_eq_inv_mul
dist_birkhoffAverage_birkhoffAverage_le 📖	mathematical	—	Real Real.instLE Dist.dist PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup birkhoffAverage Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule DivInvMonoid.toDiv Real.instDivInvMonoid Finset.sum Real.instAddCommMonoid Finset.range Nat.iterate Real.instNatCast	—	Eq.trans_le dist_birkhoffAverage_birkhoffAverage div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing dist_birkhoffSum_birkhoffSum_le Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass
dist_birkhoffSum_apply_birkhoffSum 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup birkhoffSum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Nat.iterate	—	dist_eq_norm birkhoffSum_apply_sub_birkhoffSum
dist_birkhoffSum_birkhoffSum_le 📖	mathematical	—	Real Real.instLE Dist.dist PseudoMetricSpace.toDist SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup birkhoffSum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Finset.sum Real.instAddCommMonoid Finset.range Nat.iterate	—	dist_sum_sum_le
isClosed_setOf_tendsto_birkhoffAverage 📖	mathematical	LipschitzWith NNReal instOneNNReal UniformContinuous PseudoEMetricSpace.toUniformSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Continuous UniformSpace.toTopologicalSpace	IsClosed setOf Filter.Tendsto birkhoffAverage Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Filter.atTop Nat.instPreorder nhds	—	Equicontinuous.isClosed_setOf_tendsto UniformEquicontinuous.equicontinuous uniformEquicontinuous_birkhoffAverage
tendsto_birkhoffAverage_apply_sub_birkhoffAverage 📖	mathematical	Bornology.IsBounded PseudoMetricSpace.toBornology SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.range Nat.iterate	Filter.Tendsto SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup birkhoffAverage Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Filter.atTop Nat.instPreorder nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Metric.isBounded_range_iff Filter.Tendsto.div_atTop Real.instIsStrictOrderedRing instOrderTopologyReal tendsto_const_nhds tendsto_natCast_atTop_atTop Real.instIsOrderedRing Real.instArchimedean squeeze_zero_norm dist_eq_norm dist_birkhoffAverage_apply_birkhoffAverage div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass
tendsto_birkhoffAverage_apply_sub_birkhoffAverage' 📖	mathematical	Bornology.IsBounded PseudoMetricSpace.toBornology SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.range	Filter.Tendsto SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup birkhoffAverage Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Filter.atTop Nat.instPreorder nhds NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	tendsto_birkhoffAverage_apply_sub_birkhoffAverage Bornology.IsBounded.subset Set.range_comp_subset_range
uniformEquicontinuous_birkhoffAverage 📖	mathematical	LipschitzWith NNReal instOneNNReal UniformContinuous PseudoEMetricSpace.toUniformSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	UniformEquicontinuous birkhoffAverage Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule	—	Filter.HasBasis.uniformEquicontinuous_iff_right Metric.uniformity_basis_dist_le Filter.HasBasis.uniformContinuous_iff uniformity_basis_edist_le mem_uniformity_edist dist_birkhoffAverage_birkhoffAverage_le div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid one_pow one_mul LipschitzWith.edist_le_mul_of_le LipschitzWith.iterate LT.lt.le Nat.cast_nonneg' Real.instZeroLEOneClass Finset.sum_const Finset.card_range nsmul_eq_mul eq_or_ne CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike MulZeroClass.zero_mul div_zero mul_div_cancel_left₀ GroupWithZero.toMulDivCancelClass

---

← Back to Index