InformationTheory

InformationTheory.Shannon.LZ78.PhraseCountAsymptotics

source

Imports 9

LZ78 phrase-count asymptotic envelope (IsBigO bound) #

This file discharges the predicate IsLZ78PhraseCountAsymptotic p B (published in InformationTheory/Shannon/LZ78/ConverseAsymptotic.lean) with real-analysis content rather than a hypothesis pass-through.

The target predicate unfolds to (fun n => ((p n).count : ℝ)) =O[atTop] (fun n => (n : ℝ) / Real.log n), i.e. the Cover–Thomas statement c(n) = O(n / log n).

Approach #

The substantive ingredient is the inversion of the Ziv counting inequality. Cover–Thomas gives, for an LZ78 parsing of a length-n string over a b-symbol alphabet, the primitive bound

c(n) · log c(n) ≤ K · n          (K = log b, large n)        (★)

We take (★) as the more-primitive hypothesis and prove the real-analysis lemma

(★) + (c n → handled pointwise)  ⟹  c(n) = O(n / log n).

The proof is a two-case argument at the threshold √n = n^(1/2):

  • Large branch c(n) > √n: then log c(n) > ½ log n, so (★) gives c(n) · ½ log n < K n, hence c(n) · log n ≤ 2K n.
  • Small branch c(n) ≤ √n: then c(n) · log n ≤ √n · log n, and log n ≤ 2√n (Real.log_natCast_le_rpow_div with ε = ½), so c(n) · log n ≤ √n · 2√n = 2n.

In both branches c(n) · log n ≤ C · n with C = max (2K) 2, which — since log n > 0 eventually — is exactly c(n) ≤ C · (n / log n), i.e. the IsBigO bound with constant C.

Layering #

§1. Threshold algebra (√n = n^(1/2)) #

theorem

InformationTheory.Shannon.rpow_half_mul_self

source
(x : ℝ) (hx : 0 ≤ x) :
x ^ (1 / 2) * x ^ (1 / 2) = x

√x · √x = x for 0 ≤ x, with √x := x ^ (1/2 : ℝ).

Used by
    theorem

    InformationTheory.Shannon.log_rpow_half

    source
    (x : ℝ) (hx : 0 < x) :
    Real.log (x ^ (1 / 2)) = 1 / 2 * Real.log x

    log (x ^ (1/2)) = (1/2) · log x for 0 < x.

    Used by
      theorem

      InformationTheory.Shannon.log_natCast_le_two_mul_rpow_half

      source
      (n : ℕ) :
      Real.log ↑n ≤ 2 * ↑n ^ (1 / 2)

      The square-root envelope of log: log n ≤ 2 · n^(1/2).

      Used by
        theorem

        InformationTheory.Shannon.rpow_half_nonneg

        source
        (n : ℕ) :
        0 ≤ ↑n ^ (1 / 2)

        0 ≤ n^(1/2).

        Used by

          §2. The inversion lemma #

          theorem

          InformationTheory.Shannon.isBigO_natCast_div_log_of_mul_log_le

          source
          {f : ℕ → ℝ} {K : ℝ} (h_nonneg : ∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ f n) (h_mul_log : ∀ᶠ (n : ℕ) in Filter.atTop, f n * Real.log (f n) ≤ K * ↑n) :
          f =O[Filter.atTop] fun (n : ℕ) => ↑n / Real.log ↑n

          From the primitive Cover–Thomas c(n) · log c(n) ≤ K · n bound, the count c(n) is O(n / log n).

          f : ℕ → ℝ is the (nonnegative, real-valued) count sequence. The hypotheses are all eventual: f n ≥ 0 and the primitive product bound. The IsBigO constant is max (2K) 2, so the result holds for any real K (the negative-K case is vacuously stronger).

          Used by

            §3. The primitive predicate IsZivCountingMulLogBound and discharge #

            def

            InformationTheory.Shannon.IsZivCountingMulLogBound

            source
            {α : Type u_1} (p : ℕ → LZ78Parsing α) (K : ℝ) :
            Prop

            The primitive Ziv c·log c product predicate.

            For a family of parsings p : ℕ → LZ78Parsing α and constant K : ℝ, this asserts the Cover–Thomas primitive bound (★): eventually c(n) · log c(n) ≤ K · n. This is strictly more primitive than IsLZ78PhraseCountAsymptotic — the latter is derived from it by the inversion lemma of §2.

            Equations
            Instances For
              Used by
                theorem

                InformationTheory.Shannon.IsLZ78PhraseCountAsymptotic.of_mul_log_bound

                source
                {α : Type u_1} {p : ℕ → LZ78Parsing α} {K : ℝ} (_hK : 0 ≤ K) (h : IsZivCountingMulLogBound p K) :
                IsLZ78PhraseCountAsymptotic p fun (n : ℕ) => ↑n / Real.log ↑n

                Discharge of IsLZ78PhraseCountAsymptotic from the primitive c·log c ≤ Kn product bound: the asymptotic envelope predicate holds with IsBigO content.

                Used by

                  §4. Re-published wrappers #

                  theorem

                  InformationTheory.Shannon.lz78_phrase_count_asymptotic_of_mul_log

                  source
                  {α : Type u_1} (p : ℕ → LZ78Parsing α) {K : ℝ} (hK : 0 ≤ K) (h : IsZivCountingMulLogBound p K) :
                  IsLZ78PhraseCountAsymptotic p fun (n : ℕ) => ↑n / Real.log ↑n

                  The re-published main statement: the LZ78 phrase-count is O(n / log n) whenever the primitive product bound holds. Mirrors the shape of lz78_phrase_count_asymptotic_n_div_log but with the IsBigO content supplied (no eventual-≤ hypothesis needed).

                  Used by
                    theorem

                    InformationTheory.Shannon.IsLZ78PhraseCountSandwich.of_mul_log_bound

                    source
                    {α : Type u_1} (p : ℕ → LZ78Parsing α) {K : ℝ} (hK : 0 ≤ K) (h : IsZivCountingMulLogBound p K) :
                    IsLZ78PhraseCountSandwich p (fun (n : ℕ) => ↑(p n).count) fun (n : ℕ) => ↑n / Real.log ↑n

                    Combine the upper envelope with the reflexive lower envelope into a phrase-count sandwich.

                    Used by