Documentation Verification Report

Average

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

Statistics

Metric	Count
Definitions `birkhoffAverage`	1
Theorems `birkhoffAverage_eq`, `birkhoffAverage_add`, `birkhoffAverage_apply_sub_birkhoffAverage`, `birkhoffAverage_congr_ring`, `birkhoffAverage_congr_ring'`, `birkhoffAverage_neg`, `birkhoffAverage_of_comp_eq`, `birkhoffAverage_one`, `birkhoffAverage_one'`, `birkhoffAverage_sub`, `birkhoffAverage_zero`, `birkhoffAverage_zero'`, `map_birkhoffAverage`	13
Total	14

Function.IsFixedPt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`birkhoffAverage_eq` 📖	mathematical	`Function.IsFixedPt`	`birkhoffAverage`	—	`birkhoffAverage.eq_1` `birkhoffSum_eq` `Nat.cast_smul_eq_nsmul` `inv_smul_smul₀` `Nat.cast_ne_zero`

(root)

Definitions

Name	Category	Theorems
`birkhoffAverage` 📖	CompOp	24 math math: `tendsto_birkhoffAverage_apply_sub_birkhoffAverage'`, `birkhoffAverage_add`, `birkhoffAverage_of_comp_eq`, `tendsto_birkhoffAverage_apply_sub_birkhoffAverage`, `map_birkhoffAverage`, `birkhoffAverage_neg`, `isClosed_setOf_tendsto_birkhoffAverage`, `dist_birkhoffAverage_apply_birkhoffAverage`, `dist_birkhoffAverage_birkhoffAverage`, `Function.IsFixedPt.birkhoffAverage_eq`, `birkhoffAverage_congr_ring'`, `MeasureTheory.Measure.QuasiMeasurePreserving.birkhoffAverage_ae_eq_of_ae_eq`, `birkhoffAverage_zero`, `birkhoffAverage_one`, `birkhoffAverage_one'`, `uniformEquicontinuous_birkhoffAverage`, `birkhoffAverage_sub`, `ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection`, `birkhoffAverage_zero'`, `birkhoffAverage_congr_ring`, `dist_birkhoffAverage_birkhoffAverage_le`, `birkhoffAverage_apply_sub_birkhoffAverage`, `LinearMap.tendsto_birkhoffAverage_of_ker_subset_closure`, `Function.IsFixedPt.tendsto_birkhoffAverage`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`birkhoffAverage_add` 📖	mathematical	—	`birkhoffAverage` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`Finset.sum_congr` `Finset.sum_add_distrib` `smul_add`
`birkhoffAverage_apply_sub_birkhoffAverage` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `birkhoffAverage` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Module.toDistribMulAction` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `DivisionSemiring.toGroupWithZero` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Nat.iterate`	—	`birkhoffSum_apply_sub_birkhoffSum`
`birkhoffAverage_congr_ring` 📖	mathematical	—	`birkhoffAverage`	—	`map_birkhoffAverage` `AddMonoidHom.instAddMonoidHomClass`
`birkhoffAverage_congr_ring'` 📖	mathematical	—	`birkhoffAverage`	—	`birkhoffAverage_congr_ring`
`birkhoffAverage_neg` 📖	mathematical	—	`birkhoffAverage` `AddCommGroup.toAddCommMonoid` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`Finset.sum_congr` `Finset.sum_neg_distrib` `smul_neg`
`birkhoffAverage_of_comp_eq` 📖	mathematical	—	`birkhoffAverage` `AddCommGroup.toAddCommMonoid`	—	`Nat.cast_smul_eq_nsmul` `SemigroupAction.mul_smul` `inv_mul_cancel₀` `Nat.cast_zero` `one_smul` `birkhoffSum_of_comp_eq`
`birkhoffAverage_one` 📖	mathematical	—	`birkhoffAverage`	—	`Nat.cast_one` `inv_one` `birkhoffSum_one'` `one_smul`
`birkhoffAverage_one'` 📖	mathematical	—	`birkhoffAverage`	—	`birkhoffAverage_one`
`birkhoffAverage_sub` 📖	mathematical	—	`birkhoffAverage` `AddCommGroup.toAddCommMonoid` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`Finset.sum_congr` `Finset.sum_sub_distrib` `smul_sub`
`birkhoffAverage_zero` 📖	mathematical	—	`birkhoffAverage` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`Nat.cast_zero` `inv_zero` `birkhoffSum_zero'` `smul_zero`
`birkhoffAverage_zero'` 📖	mathematical	—	`birkhoffAverage` `Pi.instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`birkhoffAverage_zero`
`map_birkhoffAverage` 📖	mathematical	—	`DFunLike.coe` `birkhoffAverage`	—	`map_inv_natCast_smul` `map_birkhoffSum`

---

← Back to Index