OAI/NumberTheory/DukePrimeDegree/Dynamics/FlowOccupation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

One-unit occupation observables

For a measurable measure-preserving flow, the time spent in a measurable set during one unit interval is a measurable integrable observable. Its space integral is exactly the measure of that set. Its discrete sums are the occupation integrals on the corresponding integer intervals.

  1. lemma OAI.DukePrimeDegree.integrable_one_indicator_comp line 21
  2. def OAI.DukePrimeDegree.unitFlowOccupation line 31
  3. lemma OAI.DukePrimeDegree.measurable_unitFlowOccupation line 34
  4. lemma OAI.DukePrimeDegree.unitFlowOccupation_nonneg line 43
  5. lemma OAI.DukePrimeDegree.unitFlowOccupation_le_one line 50
  6. lemma OAI.DukePrimeDegree.integrable_unitFlowOccupation line 61
  7. theorem OAI.DukePrimeDegree.integral_unitFlowOccupation line 70
  8. lemma OAI.DukePrimeDegree.intervalIntegrable_flow_indicator line 91
  9. lemma OAI.DukePrimeDegree.flow_nat_iterate line 102

    Distinct definitions of this name: OAI/NumberTheory/DukePrimeDegree/Dynamics/FlowWindowAverages.lean:26 (different declaration text). Qualify references as OAI.DukePrimeDegree.flow_nat_iterate@path.

  10. theorem OAI.DukePrimeDegree.birkhoffSum_unitFlowOccupation line 111