Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `birkhoffSum`	1
Theorems `birkhoffSum_eq`, `birkhoffSum_add`, `birkhoffSum_add'`, `birkhoffSum_apply_sub_birkhoffSum`, `birkhoffSum_neg`, `birkhoffSum_of_comp_eq`, `birkhoffSum_one`, `birkhoffSum_one'`, `birkhoffSum_sub`, `birkhoffSum_succ`, `birkhoffSum_succ'`, `birkhoffSum_zero`, `birkhoffSum_zero'`, `map_birkhoffSum`	14
Total	15

Function.IsFixedPt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`birkhoffSum_eq` 📖	mathematical	`Function.IsFixedPt`	`birkhoffSum` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid`	—	`Finset.sum_congr` `eq` `iterate` `Finset.sum_const` `Finset.card_range`

(root)

Definitions

Name	Category	Theorems
`birkhoffSum` 📖	CompOp	18 math math: `birkhoffSum_add`, `birkhoffSum_succ`, `dist_birkhoffSum_birkhoffSum_le`, `birkhoffSum_apply_sub_birkhoffSum`, `birkhoffSum_zero`, `MeasureTheory.Measure.QuasiMeasurePreserving.birkhoffSum_ae_eq_of_ae_eq`, `map_birkhoffSum`, `birkhoffSum_of_comp_eq`, `dist_birkhoffAverage_birkhoffAverage`, `birkhoffSum_zero'`, `birkhoffSum_one'`, `dist_birkhoffSum_apply_birkhoffSum`, `birkhoffSum_add'`, `birkhoffSum_sub`, `birkhoffSum_neg`, `Function.IsFixedPt.birkhoffSum_eq`, `birkhoffSum_one`, `birkhoffSum_succ'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`birkhoffSum_add` 📖	mathematical	—	`birkhoffSum` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Nat.iterate`	—	`Finset.sum_range_add` `Finset.sum_congr` `add_comm` `Function.iterate_add_apply`
`birkhoffSum_add'` 📖	mathematical	—	`birkhoffSum` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`Finset.sum_congr` `Finset.sum_add_distrib`
`birkhoffSum_apply_sub_birkhoffSum` 📖	mathematical	—	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `birkhoffSum` `AddCommGroup.toAddCommMonoid` `Nat.iterate`	—	`sub_eq_iff_eq_add` `birkhoffSum_succ` `birkhoffSum_succ'` `sub_add` `sub_add_comm`
`birkhoffSum_neg` 📖	mathematical	—	`birkhoffSum` `AddCommGroup.toAddCommMonoid` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`Finset.sum_congr` `Finset.sum_neg_distrib`
`birkhoffSum_of_comp_eq` 📖	mathematical	—	`birkhoffSum` `AddMonoid.toNatSMul` `Pi.addMonoid` `AddCommMonoid.toAddMonoid`	—	`Function.iterate_invariant` `Finset.sum_congr` `Finset.sum_const` `Finset.card_range`
`birkhoffSum_one` 📖	mathematical	—	`birkhoffSum`	—	`Finset.sum_range_one`
`birkhoffSum_one'` 📖	mathematical	—	`birkhoffSum`	—	`birkhoffSum_one`
`birkhoffSum_sub` 📖	mathematical	—	`birkhoffSum` `AddCommGroup.toAddCommMonoid` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`Finset.sum_congr` `Finset.sum_sub_distrib`
`birkhoffSum_succ` 📖	mathematical	—	`birkhoffSum` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Nat.iterate`	—	`Finset.sum_range_succ`
`birkhoffSum_succ'` 📖	mathematical	—	`birkhoffSum` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`Finset.sum_range_succ'` `add_comm`
`birkhoffSum_zero` 📖	mathematical	—	`birkhoffSum` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`Finset.sum_range_zero`
`birkhoffSum_zero'` 📖	mathematical	—	`birkhoffSum` `Pi.instZero` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`birkhoffSum_zero`
`map_birkhoffSum` 📖	mathematical	—	`DFunLike.coe` `birkhoffSum`	—	`map_sum`

---

← Back to Index