RootInformationGrowth.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Linear growth of actual root information

Small-ball differentiation bounds the information along integer scales. The actual scaling cocycle identifies these scales with Birkhoff sums.

lemma OAI.DukePrimeDegree.ae_rootInformation_nat_sum line 27

Source documentation

The information at integer time is the corresponding finite orbit sum.

lemma ae_rootInformation_nat_sum (n : ℕ) :
    ∀ᵐ x ∂μ, rootInformation hij μ n x =
      birkhoffSum (fun y => rightAction y (rootCanonicalFlow d j 1))
        (rootInformation hij μ 1) n x := by
…

lemma OAI.DukePrimeDegree.ae_rootInformation_linear_bound line 52
Source documentation
Root information grows at most linearly, with slope one and a point-dependent additive constant.
```
lemma ae_rootInformation_linear_bound :
    ∀ᵐ x ∂μ, ∃ B : ℝ, ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
      rootInformation hij μ n x ≤ n + B := by
…
```