Kingman's subadditive ergodic theorem

TheoremKingman's subadditive ergodic theorem (nonnegative case)#✓fully proved

Let \(\mu\) be a probability measure on a measurable space \(\alpha\) and let \(T : \alpha \to \alpha\) preserve \(\mu\). Let \((f_n)_{n \in \mathbb{N}}\) be functions \(\alpha \to \mathbb{R}\), each measurable and \(\mu\)-integrable, such that for every \(n\) the inequality \(f_n \ge 0\) holds \(\mu\)-almost everywhere, \(f_0 = 0\) holds \(\mu\)-almost everywhere, and for all natural numbers \(m\) and \(n\) the inequality \(f_{m+n}(x) \le f_m(x) + f_n(T^m x)\) holds for \(\mu\)-almost every \(x\). Then there is a \(\mu\)-integrable function \(g : \alpha \to \mathbb{R}\) such that \(g(T x) = g(x)\) for \(\mu\)-almost every \(x\) and \(f_n(x)/n\) converges to \(g(x)\) as \(n \to \infty\) for \(\mu\)-almost every \(x\).

theorem kingman_subadditive
    {α : Type*} [MeasurableSpace α] {μ : Measure α} [IsProbabilityMeasure μ]
    {T : α → α} (hT : MeasurePreserving T μ μ)
    (f : ℕ → α → ℝ)
    (hf_meas : ∀ n, Measurable (f n))
    (hf_int : ∀ n, Integrable (f n) μ)
    (hf_nonneg : ∀ n, ∀ᵐ x ∂μ, 0 ≤ f n x)
    (hf_zero : ∀ᵐ x ∂μ, f 0 x = 0)
    (hf_subadd : ∀ m n, ∀ᵐ x ∂μ, f (m + n) x ≤ f m x + f n ((T^[m]) x)) :
    ∃ g : α → ℝ, Integrable g μ ∧ (∀ᵐ x ∂μ, g (T x) = g x) ∧
      ∀ᵐ x ∂μ, Tendsto (fun n : ℕ => f n x / (n : ℝ)) atTop (nhds (g x))
Sources
  • J. F. C. Kingman, "The Ergodic Theory of Subadditive Stochastic Processes", Journal of the Royal Statistical Society Series B 30 (1968), 499–510, DOI 10.1111/j.2517-6161.1968.tb00749.x.
Uses 7
Proof usesMaximal divergence set · Invariance of the maximal divergence set under iterates · Measurability of the maximal divergence set · Membership in the maximal divergence set · Birkhoff sums of a function cut off to an invariant set, inside the set · Birkhoff sums of a function cut off to an invariant set, outside the set · Hopf maximal ergodic theorem

TheoremIntegral is invariant under a measure-preserving map#✓fully proved

The integral is invariant under a measure-preserving map: ∫ g ∘ T dμ = ∫ g dμ for a.e.-strongly measurable g.

theorem integral_comp_measurePreserving (T : α → α) (hT : MeasurePreserving T μ μ)
    (g : α → ℝ) (hg : AEStronglyMeasurable g μ) :
    ∫ x, g (T x) ∂μ = ∫ x, g x ∂μ
Used by 2
Used byMaximal ergodic theorem · Invariance of the Kingman limit

TheoremIntegral is invariant under iterates of a measure-preserving map#✓fully proved

The integral is invariant under iterates of a measure-preserving map: ∫ g ∘ T^[m] dμ = ∫ g dμ for a.e.-strongly measurable g. See also MathlibExt.Probability.BirkhoffErgodicL1.integral_comp_iterate_of_measurePreserving, which assumes g integrable.

theorem integral_comp_iterate (T : α → α) (hT : MeasurePreserving T μ μ)
    (g : α → ℝ) (hg : AEStronglyMeasurable g μ) (m : ℕ) :
    ∫ x, g (T^[m] x) ∂μ = ∫ x, g x ∂μ
Used by 4
Used byLower limit of the normalized defect is finite almost everywhere · Expectation of a subadditive cocycle grows at most linearly · Expectations of a subadditive cocycle are subadditive · Time constant is at most the integral of the lower limit

StructureSubadditive cocycle over a measure-preserving map#✓fully proved

X is a subadditive cocycle over T: T preserves μ, every X n is integrable, and X (m + n) ≤ X m + X n ∘ T^[m] almost everywhere.

structure SubadditiveCocycle (T : α → α) (μ : Measure α) (X : ℕ → α → ℝ) : Prop where
  /-- `T` preserves `μ`. -/
  measurePreserving : MeasurePreserving T μ μ
  /-- Every `X n` is integrable. -/
  integrable : ∀ n, Integrable (X n) μ
  /-- The cocycle inequality, almost everywhere. -/
  subadditive : ∀ m n, ∀ᵐ x ∂μ, X (m + n) x ≤ X m x + X n (T^[m] x)
Used by 27
Used byCocycle inequality holds for all indices almost everywhere · Subadditive cocycle bounded by Birkhoff sums of its first term · Block decomposition bound for a subadditive cocycle · Lower limit of the normalized defect is finite almost everywhere · Kingman's theorem: normalized cocycle converges almost everywhere · Normalized expectations of a nonnegative cocycle are bounded below · Kingman's subadditive ergodic theorem for nonnegative cocycles · Expectation of a subadditive cocycle grows at most linearly · Expectations of a subadditive cocycle are subadditive · Upper limit of a cocycle bounded by Birkhoff limits of blocks · Upper and lower limits of a nonnegative cocycle agree · Lower limit of a cocycle is nondecreasing along the map · Upper limit of a normalized cocycle is finite almost everywhere · Time constant of a subadditive cocycle · Time constant is a lower bound for normalized expectations · Time constant is at most the first expectation · Time constant is at most the integral of the lower limit · Integrability of the Kingman limit for nonnegative cocycles · Integral of the Kingman limit is at most the time constant · Kingman's subadditive ergodic theorem · Invariance of the Kingman limit · Expectations of a subadditive cocycle form a subadditive sequence · Almost-everywhere convergence to the Kingman limit · Kingman's subadditive ergodic theorem · Fekete's lemma for the expectations of a subadditive cocycle · Truncated defect is a nonnegative subadditive cocycle · Negative defect is a subadditive cocycle

DefinitionExpectation sequence of a cocycle#✓fully proved

The expectation ∫ X n dμ of the n-th term.

noncomputable def expSeq (X : ℕ → α → ℝ) (μ : Measure α) (n : ℕ) : ℝ := ∫ x, X n x ∂μ
Used by 13
Used byLower limit of the normalized defect is finite almost everywhere · Kingman's theorem: normalized cocycle converges almost everywhere · Normalized expectations of a nonnegative cocycle are bounded below · Expectation of a subadditive cocycle grows at most linearly · Expectations of a subadditive cocycle are subadditive · Time constant of a subadditive cocycle · Time constant is a lower bound for normalized expectations · Time constant is at most the first expectation · Time constant is at most the integral of the lower limit · Integral of the Kingman limit is at most the time constant · Kingman's subadditive ergodic theorem · Expectations of a subadditive cocycle form a subadditive sequence · Fekete's lemma for the expectations of a subadditive cocycle

TheoremExpectations of a subadditive cocycle are subadditive#✓fully proved

The expectations of a subadditive cocycle are subadditive.

theorem expSeq_subadditive (h : SubadditiveCocycle T μ X) (m n : ℕ) :
    expSeq X μ (m + n) ≤ expSeq X μ m + expSeq X μ n
Uses 3 · Used by 1
Statement usesSubadditive cocycle over a measure-preserving map · Expectation sequence of a cocycle
Proof usesIntegral is invariant under iterates of a measure-preserving map
Used byExpectations of a subadditive cocycle form a subadditive sequence

TheoremExpectations of a subadditive cocycle form a subadditive sequence#✓fully proved

The expectations of a subadditive cocycle form a Subadditive sequence.

theorem subadditive_expSeq (h : SubadditiveCocycle T μ X) :
    Subadditive (expSeq X μ)
Uses 3 · Used by 4
Statement usesSubadditive cocycle over a measure-preserving map · Expectation sequence of a cocycle
Proof usesExpectations of a subadditive cocycle are subadditive
Used byTime constant of a subadditive cocycle · Time constant is a lower bound for normalized expectations · Integral of the Kingman limit is at most the time constant · Fekete's lemma for the expectations of a subadditive cocycle

TheoremSubadditive cocycle bounded by Birkhoff sums of its first term#✓fully proved

Iterating subadditivity: X n ≤ ∑_{k<n} X 1 ∘ T^[k] almost everywhere, for all n ≥ 1.

theorem ae_le_birkhoffSum (h : SubadditiveCocycle T μ X) :
    ∀ᵐ x ∂μ, ∀ n, 1 ≤ n → X n x ≤ birkhoffSum T (X 1) n x
Uses 1 · Used by 2
Statement usesSubadditive cocycle over a measure-preserving map
Used byLower limit of the normalized defect is finite almost everywhere · Expectation of a subadditive cocycle grows at most linearly

TheoremExpectation of a subadditive cocycle grows at most linearly#✓fully proved

∫ X n dμ ≤ n ∫ X 1 dμ for n ≥ 1.

theorem expSeq_le_nsmul (h : SubadditiveCocycle T μ X) {n : ℕ} (hn : 1 ≤ n) :
    expSeq X μ n ≤ n • expSeq X μ 1
Uses 5
Statement usesSubadditive cocycle over a measure-preserving map · Expectation sequence of a cocycle
Proof usesIntegrability of Birkhoff sums · Subadditive cocycle bounded by Birkhoff sums of its first term · Integral is invariant under iterates of a measure-preserving map

DefinitionTime constant of a subadditive cocycle#✓fully proved

The time constant lim_n (∫ X n dμ) / n = inf_n (∫ X n dμ) / n (Fekete's lemma); it is meaningful when expSeq n / n is bounded below.

noncomputable def gamma (h : SubadditiveCocycle T μ X) : ℝ :=
  (subadditive_expSeq h).lim
Uses 3 · Used by 6
Statement usesSubadditive cocycle over a measure-preserving map · Expectation sequence of a cocycle · Expectations of a subadditive cocycle form a subadditive sequence
Used byUpper and lower limits of a nonnegative cocycle agree · Time constant is a lower bound for normalized expectations · Time constant is at most the first expectation · Time constant is at most the integral of the lower limit · Integral of the Kingman limit is at most the time constant · Fekete's lemma for the expectations of a subadditive cocycle

TheoremFekete's lemma for the expectations of a subadditive cocycle#✓fully proved

Fekete's lemma for the expectations: expSeq n / n → gamma when bounded below.

theorem tendsto_expSeq_div (h : SubadditiveCocycle T μ X)
    (hbdd : BddBelow (Set.range fun n => expSeq X μ n / n)) :
    Tendsto (fun n => expSeq X μ n / n) atTop (𝓝 (gamma h))
Uses 4 · Used by 1
Statement usesSubadditive cocycle over a measure-preserving map · Expectation sequence of a cocycle · Time constant of a subadditive cocycle
Proof usesExpectations of a subadditive cocycle form a subadditive sequence
Used byTime constant is at most the integral of the lower limit

TheoremTime constant is a lower bound for normalized expectations#✓fully proved

gamma ≤ expSeq n / n for every n ≠ 0.

theorem gamma_le_div (h : SubadditiveCocycle T μ X)
    (hbdd : BddBelow (Set.range fun n => expSeq X μ n / n)) {n : ℕ} (hn : n ≠ 0) :
    gamma h ≤ expSeq X μ n / n
Uses 4 · Used by 1
Statement usesSubadditive cocycle over a measure-preserving map · Expectation sequence of a cocycle · Time constant of a subadditive cocycle
Proof usesExpectations of a subadditive cocycle form a subadditive sequence
Used byTime constant is at most the first expectation

TheoremTime constant is at most the first expectation#✓fully proved

gamma ≤ ∫ X 1 dμ.

theorem gamma_le_expSeq_one (h : SubadditiveCocycle T μ X)
    (hbdd : BddBelow (Set.range fun n => expSeq X μ n / n)) :
    gamma h ≤ expSeq X μ 1
Uses 4
Statement usesSubadditive cocycle over a measure-preserving map · Expectation sequence of a cocycle · Time constant of a subadditive cocycle
Proof usesTime constant is a lower bound for normalized expectations

TheoremNormalized expectations of a nonnegative cocycle are bounded below#✓fully proved

For a nonnegative cocycle, expSeq n / n is bounded below by 0.

theorem bddBelow_of_nonneg (_h : SubadditiveCocycle T μ X)
    (hnn : ∀ n, 0 ≤ᵐ[μ] X n) :
    BddBelow (Set.range fun n => expSeq X μ n / n)
Uses 2 · Used by 1
Statement usesSubadditive cocycle over a measure-preserving map · Expectation sequence of a cocycle
Used byTime constant is at most the integral of the lower limit

TheoremCocycle inequality holds for all indices almost everywhere#✓fully proved

The cocycle inequality holds for all m, n simultaneously, almost everywhere.

theorem ae_all_subadditive (h : SubadditiveCocycle T μ X) :
    ∀ᵐ x ∂μ, ∀ m n, X (m + n) x ≤ X m x + X n (T^[m] x)
Uses 1 · Used by 3
Statement usesSubadditive cocycle over a measure-preserving map
Used byBlock decomposition bound for a subadditive cocycle · Upper limit of a cocycle bounded by Birkhoff limits of blocks · Time constant is at most the integral of the lower limit

TheoremBlock decomposition bound for a subadditive cocycle#✓fully proved

Block decomposition: X (q k) ≤ ∑_{j<q} X k ∘ T^{j k} almost everywhere.

theorem ae_le_block_birkhoffSum (h : SubadditiveCocycle T μ X) :
    ∀ᵐ x ∂μ, ∀ k q, 1 ≤ q → X (q * k) x ≤ birkhoffSum (T^[k]) (X k) q x
Uses 2 · Used by 1
Statement usesSubadditive cocycle over a measure-preserving map
Proof usesCocycle inequality holds for all indices almost everywhere
Used byUpper limit of a cocycle bounded by Birkhoff limits of blocks

TheoremIntegrable function along an orbit divided by time tends to zero#✓fully proved

For integrable g, g (T^[m] x) / m → 0 almost everywhere.

theorem tendsto_comp_div_atTop (hT : MeasurePreserving T μ μ) {g : α → ℝ}
    (hg : Integrable g μ) :
    ∀ᵐ x ∂μ, Tendsto (fun m : ℕ => g (T^[m] x) / m) atTop (𝓝 0)
Uses 2 · Used by 1
Proof usesBirkhoff limit of a function · Birkhoff averages converge almost everywhere to the Birkhoff limit
Used byUpper limit of a cocycle bounded by Birkhoff limits of blocks

DefinitionDominating function for remainder terms in Kingman's theorem#✓fully proved

The integrable dominating function ∑_{r<k} (X r)⁺ for the remainder terms X r, r < k.

noncomputable def remDom (X : ℕ → α → ℝ) (k : ℕ) (y : α) : ℝ :=
  ∑ r ∈ Finset.range k, (X r y)⁺
Used by 4
Used byUpper limit of a cocycle bounded by Birkhoff limits of blocks · Time constant is at most the integral of the lower limit · Greedy decomposition along an orbit · Windowed greedy bound from time zero

TheoremUpper limit of a cocycle bounded by Birkhoff limits of blocks#✓fully proved

For each k ≥ 1, limsup X n / n ≤ birkhoffLimit (T^[k]) (X k) / k almost everywhere.

theorem gStar_le (h : SubadditiveCocycle T μ X) {k : ℕ} (hk : 1 ≤ k) :
    ∀ᵐ x ∂μ, limsup (fun n => ((X n x / n : ℝ) : EReal)) atTop
      ≤ ((birkhoffLimit (T^[k]) (X k) x / k : ℝ) : EReal)
Uses 7 · Used by 3
Statement usesBirkhoff limit of a function · Subadditive cocycle over a measure-preserving map
Proof usesBirkhoff averages converge almost everywhere to the Birkhoff limit · Cocycle inequality holds for all indices almost everywhere · Block decomposition bound for a subadditive cocycle · Dominating function for remainder terms in Kingman's theorem · Integrable function along an orbit divided by time tends to zero
Used byUpper limit of a normalized cocycle is finite almost everywhere · Integrability of the Kingman limit for nonnegative cocycles · Integral of the Kingman limit is at most the time constant

DefinitionUpper limit of a normalized subadditive cocycle#✓fully proved

The upper limit limsup_n X n x / n in EReal. The map T is a parameter only so that the notation records the cocycle's base map.

@[nolint unusedArguments]
noncomputable def gStar (_T : α → α) (X : ℕ → α → ℝ) (x : α) : EReal :=
  limsup (fun n => ((X n x / n : ℝ) : EReal)) atTop
Used by 11
Used byKingman's subadditive ergodic theorem for nonnegative cocycles · Upper and lower limits of a nonnegative cocycle agree · Upper limit of a normalized cocycle is finite almost everywhere · Time constant is at most the integral of the lower limit · Integrability of the Kingman limit for nonnegative cocycles · Integral of the Kingman limit is at most the time constant · Kingman's subadditive ergodic theorem · Kingman limit of a subadditive cocycle · Invariance of the Kingman limit · Almost-everywhere convergence to the Kingman limit · Kingman's subadditive ergodic theorem

DefinitionLower limit of a normalized subadditive cocycle#✓fully proved

The lower limit liminf_n X n x / n in EReal.

@[nolint unusedArguments]
noncomputable def gStarLow (_T : α → α) (X : ℕ → α → ℝ) (x : α) : EReal :=
  liminf (fun n => ((X n x / n : ℝ) : EReal)) atTop
Used by 6
Used byReal lower limit of a normalized cocycle · Upper and lower limits of a nonnegative cocycle agree · Lower limit of a cocycle is nondecreasing along the map · Time constant is at most the integral of the lower limit · Invariance of the Kingman limit · Almost-everywhere convergence to the Kingman limit

TheoremUpper limit of a normalized cocycle is finite almost everywhere#✓fully proved

limsup X n / n < ⊤ almost everywhere.

theorem gStar_lt_top_ae (h : SubadditiveCocycle T μ X) : ∀ᵐ x ∂μ, gStar T X x < ⊤
Uses 4 · Used by 3
Statement usesSubadditive cocycle over a measure-preserving map · Upper limit of a normalized subadditive cocycle
Proof usesBirkhoff limit of a function · Upper limit of a cocycle bounded by Birkhoff limits of blocks
Used byUpper and lower limits of a nonnegative cocycle agree · Time constant is at most the integral of the lower limit · Almost-everywhere convergence to the Kingman limit

DefinitionKingman limit of a subadditive cocycle#✓fully proved

The limit lim X n / n in Kingman's theorem, defined as limsup X n / n cast to ℝ (so it is 0 where the limsup is infinite).

noncomputable def kingmanLimit (T : α → α) (X : ℕ → α → ℝ) (x : α) : ℝ := (gStar T X x).toReal
Uses 1 · Used by 10
Statement usesUpper limit of a normalized subadditive cocycle
Used byKingman's theorem: normalized cocycle converges almost everywhere · Kingman's subadditive ergodic theorem for nonnegative cocycles · Upper and lower limits of a nonnegative cocycle agree · Time constant is at most the integral of the lower limit · Integrability of the Kingman limit for nonnegative cocycles · Integral of the Kingman limit is at most the time constant · Kingman's subadditive ergodic theorem · Invariance of the Kingman limit · Almost-everywhere convergence to the Kingman limit · Kingman's subadditive ergodic theorem

TheoremAlmost-everywhere convergence to the Kingman limit#✓fully proved

If g* ≤ g_* and g* > ⊥ almost everywhere, then X n / n → kingmanLimit almost everywhere.

theorem tendsto_div_kingmanLimit_ae (h : SubadditiveCocycle T μ X)
    (heq : ∀ᵐ x ∂μ, gStar T X x ≤ gStarLow T X x)
    (hbot : ∀ᵐ x ∂μ, ⊥ < gStar T X x) :
    ∀ᵐ x ∂μ, Tendsto (fun n => X n x / n) atTop (𝓝 (kingmanLimit T X x))
Uses 5 · Used by 2
Statement usesSubadditive cocycle over a measure-preserving map · Upper limit of a normalized subadditive cocycle · Lower limit of a normalized subadditive cocycle · Kingman limit of a subadditive cocycle
Proof usesUpper limit of a normalized cocycle is finite almost everywhere
Used byInvariance of the Kingman limit · Kingman's subadditive ergodic theorem

TheoremInvariance of the Kingman limit#✓fully proved

Under the hypotheses of tendsto_div_kingmanLimit_ae and integrability of the limit, the limit is T-invariant almost everywhere.

theorem kingmanLimit_comp_ae (h : SubadditiveCocycle T μ X)
    (heq : ∀ᵐ x ∂μ, gStar T X x ≤ gStarLow T X x)
    (hbot : ∀ᵐ x ∂μ, ⊥ < gStar T X x)
    (hint : Integrable (kingmanLimit T X) μ) :
    ∀ᵐ x ∂μ, kingmanLimit T X (T x) = kingmanLimit T X x
Uses 6 · Used by 1
Statement usesSubadditive cocycle over a measure-preserving map · Upper limit of a normalized subadditive cocycle · Lower limit of a normalized subadditive cocycle · Kingman limit of a subadditive cocycle
Proof usesIntegral is invariant under a measure-preserving map · Almost-everywhere convergence to the Kingman limit
Used byKingman's subadditive ergodic theorem for nonnegative cocycles

TheoremIntegrability of the Kingman limit for nonnegative cocycles#✓fully proved

For a nonnegative cocycle, kingmanLimit is integrable.

theorem integrable_kingmanLimit (h : SubadditiveCocycle T μ X) (hnn : ∀ n, 0 ≤ᵐ[μ] X n) :
    Integrable (kingmanLimit T X) μ
Uses 6 · Used by 4
Statement usesSubadditive cocycle over a measure-preserving map · Kingman limit of a subadditive cocycle
Proof usesBirkhoff limit of a function · Integrability of the Birkhoff limit · Upper limit of a normalized subadditive cocycle · Upper limit of a cocycle bounded by Birkhoff limits of blocks
Used byKingman's subadditive ergodic theorem for nonnegative cocycles · Upper and lower limits of a nonnegative cocycle agree · Time constant is at most the integral of the lower limit · Integral of the Kingman limit is at most the time constant

TheoremIntegral of the Kingman limit is at most the time constant#✓fully proved

For a nonnegative cocycle, ∫ kingmanLimit ≤ gamma.

theorem integral_kingmanLimit_le_gamma (h : SubadditiveCocycle T μ X) (hnn : ∀ n, 0 ≤ᵐ[μ] X n) :
    (∫ x, kingmanLimit T X x ∂μ) ≤ SubadditiveCocycle.gamma h
Uses 12 · Used by 1
Statement usesSubadditive cocycle over a measure-preserving map · Time constant of a subadditive cocycle · Kingman limit of a subadditive cocycle
Proof usesInvariant set of a map · Birkhoff limit of a function · Integrability of the Birkhoff limit · Birkhoff limit preserves integrals over invariant sets · Expectation sequence of a cocycle · Expectations of a subadditive cocycle form a subadditive sequence · Upper limit of a normalized subadditive cocycle · Upper limit of a cocycle bounded by Birkhoff limits of blocks · Integrability of the Kingman limit for nonnegative cocycles
Used byUpper and lower limits of a nonnegative cocycle agree

DefinitionReal lower limit of a normalized cocycle#✓fully proved

The lower limit liminf_n X n x / n, cast to ℝ.

noncomputable def gLow (T : α → α) (X : ℕ → α → ℝ) (x : α) : ℝ := (gStarLow T X x).toReal
Uses 1 · Used by 6
Statement usesLower limit of a normalized subadditive cocycle
Used byBad set in the greedy decomposition for Kingman's theorem · Per-step budget of the greedy decomposition · Upper and lower limits of a nonnegative cocycle agree · Time constant is at most the integral of the lower limit · Greedy decomposition along an orbit · Windowed greedy bound from time zero

TheoremOrdered extended reals with equal real parts are equal#✓fully proved

Two extended reals x ≤ y with x ≠ ⊥, y ≠ ⊤ and equal real parts are equal.

theorem eq_of_le_toReal_eq {x y : EReal} (hle : x ≤ y) (hxbot : x ≠ ⊥) (hytop : y ≠ ⊤)
    (heq : x.toReal = y.toReal) : x = y
Used by 1
Used byUpper and lower limits of a nonnegative cocycle agree

TheoremLower limit of a cocycle is nondecreasing along the map#✓fully proved

The lower limit is nondecreasing along T: g_* ≤ g_* ∘ T almost everywhere.

theorem gStarLow_le_comp (h : SubadditiveCocycle T μ X) :
    ∀ᵐ x ∂μ, gStarLow T X x ≤ gStarLow T X (T x)
Uses 2 · Used by 1
Statement usesSubadditive cocycle over a measure-preserving map · Lower limit of a normalized subadditive cocycle
Used byTime constant is at most the integral of the lower limit

DefinitionBad set in the greedy decomposition for Kingman's theorem#✓fully proved

The bad set: points where X m x > (gLow x + ε) m for every block length 1 ≤ m ≤ N.

def badSet (T : α → α) (X : ℕ → α → ℝ) (ε : ℝ) (N : ℕ) : Set α :=
  {x | ∀ m, 1 ≤ m → m ≤ N → (gLow T X x + ε) * m < X m x}
Uses 1 · Used by 4
Statement usesReal lower limit of a normalized cocycle
Used byCost of a bad step in the greedy decomposition · Per-step budget of the greedy decomposition · Time constant is at most the integral of the lower limit · Greedy decomposition along an orbit

DefinitionPer-step budget of the greedy decomposition#✓fully proved

The per-step budget gLow + ε + 1_{badSet} X 1 of the greedy decomposition.

noncomputable def dep (T : α → α) (X : ℕ → α → ℝ) (ε : ℝ) (N : ℕ) (y : α) : ℝ :=
  gLow T X y + ε + (badSet T X ε N).indicator (fun z => X 1 z) y
Uses 2 · Used by 3
Statement usesBad set in the greedy decomposition for Kingman's theorem · Real lower limit of a normalized cocycle
Used byTime constant is at most the integral of the lower limit · Greedy decomposition along an orbit · Windowed greedy bound from time zero

DefinitionCost of a bad step in the greedy decomposition#✓fully proved

The cost 1_{badSet} X 1 of a bad step.

noncomputable def badCost (T : α → α) (X : ℕ → α → ℝ) (ε : ℝ) (N : ℕ) (x : α) : ℝ :=
  (badSet T X ε N).indicator (fun z => X 1 z) x
Uses 1 · Used by 1
Statement usesBad set in the greedy decomposition for Kingman's theorem
Used byTime constant is at most the integral of the lower limit

TheoremGreedy decomposition along an orbit#✓fully proved

Greedy decomposition along one orbit: X n (T^[s] x) is at most the sum of the budgets dep over n steps plus one remainder term, for every n and starting time s.

theorem greedy (ε : ℝ) (N : ℕ) (hN : 1 ≤ N) (x : α)
    (hsub : ∀ s a b, X (a + b) (T^[s] x) ≤ X a (T^[s] x) + X b (T^[a + s] x))
    (hmono : ∀ i j, i ≤ j → gLow T X (T^[i] x) ≤ gLow T X (T^[j] x))
    (hgnn : ∀ i, 0 ≤ gLow T X (T^[i] x))
    (hx1nn : ∀ i, 0 ≤ X 1 (T^[i] x))
    (hεnn : 0 ≤ ε)
    (hrem : ∀ i n, n < N → X n (T^[i] x) ≤ remDom X N (T^[i] x)) :
    ∀ n s, ∃ m, m ≤ n ∧ n ≤ m + N ∧
      X n (T^[s] x) ≤ (∑ j ∈ Finset.range n, dep T X ε N (T^[s + j] x))
        + remDom X N (T^[s + m] x)
Uses 4 · Used by 1
Statement usesDominating function for remainder terms in Kingman's theorem · Per-step budget of the greedy decomposition · Real lower limit of a normalized cocycle
Proof usesBad set in the greedy decomposition for Kingman's theorem
Used byWindowed greedy bound from time zero

TheoremWindowed greedy bound from time zero#✓fully proved

The greedy bound from time 0, with the remainder bounded by a sum over the last window.

theorem greedy_windowed (ε : ℝ) (N : ℕ) (hN : 1 ≤ N) (x : α)
    (hsub : ∀ s a b, X (a + b) (T^[s] x) ≤ X a (T^[s] x) + X b (T^[a + s] x))
    (hmono : ∀ i j, i ≤ j → gLow T X (T^[i] x) ≤ gLow T X (T^[j] x))
    (hgnn : ∀ i, 0 ≤ gLow T X (T^[i] x))
    (hx1nn : ∀ i, 0 ≤ X 1 (T^[i] x))
    (hεnn : 0 ≤ ε)
    (hremnn : ∀ t, 0 ≤ remDom X N (T^[t] x)) (n : ℕ) :
    X n x ≤ (∑ j ∈ Finset.range n, dep T X ε N (T^[j] x))
      + ∑ t ∈ Finset.Icc (n-N) n, remDom X N (T^[t] x)
Uses 4 · Used by 1
Statement usesDominating function for remainder terms in Kingman's theorem · Per-step budget of the greedy decomposition · Real lower limit of a normalized cocycle
Proof usesGreedy decomposition along an orbit
Used byTime constant is at most the integral of the lower limit

TheoremTime constant is at most the integral of the lower limit#✓fully proved

The time constant is at most ∫ g_*.

theorem gamma_le_integral_gLow (h : SubadditiveCocycle T μ X) (hnn : ∀ n, 0 ≤ᵐ[μ] X n) :
    h.gamma ≤ ∫ x, gLow T X x ∂μ
Uses 19 · Used by 1
Statement usesSubadditive cocycle over a measure-preserving map · Time constant of a subadditive cocycle · Real lower limit of a normalized cocycle
Proof usesNormalized expectations of a nonnegative cocycle are bounded below · Expectation sequence of a cocycle · Fekete's lemma for the expectations of a subadditive cocycle · Integral is invariant under iterates of a measure-preserving map · Cocycle inequality holds for all indices almost everywhere · Upper limit of a normalized subadditive cocycle · Lower limit of a normalized subadditive cocycle · Upper limit of a normalized cocycle is finite almost everywhere · Integrability of the Kingman limit for nonnegative cocycles · Kingman limit of a subadditive cocycle · Dominating function for remainder terms in Kingman's theorem · Cost of a bad step in the greedy decomposition · Bad set in the greedy decomposition for Kingman's theorem · Per-step budget of the greedy decomposition · Lower limit of a cocycle is nondecreasing along the map · Windowed greedy bound from time zero
Used byUpper and lower limits of a nonnegative cocycle agree

TheoremUpper and lower limits of a nonnegative cocycle agree#✓fully proved

For a nonnegative cocycle the upper and lower limits of X n / n agree almost everywhere.

theorem gStar_le_gStarLow_ae (h : SubadditiveCocycle T μ X) (hnn : ∀ n, 0 ≤ᵐ[μ] X n) :
    ∀ᵐ x ∂μ, gStar T X x ≤ gStarLow T X x
Uses 11 · Used by 2
Statement usesSubadditive cocycle over a measure-preserving map · Upper limit of a normalized subadditive cocycle · Lower limit of a normalized subadditive cocycle
Proof usesTime constant of a subadditive cocycle · Upper limit of a normalized cocycle is finite almost everywhere · Integrability of the Kingman limit for nonnegative cocycles · Integral of the Kingman limit is at most the time constant · Kingman limit of a subadditive cocycle · Ordered extended reals with equal real parts are equal · Real lower limit of a normalized cocycle · Time constant is at most the integral of the lower limit
Used byKingman's subadditive ergodic theorem for nonnegative cocycles · Kingman's subadditive ergodic theorem

TheoremKingman's subadditive ergodic theorem#✓fully proved

Kingman's subadditive ergodic theorem for nonnegative cocycles: X n / n converges almost everywhere to kingmanLimit T X (J. F. C. Kingman, 1968; proof of J. M. Steele, 1989).

theorem tendsto_div_kingmanLimit_ae_of_nonneg (h : SubadditiveCocycle T μ X)
    (hnn : ∀ n, 0 ≤ᵐ[μ] X n) :
    ∀ᵐ x ∂μ, Tendsto (fun n => X n x / n) atTop (𝓝 (kingmanLimit T X x))
Uses 5 · Used by 2
Statement usesSubadditive cocycle over a measure-preserving map · Kingman limit of a subadditive cocycle
Proof usesUpper limit of a normalized subadditive cocycle · Almost-everywhere convergence to the Kingman limit · Upper and lower limits of a nonnegative cocycle agree
Used byKingman's theorem: normalized cocycle converges almost everywhere · Kingman's subadditive ergodic theorem for nonnegative cocycles

DefinitionAdditive cocycle of Birkhoff sums of the first term#✓fully proved

The additive cocycle n ↦ ∑_{k<n} X 1 ∘ T^[k] (the Birkhoff sums of X 1).

noncomputable def addCoc (T : α → α) (X : ℕ → α → ℝ) (n : ℕ) (x : α) : ℝ :=
  birkhoffSum T (X 1) n x
Used by 7
Used byLower limit of the normalized defect is finite almost everywhere · Kingman's theorem: normalized cocycle converges almost everywhere · Shifted subadditivity defect of a cocycle · Truncated defect is a nonnegative subadditive cocycle · Negative subadditivity defect of a cocycle · Negative defect is a subadditive cocycle · Subadditivity defect of a cocycle

DefinitionSubadditivity defect of a cocycle#✓fully proved

The subadditivity defect addCoc n - X n (0 at n = 0); it is nonnegative a.e.

noncomputable def Zc (T : α → α) (X : ℕ → α → ℝ) (n : ℕ) (x : α) : ℝ :=
  if n = 0 then 0 else addCoc T X n x - X n x
Uses 1 · Used by 2
Statement usesAdditive cocycle of Birkhoff sums of the first term
Used byLower limit of the normalized defect is finite almost everywhere · Kingman's theorem: normalized cocycle converges almost everywhere

DefinitionNegative subadditivity defect of a cocycle#✓fully proved

The negative defect X n - addCoc n (0 at n = 0), a nonpositive subadditive cocycle.

noncomputable def Wc (T : α → α) (X : ℕ → α → ℝ) (n : ℕ) (x : α) : ℝ :=
  if n = 0 then 0 else X n x - addCoc T X n x
Uses 1 · Used by 2
Statement usesAdditive cocycle of Birkhoff sums of the first term
Used byLower limit of the normalized defect is finite almost everywhere · Negative defect is a subadditive cocycle

TheoremNegative defect is a subadditive cocycle#✓fully proved

The negative defect is a subadditive cocycle.

theorem Wc_subaddCocycle (h : SubadditiveCocycle T μ X) : SubadditiveCocycle T μ (Wc T X)
Uses 4
Statement usesSubadditive cocycle over a measure-preserving map · Negative subadditivity defect of a cocycle
Proof usesIntegrability of Birkhoff sums · Additive cocycle of Birkhoff sums of the first term

DefinitionShifted subadditivity defect of a cocycle#✓fully proved

The shifted defect X n + M n - addCoc n, a subadditive cocycle for every M.

noncomputable def Sc (T : α → α) (X : ℕ → α → ℝ) (M : ℝ) (n : ℕ) (x : α) : ℝ :=
  X n x + (M * n - addCoc T X n x)
Uses 1 · Used by 3
Statement usesAdditive cocycle of Birkhoff sums of the first term
Used byKingman's theorem: normalized cocycle converges almost everywhere · Truncated subadditivity defect of a cocycle · Truncated defect is a nonnegative subadditive cocycle

DefinitionTruncated subadditivity defect of a cocycle#✓fully proved

The truncated defect (Sc M n)⁺ = (M n - Zc n)⁺, a nonnegative subadditive cocycle.

noncomputable def Vc (T : α → α) (X : ℕ → α → ℝ) (M : ℝ) (n : ℕ) (x : α) : ℝ :=
  (Sc T X M n x)⁺
Uses 1 · Used by 2
Statement usesShifted subadditivity defect of a cocycle
Used byKingman's theorem: normalized cocycle converges almost everywhere · Truncated defect is a nonnegative subadditive cocycle

TheoremTruncated defect is a nonnegative subadditive cocycle#✓fully proved

The truncated defect is a nonnegative subadditive cocycle.

theorem Vc_subaddCocycle (h : SubadditiveCocycle T μ X) (M : ℝ) :
    SubadditiveCocycle T μ (Vc T X M)
Uses 5 · Used by 1
Statement usesSubadditive cocycle over a measure-preserving map · Truncated subadditivity defect of a cocycle
Proof usesIntegrability of Birkhoff sums · Shifted subadditivity defect of a cocycle · Additive cocycle of Birkhoff sums of the first term
Used byKingman's theorem: normalized cocycle converges almost everywhere

TheoremLower limit of the normalized defect is finite almost everywhere#✓fully proved

If the time constant is finite, liminf_n Zc n / n < ∞ almost everywhere (Fatou).

theorem ae_liminf_lt_top (h : SubadditiveCocycle T μ X)
    (hbdd : BddBelow (Set.range fun n => SubadditiveCocycle.expSeq X μ n / n)) :
    ∀ᵐ x ∂μ, liminf (fun n => ENNReal.ofReal (Zc T X n x / n)) atTop < ∞
Uses 8 · Used by 1
Statement usesSubadditive cocycle over a measure-preserving map · Expectation sequence of a cocycle · Subadditivity defect of a cocycle
Proof usesIntegrability of Birkhoff sums · Subadditive cocycle bounded by Birkhoff sums of its first term · Integral is invariant under iterates of a measure-preserving map · Negative subadditivity defect of a cocycle · Additive cocycle of Birkhoff sums of the first term
Used byKingman's theorem: normalized cocycle converges almost everywhere

TheoremKingman's theorem: normalized cocycle converges almost everywhere#✓fully proved

If the time constant is finite, X n / n converges almost everywhere.

theorem ae_tendsto_X_div (h : SubadditiveCocycle T μ X)
    (hbdd : BddBelow (Set.range fun n => SubadditiveCocycle.expSeq X μ n / n)) :
    ∀ᵐ x ∂μ, ∃ L : ℝ, Tendsto (fun n => X n x / n) atTop (𝓝 L)
Uses 12 · Used by 1
Statement usesSubadditive cocycle over a measure-preserving map · Expectation sequence of a cocycle
Proof usesBirkhoff limit of a function · Birkhoff averages converge almost everywhere to the Birkhoff limit · Kingman limit of a subadditive cocycle · Kingman's subadditive ergodic theorem · Shifted subadditivity defect of a cocycle · Truncated subadditivity defect of a cocycle · Truncated defect is a nonnegative subadditive cocycle · Subadditivity defect of a cocycle · Additive cocycle of Birkhoff sums of the first term · Lower limit of the normalized defect is finite almost everywhere
Used byKingman's subadditive ergodic theorem

TheoremKingman's subadditive ergodic theorem#✓fully proved

Kingman's subadditive ergodic theorem (J. F. C. Kingman, The ergodic theory of subadditive stochastic processes, 1968): if X is a subadditive cocycle over a map T preserving the finite measure μ and inf_n (∫ X n dμ) / n > -∞, then X n / n converges μ-almost everywhere to the finite limit kingmanLimit T X. The sign of X is arbitrary. Invariance and integrability of the limit, and ∫ kingmanLimit = gamma, are not stated here; for nonnegative cocycles see exists_invariant_limit_of_nonneg, which contains MathlibExt.Dynamics.Ergodic.KingmanWanted.kingman_subadditive.

theorem kingman_ae_general (h : SubadditiveCocycle T μ X)
    (hbdd : BddBelow (Set.range fun n => SubadditiveCocycle.expSeq X μ n / n)) :
    ∀ᵐ x ∂μ, Tendsto (fun n => X n x / n) atTop (𝓝 (kingmanLimit T X x))
Uses 5
Statement usesSubadditive cocycle over a measure-preserving map · Expectation sequence of a cocycle · Kingman limit of a subadditive cocycle
Proof usesUpper limit of a normalized subadditive cocycle · Kingman's theorem: normalized cocycle converges almost everywhere

TheoremKingman's subadditive ergodic theorem for nonnegative cocycles#✓fully proved

Kingman's theorem for nonnegative cocycles, with integrable and invariant limit: if T preserves the finite measure μ and X is a nonnegative integrable subadditive cocycle, then X n / n converges a.e. to an integrable T-invariant function. This is MathlibExt.Dynamics.Ergodic.KingmanWanted.kingman_subadditive without its hypotheses that each X n is measurable and X 0 = 0, and for finite rather than probability measures.

theorem exists_invariant_limit_of_nonneg (hT : MeasurePreserving T μ μ)
    (hX_int : ∀ n, Integrable (X n) μ) (hX_nonneg : ∀ n, ∀ᵐ x ∂μ, 0 ≤ X n x)
    (hX_subadd : ∀ m n, ∀ᵐ x ∂μ, X (m + n) x ≤ X m x + X n (T^[m] x)) :
    ∃ g : α → ℝ, Integrable g μ ∧ (∀ᵐ x ∂μ, g (T x) = g x) ∧
      ∀ᵐ x ∂μ, Tendsto (fun n : ℕ => X n x / (n : ℝ)) atTop (𝓝 (g x))
Uses 7
Proof usesSubadditive cocycle over a measure-preserving map · Upper limit of a normalized subadditive cocycle · Integrability of the Kingman limit for nonnegative cocycles · Kingman limit of a subadditive cocycle · Invariance of the Kingman limit · Upper and lower limits of a nonnegative cocycle agree · Kingman's subadditive ergodic theorem
49 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.