OAI/GroupTheory/PolycyclicRecognition/Analysis/CyclicInvariantMean.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Invariant means on cyclic groups from literal power averages

  1. def OAI.PolycyclicRecognition.cyclicMeanState line 19
  2. theorem OAI.PolycyclicRecognition.cyclicMeanState_positive line 24
  3. theorem OAI.PolycyclicRecognition.cyclicMeanState_one line 28
  4. theorem OAI.PolycyclicRecognition.cyclicMeanState_generator_defect line 33

    Source documentation

    The generator defect telescopes without any injectivity assumption on the powers. The same averages work for finite and infinite cyclic groups.

    theorem cyclicMeanState_generator_defect (a : G) (n : ℕ) (f : BoundedReal G) :
    cyclicMeanState a n (leftPull a f) - cyclicMeanState a n f =
      (f (a ^ (n + 1)) - f 1) / ((n : ℝ) + 1) := by
…

    Mentions: OAI.PolycyclicRecognition.cyclicMeanState

  5. theorem OAI.PolycyclicRecognition.invariantMean_of_zpowers_eq_top line 50
  6. theorem OAI.PolycyclicRecognition.invariantMean_of_isCyclic line 73