Kac's formula: the mean return time is the reciprocal of the measure

Category: 1-Mathlib. No CSD content. Mathlib has Poincaré recurrence (Conservative) and ergodicity but not this, and no return times at all.

★★ tsum_measure_lt_returnTime — for an ergodic measure-preserving map of a probability space and any A with μ A ≠ 0,

∑ₙ μ {x ∈ A : n < n_A x} = 1,

where n_A x is the first n ≥ 1 with f^[n] x ∈ A. The left side is the expectation of n_A over A, so conditioning on starting in A the mean return time is exactly 1 / μ A (tsum_measure_lt_returnTime_div).

The proof avoids the tower

The textbook proof builds the Kakutani skyscraper and needs the pieces f^k(Aₙ) to be disjoint and to exhaust the space — the awkward part to formalise. This is the telescoping proof instead, which uses no images at all, only preimages, where measure preservation applies directly.

Write notYet f A n for the points whose iterates 0, …, n-1 all miss A. Everything turns on one identity (measure_notYet_succ):

f ⁻¹' (notYet n) splits into A ∩ f ⁻¹' (notYet n) and notYet (n+1), and measure preservation turns its measure back into μ (notYet n).

Telescoping gives ∑_{n<N} μ (A ∩ f ⁻¹' notYet n) + μ (notYet N) = 1, ergodicity kills the tail (a.e. point eventually meets A), and inter_lt_returnTime identifies each summand as {x ∈ A : n_A x > n}.

⚠️ returnTime is ℕ∞-valued, and that is not cosmetic

With a natural-number junk value the bridge lemma is false: a point that never returns would have n_A = 0, so n < n_A would fail, while it does belong to every notYet n. The two sides disagree exactly on the never-returning set. That set is null here, but the identity is wanted pointwise, so ⊤ is the honest value.

What it is for, and what it is not

specs/q12-fibre-mechanism-scoping.md Q12-d asks for the record layer's first-passage race to come from dynamics rather than a posited clock law. Kac is the part of that which is regime-correct: it holds for any set of positive measure, with no rarity hypothesis — unlike the hitting-time limit theorems (Galves–Schmitt/Abadi), which need μ A → 0 and so cannot be instantiated on a Born partition, whose cells have measures summing to one.

⚠️ So this supplies the rates — mean return time to a cell of measure bᵢ is 1/bᵢ, derived from the dynamics — and not the exponential law. The law does not follow, and the Q12-d row records why.

Reference: specs/q12-fibre-mechanism-scoping.md; specs/record-layer-plan.md §3c; specs/future-work.md.

The sets that have not met A yet

def MeasureTheory.notYet {α : Type u_1} (f : α → α) (A : Set α) : ℕ → Set α

The points that have not met A yet: those whose iterates at times 0, …, n-1 all miss A. Defined by recursion rather than as an intersection, because the recursion is the identity the whole proof turns on.

Equations

• MeasureTheory.notYet f A 0 = Set.univ
• MeasureTheory.notYet f A n.succ = Aᶜ ∩ f ⁻¹' MeasureTheory.notYet f A n

@[simp]

theorem MeasureTheory.notYet_zero {α : Type u_1} {f : α → α} {A : Set α} : notYet f A 0 = Set.univ

@[simp]

theorem MeasureTheory.notYet_succ {α : Type u_1} {f : α → α} {A : Set α} (n : ℕ) : notYet f A (n + 1) = Aᶜ ∩ f ⁻¹' notYet f A n

theorem MeasureTheory.mem_notYet_iff {α : Type u_1} {f : α → α} {A : Set α} (n : ℕ) (x : α) : x ∈ notYet f A n ↔ ∀ k < n, f^[k] x ∉ A

theorem MeasureTheory.measurableSet_notYet {α : Type u_1} {f : α → α} {A : Set α} [MeasurableSpace α] (hf : Measurable f) (hA : MeasurableSet A) (n : ℕ) : MeasurableSet (notYet f A n)

The one identity, and the telescope

theorem MeasureTheory.measure_notYet_succ {α : Type u_1} {f : α → α} {A : Set α} [MeasurableSpace α] {μ : Measure α} (hf : MeasurePreserving f μ μ) (hA : MeasurableSet A) (hfm : Measurable f) (n : ℕ) : μ (notYet f A n) = μ (A ∩ f ⁻¹' notYet f A n) + μ (notYet f A (n + 1))

★★ The telescoping step. The preimage of notYet n splits into the points of A that have not returned within n steps, and notYet (n+1); measure preservation identifies its measure with μ (notYet n).

theorem MeasureTheory.sum_measure_inter_notYet {α : Type u_1} {f : α → α} {A : Set α} [MeasurableSpace α] {μ : Measure α} [IsProbabilityMeasure μ] (hf : MeasurePreserving f μ μ) (hA : MeasurableSet A) (hfm : Measurable f) (N : ℕ) : ∑ n ∈ Finset.range N, μ (A ∩ f ⁻¹' notYet f A n) + μ (notYet f A N) = 1

The telescoped partial sums: the mass that has already returned by time N, plus the mass that has not, is everything.

Ergodicity kills the tail

theorem MeasureTheory.measure_iInter_notYet_eq_zero {α : Type u_1} {f : α → α} {A : Set α} [MeasurableSpace α] {μ : Measure α} [IsProbabilityMeasure μ] (hf : MeasurePreserving f μ μ) (herg : PreErgodic f μ) (hA : MeasurableSet A) (hApos : μ A ≠ 0) (hfm : Measurable f) : μ (⋂ (n : ℕ), notYet f A n) = 0

Almost every point eventually meets A, so the set that never does is null.

The return time, and Kac's formula

noncomputable def MeasureTheory.returnTime {α : Type u_1} (f : α → α) (A : Set α) (x : α) : ℕ∞

The first return time to A, valued in ℕ∞ with ⊤ for points that never return. The ⊤ is load-bearing — see the module docstring.

Equations

• MeasureTheory.returnTime f A x = if h : ∃ (n : ℕ), 1 ≤ n ∧ f^[n] x ∈ A then ↑(Nat.find h) else ⊤

theorem MeasureTheory.lt_returnTime_iff {α : Type u_1} {f : α → α} {A : Set α} (n : ℕ) (x : α) : ↑n < returnTime f A x ↔ f x ∈ notYet f A n

★ The bridge. Starting anywhere, "the first return exceeds n" is exactly "the n steps after the first all miss A". This is what lets the whole proof avoid mentioning returnTime.

theorem MeasureTheory.inter_lt_returnTime {α : Type u_1} {f : α → α} {A : Set α} (n : ℕ) : A ∩ {x : α | ↑n < returnTime f A x} = A ∩ f ⁻¹' notYet f A n

theorem MeasureTheory.tsum_measure_lt_returnTime {α : Type u_1} {f : α → α} {A : Set α} [MeasurableSpace α] {μ : Measure α} [IsProbabilityMeasure μ] (hf : MeasurePreserving f μ μ) (herg : PreErgodic f μ) (hA : MeasurableSet A) (hApos : μ A ≠ 0) (hfm : Measurable f) : ∑' (n : ℕ), μ (A ∩ {x : α | ↑n < returnTime f A x}) = 1

★★★ Kac's formula. For an ergodic measure-preserving map of a probability space and any A of positive measure, the expected first return time to A, summed over A, is exactly one.

Since ∑ₙ μ {x ∈ A : n_A x > n} is the expectation of n_A restricted to A, dividing by μ A gives the mean return time conditioned on starting in A as 1 / μ A (tsum_measure_lt_returnTime_div). Small cells are returned to rarely, in exact proportion.

theorem MeasureTheory.tsum_measure_lt_returnTime_div {α : Type u_1} {f : α → α} {A : Set α} [MeasurableSpace α] {μ : Measure α} [IsProbabilityMeasure μ] (hf : MeasurePreserving f μ μ) (herg : PreErgodic f μ) (hA : MeasurableSet A) (hApos : μ A ≠ 0) (hfm : Measurable f) : (∑' (n : ℕ), μ (A ∩ {x : α | ↑n < returnTime f A x})) / μ A = 1 / μ A

★★ The mean return time is 1 / μ A. Kac's formula, normalised by the measure of A — the form the record layer reads: a cell of Born weight bᵢ is returned to on average every 1/bᵢ steps.