FiniteLevelFutureLifts.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Future observations finite on each compact height range

Compact height levels provide finite chart covers. Encoding their level and chart labels gives one countable observation with controlled future lifts, while its restriction to every bounded height range is finite. No finite Shannon entropy of the countable observation is asserted.

theorem OAI.DukePrimeDegree.exists_finite_level_triangular_observation line 21

theorem OAI.DukePrimeDegree.exists_tempered_finite_level_observation line 128

Source documentation

A countable geometric observation whose compact levels are finite and whose level height grows sublinearly along almost every diagonal orbit.

theorem exists_tempered_finite_level_observation (d : ℕ)
    (μ : Measure (X (d+1))) [IsFiniteMeasure μ]
    (hA : ∀ u : LogCoordinates d, μ.map (fun x => rightAction x (diagonalFlow u))=μ)
    (ell : Fin (d+1) → ℝ) (hell : ∑ i, ell i=0) :
    ∃ (H Q : X (d+1) → ℕ), Measurable H ∧ Measurable Q ∧
      (∀ m, IsCompact {x | H x ≤ m}) ∧
      (∀ m, (Q '' {x | H x ≤ m}).Finite) ∧
      (∀ᵐ x ∂μ, Tendsto (fun k : ℕ =>
        (H ((fun z => rightAction z (diagonalOneParameter ell hell (-1)))^[k] x) : ℝ)/
          (k:ℝ)) atTop (𝓝 0)) ∧
      ∀ x y, (∀ k : ℕ,
          Q ((fun z => rightAction z (diagonalOneParameter ell hell (-1)))^[k] y) =
…

Mentions: OAI.DukePrimeDegree.diagonalFlow