OAI/NumberTheory/JointDickman/Counting/EntropyWindowStability.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform entropy estimates across regularity windows

  1. theorem OAI.JointDickman.entropy_window_stability line 13

    Source documentation

    Uniformity includes both endpoint cardinalities. The population stays away from zero because the prefix scale g is fixed and positive.

    theorem entropy_window_stability {g ε : ℝ} (hg : 0 < g) (hε : 0 < ε) :
    ∃ τ₀ : ℝ, 0 < τ₀ ∧ ∀ (τ x y r : ℝ), 0 ≤ τ → τ ≤ τ₀ →
      0 ≤ r → r ≤ 1/2 → |x-g/2| ≤ τ → |y-g*r| ≤ 3*τ →
      x*Real.binEntropy (y/x) ≤ (g/2)*Real.binEntropy (2*r)+ε := by
…