CountableBoundaryEntropy.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

A countable boundary label has sublinear information cost

Finite clipping controls the information in a single countable label, even when that label has infinite Shannon entropy. The clipping error depends only on its tail probability and the alphabet of the observed word, rather than on the entropy of the countable label.

theorem OAI.DukePrimeDegree.heightClip_sigma_monotone line 22
theorem OAI.DukePrimeDegree.heightClip_sigma_generate line 36
theorem OAI.DukePrimeDegree.conditional_heightClip_tendsto line 64
theorem OAI.DukePrimeDegree.conditional_heightClip_le_larger line 76

theorem OAI.DukePrimeDegree.conditional_heightClip_le_countable line 135

Source documentation

Removing a finite clipping of the conditioning label changes entropy only on the clipped tail.

theorem conditional_heightClip_le_countable {Y α : Type*}
    [MeasurableSpace Y] [Fintype α]
    (μ : Measure Y) [IsProbabilityMeasure μ]
    (P : Y → α) (hP : ∀ a, MeasurableSet {y | P y=a})
    (Q : Y → ℕ) (hQ : Measurable Q) (L : ℕ) :
    conditionalObservationEntropy μ P (heightClip Q L) ≤
      conditionalSigmaEntropy μ P (MeasurableSpace.comap Q inferInstance) +
        μ.real {y | L ≤ Q y} * Real.log (Fintype.card α) := by
…

Mentions: OAI.DukePrimeDegree.heightClip

theorem OAI.DukePrimeDegree.observationEntropy_le_countable_conditioning line 147
theorem OAI.DukePrimeDegree.conditional_countable_le_observationEntropy line 165
theorem OAI.DukePrimeDegree.countable_tail_measureReal_tendsto_zero line 177

theorem OAI.DukePrimeDegree.countable_boundary_information_sublinear line 197

Source documentation

A single countable observation at the end of an orbit word carries sublinear information about that word. Its Shannon entropy may be infinite.

theorem countable_boundary_information_sublinear {Y α : Type*}
    [MeasurableSpace Y] [Fintype α]
    (μ : Measure Y) [IsProbabilityMeasure μ]
    {T : Y → Y} (hT : MeasurePreserving T μ μ)
    (P : Y → α) (hP : ∀ a, MeasurableSet {y | P y=a})
    (Q : Y → ℕ) (hQ : Measurable Q) :
    Tendsto (fun N : ℕ =>
      (observationEntropy μ (orbitName T P N) -
        conditionalSigmaEntropy μ (orbitName T P N)
          (MeasurableSpace.comap (Q ∘ T^[N]) inferInstance)) / N)
      atTop (𝓝 0) := by
…

theorem OAI.DukePrimeDegree.conditional_boundary_entropy_rate line 252