MeanErgodic

📁 Source: Mathlib/Analysis/InnerProductSpace/MeanErgodic.lean

Statistics

Metric	Count
Definitions	0
Theorems tendsto_birkhoffAverage_orthogonalProjection, tendsto_birkhoffAverage_of_ker_subset_closure	2
Total	2

ContinuousLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendsto_birkhoffAverage_orthogonalProjection 📖	mathematical	Real Real.instLE Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace hasOpNorm DenselyNormedField.toNontriviallyNormedField Real.instOne	Filter.Tendsto birkhoffAverage DFunLike.coe funLike Filter.atTop Nat.instPreorder nhds Submodule SetLike.instMembership Submodule.setLike LinearMap.eqLocus ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass one instTopologicalSpaceSubtype Submodule.addCommMonoid Submodule.module Submodule.orthogonalProjection Submodule.HasOrthogonalProjection.ofCompleteSpace completeSpace_eqLocus TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace	—	LinearMap.tendsto_birkhoffAverage_of_ker_subset_closure LipschitzWith.weaken RingHomIsometric.ids lipschitz ContinuousSemilinearMapClass.toSemilinearMapClass continuousSemilinearMapClass Submodule.HasOrthogonalProjection.ofCompleteSpace completeSpace_eqLocus TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Submodule.orthogonalProjection_mem_subspace_eq_self LinearMap.semilinearMapClass RingHomSurjective.ids Submodule.ker_orthogonalProjection UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup Submodule.topologicalClosure_coe SetLike.coe_subset_coe instIsConcreteLE Submodule.orthogonal_orthogonal_eq_closure Submodule.orthogonal_le eq_of_norm_le_re_inner_eq_norm_sq one_mul le_of_opNorm_le inner_sub_left inner_self_eq_norm_sq_to_K RCLike.re_ofReal_pow

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tendsto_birkhoffAverage_of_ker_subset_closure 📖	mathematical	LipschitzWith EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace NNReal instOneNNReal DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule instFunLike ContinuousLinearMap Submodule SetLike.instMembership Submodule.setLike eqLocus semilinearMapClass Module.End.instOne instTopologicalSpaceSubtype Submodule.addCommMonoid Submodule.module ContinuousLinearMap.funLike Set Set.instHasSubset SetLike.coe ker ContinuousLinearMap.toLinearMap closure range RingHomSurjective.ids instSub SeminormedAddCommGroup.toAddCommGroup	Filter.Tendsto birkhoffAverage Filter.atTop Nat.instPreorder nhds	—	semilinearMapClass RingHomSurjective.ids map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass sub_self sub_add_cancel isClosed_setOf_tendsto_birkhoffAverage uniformContinuous_id continuous_const closure_minimal Set.forall_mem_range isBounded_iff_forall_norm_le iterate_map_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass dist_zero_right one_pow one_mul LipschitzWith.dist_le_mul LipschitzWith.iterate iterate_map_sub Finset.sum_congr Finset.sum_sub_distrib smul_sub tendsto_birkhoffAverage_apply_sub_birkhoffAverage iterate_map_add SemilinearMapClass.toAddHomClass Finset.sum_add_distrib smul_add map_add zero_add Filter.Tendsto.add IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup Function.IsFixedPt.tendsto_birkhoffAverage RCLike.charZero_rclike

---

← Back to Index