InformationTheory

InformationTheory.Asymptotic

source

Imports 8

Asymptotic / exponent framework #

The exponent-equality relation \doteq of Cover–Thomas and a closed-form rate-extraction wrapper, forming the asymptotic / rate API layer.

Notation #

  • a ≐ b (DotEq a b): (Real.log ∘ a − Real.log ∘ b) =o[atTop] (·:ℝ).
  • The textbook f(n) = o(n) is f =o[atTop] (fun n : ℕ => (n : ℝ)).
  • The textbook f(n) = o(1) is f =o[atTop] (fun _ => (1 : ℝ)).

Main definitions #

  • DotEq — exponent equality, defined directly as an IsLittleO.

Main statements #

Implementation notes #

  • DotEq is ℝ-valued; no ℝ≥0∞ alias is published here.
  • The notation ≐ is scoped[InformationTheory.Asymptotic], so only call sites that open InformationTheory.Asymptotic see it.
  • Positivity is not built into the predicate (Mathlib's Real.log returns 0 for x ≤ 0, so DotEq is well-defined for any ℕ → ℝ); it is required at the bridge / mul / inv use sites instead.
def

InformationTheory.Asymptotic.DotEq

source
(a b : ℕ → ℝ) :
Prop

Exponent equality (the textbook \doteq): a ≐ b when Real.log (a n) − Real.log (b n) = o(n) along atTop.

Under positivity 0 < a n ∧ 0 < b n this is equivalent to (1/n) · log (a n / b n) → 0 (dotEq_iff_tendsto_log_div). Positivity is required at the use site rather than in the predicate.

Equations
Instances For
    Used by
      def

      InformationTheory.Asymptotic.«term_≐_»

      source
      :
      Lean.TrailingParserDescr

      Exponent equality (the textbook \doteq): a ≐ b when Real.log (a n) − Real.log (b n) = o(n) along atTop.

      Under positivity 0 < a n ∧ 0 < b n this is equivalent to (1/n) · log (a n / b n) → 0 (dotEq_iff_tendsto_log_div). Positivity is required at the use site rather than in the predicate.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Used by
          theorem

          InformationTheory.Asymptotic.DotEq.refl

          source
          (a : ℕ → ℝ) :
          DotEq a a

          DotEq is reflexive: Real.log (a n) - Real.log (a n) = 0 = o(n).

          Used by
            theorem

            InformationTheory.Asymptotic.DotEq.symm

            source
            {a b : ℕ → ℝ} (h : DotEq a b) :
            DotEq b a

            DotEq is symmetric: swap a / b and negate the inside.

            Used by
              theorem

              InformationTheory.Asymptotic.DotEq.trans

              source
              {a b c : ℕ → ℝ} (hab : DotEq a b) (hbc : DotEq b c) :
              DotEq a c

              DotEq is transitive: (log a - log b) + (log b - log c) = (log a - log c).

              Used by
                theorem

                InformationTheory.Asymptotic.DotEq.mul

                source
                {a₁ a₂ b₁ b₂ : ℕ → ℝ} (hPos₁ : ∀ (n : ℕ), 0 < a₁ n ∧ 0 < b₁ n) (hPos₂ : ∀ (n : ℕ), 0 < a₂ n ∧ 0 < b₂ n) (h₁ : DotEq a₁ b₁) (h₂ : DotEq a₂ b₂) :
                DotEq (fun (n : ℕ) => a₁ n * a₂ n) fun (n : ℕ) => b₁ n * b₂ n

                Multiplicative compatibility: a₁ * a₂ ≐ b₁ * b₂ if a_i ≐ b_i (under positivity).

                Proof: log(a₁·a₂) - log(b₁·b₂) = (log a₁ - log b₁) + (log a₂ - log b₂) via Real.log_mul.

                Used by
                  theorem

                  InformationTheory.Asymptotic.DotEq.inv

                  source
                  {a b : ℕ → ℝ} (h : DotEq a b) :
                  DotEq (fun (n : ℕ) => (a n)⁻¹) fun (n : ℕ) => (b n)⁻¹

                  Inverse compatibility: (a n)⁻¹ ≐ (b n)⁻¹ if a ≐ b.

                  Proof: log a⁻¹ - log b⁻¹ = -(log a - log b) via Real.log_inv (unconditional in Mathlib).

                  Used by
                    theorem

                    InformationTheory.Asymptotic.dotEq_iff_tendsto_log_div

                    source
                    (a b : ℕ → ℝ) (hPos : ∀ (n : ℕ), 0 < a n ∧ 0 < b n) :
                    DotEq a b ↔ Filter.Tendsto (fun (n : ℕ) => 1 / ↑n * Real.log (a n / b n)) Filter.atTop (nhds 0)

                    Bridge: under positivity, a ≐ b is equivalent to Tendsto (fun n => (1/n) * log (a n / b n)) atTop (𝓝 0).

                    Used by
                      theorem

                      InformationTheory.Asymptotic.exp_decay_N_of_pos

                      source
                      {g ε' : ℝ} (hg : 0 < g) (hε' : 0 < ε') :
                      ∃ (N : ℕ), ∀ n ≥ N, Real.exp (-↑n * g) < ε'

                      Closed-form block length for exp(-n·g) < ε' (rate-extraction wrapper). For g, ε' > 0, the witness N := ⌈max 0 (-Real.log ε' / g)⌉ + 1 works.

                      Used by

                        Usage examples #