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

-- # {{lemma}}: Negligibility is preserved under constant shifts
--
-- If $\varepsilon$ is negligible and $K$ is a fixed constant, then
-- $\varepsilon_2$ defined by $\varepsilon_2(n) = \varepsilon(n - K)$ is also negligible.
--
-- **Proof.** Given target exponent $k$, apply negligibility at exponent $2k$
-- to get $N$ with $\varepsilon(j) \leq j^{-2k}$ for $j \geq N$.
-- For $n \geq \max(N + K,\, 2K,\, 4)$ we have:
-- 1. $n - K \geq N$, so $\varepsilon_2(n) = \varepsilon(n-K) \leq (n-K)^{-2k}$.
-- 2. $n \geq 2K$ implies $n - K \geq n/2$, so $(n-K)^2 \geq (n/2)^2 \geq n$
--    (using $n \geq 4$), giving $n^k \leq (n-K)^{2k}$.
-- 3. Taking reciprocals: $\varepsilon_2(n) \leq (n-K)^{-2k} \leq n^{-k}$.
--
lemma negligible_shift (ε : ℕ → ℝ) (K : ℕ) (hε : Negligible ε) :
    Negligible (fun n => ε (n - K)) := by
  intro k
  -- use the bound at exponent 2k so we have headroom to absorb the shift
  obtain ⟨N, hN⟩ := hε (2 * k)
  refine ⟨max (N + K) (max (2 * K) 4), fun n hn => ?_⟩
  -- unpack the threshold into the three conditions we need
  have hNK  : N + K ≤ n     := (le_max_left _ _).trans hn
  have h2K  : 2 * K ≤ n     := ((le_max_left _ _).trans (le_max_right _ _)).trans hn
  have h4   : 4 ≤ n         := ((le_max_right _ _).trans (le_max_right _ _)).trans hn
  have hKn  : K ≤ n         := by omega
  -- step 1: ε(n - K) ≤ (n - K)^{-2k}  (n - K ≥ N, so hN applies)
  have hstep : ε (n - K) ≤ ((n - K : ℕ) : ℝ) ^ (-(↑(2 * k) : ℤ)) :=
    hN (n - K) (by omega)
  -- step 2: (n - K)^{-2k} ≤ n^{-k}
  have hbound : ((n - K : ℕ) : ℝ) ^ (-(↑(2 * k) : ℤ)) ≤ (n : ℝ) ^ (-(↑k : ℤ)) := by
    -- cast the natural-number subtraction to ℝ
    have hcast : ((n - K : ℕ) : ℝ) = (n : ℝ) - K := Nat.cast_sub hKn
    rw [hcast]
    -- useful numeric facts as real inequalities
    have h2Kr : 2 * (K : ℝ) ≤ n := by exact_mod_cast h2K
    have h4r  : (4 : ℝ) ≤ n     := by exact_mod_cast h4
    -- n - K ≥ n/2 (since K ≤ n/2)
    have h_half : (n : ℝ) / 2 ≤ (n : ℝ) - K := by linarith
    -- (n - K)^2 ≥ n  (from (n-K) ≥ n/2 and n ≥ 4)
    have h_sq : (n : ℝ) ≤ ((n : ℝ) - K) ^ 2 :=
      calc (n : ℝ)
          ≤ (n / 2) ^ 2       := by nlinarith
        _ ≤ ((n : ℝ) - K) ^ 2 := by
            -- monotonicity of squaring: 0 ≤ n/2 and n/2 ≤ n - K
            exact pow_le_pow_left₀ (by linarith) h_half 2
    -- n^k ≤ (n - K)^{2k}  (raise both sides of h_sq to the k-th power)
    have h_pow : (n : ℝ) ^ k ≤ ((n : ℝ) - K) ^ (2 * k) := by
      -- rewrite (n - K)^{2k} = ((n - K)^2)^k then apply monotonicity
      rw [pow_mul]
      exact pow_le_pow_left₀ (by positivity) h_sq k
    -- convert `x^{-c}` to `(x^c)⁻¹` on both sides, then `x^{(c:ℤ)}` to `x^c`
    simp only [zpow_neg, zpow_natCast]
    -- goal: ((n - K)^(2k))⁻¹ ≤ (n^k)⁻¹, which follows from n^k ≤ (n - K)^{2k}
    have hn_pos : (0 : ℝ) < n := by exact_mod_cast show 0 < n by omega
    exact inv_anti₀ (pow_pos hn_pos k) h_pow
  linarith