Negligible Functions

import Mathlib.Analysis.SpecialFunctions.Pow.Real

-- leandown
-- [meta]
-- title = "Negligible functions"
-- group = "Cryptography"
-- [content]

-- # {{definition}}: Negligible functions
--
-- A function $\varepsilon : \mathbb{N} \to \mathbb{R}$ is **negligible** if it
-- eventually falls below every inverse polynomial: for every $c : \mathbb{N}$,
-- there exists $N$ such that for all $n \geq N$,
--
-- $$\varepsilon(n) \leq n^{-c}$$
--
-- Intuitively, a negligible function goes to zero faster than any polynomial rate.
-- In cryptography, a security reduction succeeds if the adversary's advantage
-- is negligible in the security parameter.
--
/-- A function `ε : ℕ → ℝ` is **negligible** if for every polynomial exponent `c : ℕ`,
    `ε(n)` eventually falls below `n^{-c}`. -/
def Negligible (ε : ℕ → ℝ) : Prop :=
  ∀ c : ℕ, ∃ N : ℕ, ∀ n ≥ N, ε n ≤ (n : ℝ) ^ (-(c : ℤ))

-- # {{theorem}}: The constant function 1 is not negligible
--
-- **proof sketch:**
-- - take $c = 1$; we need $\varepsilon(n) \leq n^{-1}$ for large $n$
-- - but $\varepsilon(n) = 1$ and $n^{-1} < 1$ for $n \geq 2$, contradiction
--
/-- The constant function 1 is not negligible. -/
lemma not_negligible_one : ¬ Negligible (fun _ => (1 : ℝ)) := by
  -- assume for contradiction that the constant function 1 is negligible
  intro h
  -- instantiate with exponent $c = 1$: get threshold $N$ with $1 \leq (n+2)^{-1}$ for $n \geq N$
  obtain ⟨N, hN⟩ := h 1
  -- apply the bound at $n = N + 2 \geq N$
  have hle := hN (N + 2) (by omega)
  -- show $(N+2)^{-1} < 1$: rewrite as $1 / (N+2) < 1$, which holds since $N + 2 > 1$
  have hlt : ((N : ℝ) + 2) ^ (-(1 : ℤ)) < 1 := by
    rw [zpow_neg, zpow_one, inv_eq_one_div, div_lt_one (by positivity)]
    norm_cast; omega
  -- `hle` has type `(1 : ℝ) ≤ ↑(N + 2) ^ (-(1 : ℤ))`; `push_cast` rewrites the
  -- coercion `↑(N + 2)` to `(↑N + 2 : ℝ)` so `linarith` can combine it with `hlt`
  push_cast at hle
  linarith