From e5e9bde4f367efb60c4283ca2edfb7fb172808f5 Mon Sep 17 00:00:00 2001
From: Geoffrey Irving <irving@naml.us>
Date: Sat, 15 Jun 2024 19:17:27 +0100
Subject: [PATCH] Write down precise constants in the asymptotic complexity

1. Alice takes 5000 k^2 t log t + smaller terms
2. Bob takes 20000/9 k^2 t log t + smaller terms
3. Vera takes 106000 * k^2 + 1
---
 Debate/Correct.lean | 30 +---------------------
 Debate/Cost.lean    | 62 +++++++++++++++++++++++++++++++++++++++++++++
 Debate/Details.lean | 37 +++++++++++++++++++++++++++
 3 files changed, 100 insertions(+), 29 deletions(-)

diff --git a/Debate/Correct.lean b/Debate/Correct.lean
index fe27404..aff7b06 100644
--- a/Debate/Correct.lean
+++ b/Debate/Correct.lean
@@ -1,3 +1,4 @@
+import Debate.Cost
 import Debate.Details
 import Debate.Protocol
 
@@ -24,35 +25,6 @@ theorem soundness (o : Oracle) (L : o.lipschitz t k) (eve : Alice)
     d ≤ ((debate eve (bob p.s p.b p.q) (vera p.c p.s p.v) t).prob' o).prob false :=
   soundness_p o L eve p m
 
-/-- Default valid parameters (not tuned) -/
-def defaults (k : ℝ) (t : ℕ) (k0 : 0 < k) : Params (2/3) (3/5) k t where
-  v := 1/100
-  c := 1/(100*k)
-  s := 2/(100*k)
-  b := 5/(100*k)
-  q := 1/(100*(t+1))
-  k0 := k0
-  cs := by rw [div_lt_div_right]; norm_num; positivity
-  sb := by rw [div_lt_div_right]; norm_num; positivity
-  q1 := by
-    rw [div_le_one]; apply one_le_mul_of_one_le_of_one_le (by norm_num)
-    simp only [le_add_iff_nonneg_left, Nat.cast_nonneg]; positivity
-  v1 := by norm_num
-  qv := by
-    rw [←div_div]; apply div_le_self (by norm_num)
-    simp only [le_add_iff_nonneg_left, Nat.cast_nonneg]
-  bw := by
-    simp only [div_eq_mul_inv, mul_inv, ←mul_assoc, mul_comm _ k⁻¹, inv_mul_cancel (ne_of_gt k0)]
-    norm_num
-  complete := by
-    simp only [←mul_div_assoc, mul_one, mul_comm _ k, ←div_div, div_self (ne_of_gt k0)]
-    rw [mul_comm_div, div_self (Nat.cast_add_one_ne_zero t)]; norm_num
-  sound := by
-    simp only [←mul_div_assoc, mul_one, mul_comm _ k, ←div_div, div_self (ne_of_gt k0)]
-    rw [mul_comm k 5, mul_div_assoc, div_self (ne_of_gt k0), mul_comm_div,
-      div_self (Nat.cast_add_one_ne_zero t)]
-    norm_num
-
 /-- The debate protocol is correct with probability 3/5, using the default parameters -/
 theorem correctness (k : ℝ) (k0 : 0 < k) (t : ℕ) :
     let p := defaults k t k0
diff --git a/Debate/Cost.lean b/Debate/Cost.lean
index 3782325..4f13084 100644
--- a/Debate/Cost.lean
+++ b/Debate/Cost.lean
@@ -1,5 +1,7 @@
 import Comp.Basic
+import Debate.Details
 import Debate.Protocol
+import Mathlib.Data.Complex.ExponentialBounds
 
 /-!
 # Query complexity for each agent in the debate protocol
@@ -109,6 +111,44 @@ theorem bob_debate_cost (o : Oracle) (alice : Alice) (vera : Vera) (t : ℕ):
   · refine exp_le_of_forall_le (fun y m ↦ ?_)
     induction y; repeat simp only [Comp.cost_pure, le_refl]
 
+/-- `Nat.ceil` adds at most one -/
+lemma Nat.ceil_le_add_one {x : ℝ} (x0 : 0 ≤ x) : ⌈x⌉₊ ≤ x + 1 := by
+  rw [natCast_ceil_eq_intCast_ceil x0]
+  exact (Int.ceil_lt_add_one x).le
+
+/-- Alice makes `O(k^2 t log t)` queries with default parameters -/
+theorem alice_fast (k : ℝ) (k0 : 0 < k) (t : ℕ) (bob : Bob) (vera : Vera) :
+    let p := defaults k t k0
+    (debate (alice p.c p.q) bob vera t).cost' o AliceId ≤
+      (t+1) * (5000 * k^2 * Real.log (200 * (t+1)) + 1) := by
+  refine le_trans (alice_debate_cost _ _ _ _) ?_
+  refine mul_le_mul_of_nonneg_left ?_ (by positivity)
+  simp only [defaults, samples, ← Real.log_inv]
+  generalize hn : (t+1 : ℝ) = n
+  field_simp
+  simp only [mul_pow, mul_div_assoc (Real.log _), mul_div_right_comm, mul_right_comm _ _ (2 : ℝ)]
+  norm_num
+  simp only [mul_comm (Real.log _)]
+  refine le_trans (Nat.ceil_le_add_one ?_) (le_refl _)
+  exact mul_nonneg (by positivity) (Real.log_nonneg (by linarith))
+
+/-- Bob makes `O(k^2 t log t)` queries with default parameters -/
+theorem bob_fast (k : ℝ) (k0 : 0 < k) (t : ℕ) (alice : Alice) (vera : Vera) :
+    let p := defaults k t k0
+    (debate alice (bob p.s p.b p.q) vera t).cost' o BobId ≤
+      (t+1) * (20000 / 9 * k^2 * Real.log (200 * (t+1)) + 1) := by
+  generalize hd : (20000 / 9 : ℝ) = d
+  refine le_trans (bob_debate_cost _ _ _ _) ?_
+  refine mul_le_mul_of_nonneg_left ?_ (by positivity)
+  simp only [defaults, samples, ← Real.log_inv]
+  generalize hn : (t+1 : ℝ) = n
+  field_simp
+  simp only [mul_pow, mul_div_assoc (Real.log _), mul_div_right_comm, mul_right_comm _ _ (2 : ℝ)]
+  norm_num
+  simp only [hd, mul_comm (Real.log _)]
+  refine le_trans (Nat.ceil_le_add_one ?_) (le_refl _)
+  exact mul_nonneg (by positivity) (Real.log_nonneg (by linarith))
+
 /-!
 ### Vera cost
 
@@ -175,3 +215,25 @@ theorem vera_debate_cost (o : Oracle) (alice : Alice) (bob : Bob) (t : ℕ):
     · simp only [Comp.cost_bind, Comp.cost_allow_all, vera_cost, Comp.prob_allow_all,
         Comp.cost_pure, exp_const, add_zero, le_refl]
     · simp only [Comp.cost_pure, Nat.cast_nonneg]
+
+/-- A calculation used in `vera_fast` -/
+lemma log_mul_le : Real.log 200 * 20000 ≤ 106000 := by
+  rw [← le_div_iff (by norm_num), Real.log_le_iff_le_exp (by norm_num)]
+  norm_num
+  rw [← Real.exp_one_rpow, div_eq_mul_inv, Real.rpow_mul (by positivity),
+    Real.le_rpow_inv_iff_of_pos (by norm_num) (by positivity) (by norm_num)]
+  refine le_trans ?_ (Real.rpow_le_rpow (by norm_num) Real.exp_one_gt_d9.le (by norm_num))
+  norm_num
+
+/-- Vera makes `O(k^2)` queries with default parameters -/
+theorem vera_fast (k : ℝ) (k0 : 0 < k) (t : ℕ) (alice : Alice) (bob : Bob) :
+    let p := defaults k t k0
+    (debate alice bob (vera p.c p.s p.v) t).cost' o VeraId ≤ 106000 * k^2 + 1 := by
+  refine le_trans (vera_debate_cost _ _ _ _) ?_
+  simp only [defaults, samples, ← Real.log_inv]
+  field_simp
+  refine le_trans (Nat.ceil_le_add_one (by positivity)) ?_
+  simp only [mul_pow, mul_div_assoc (Real.log _), mul_div_right_comm, mul_right_comm _ _ (2 : ℝ)]
+  norm_num [← mul_assoc]
+  refine mul_le_mul_of_nonneg_right ?_ (by positivity)
+  exact log_mul_le
diff --git a/Debate/Details.lean b/Debate/Details.lean
index 0da4bcd..6504a83 100644
--- a/Debate/Details.lean
+++ b/Debate/Details.lean
@@ -604,11 +604,17 @@ Meh, let's get very lazy:
 
 /-- A valid set of parameters for the debate protocol -/
 structure Params (w d k : ℝ) (t : ℕ) where
+  /-- Vera's failure probability -/
   v : ℝ
+  /-- Alice's probability goal: Honest Alice's claimed probabilities are usually off by `≤ c` -/
   c : ℝ
+  /-- Vera's acceptance probability goal: Vera usually accepts if probabilities are off by `≤ s` -/
   s : ℝ
+  /-- Vera's rejection probability goal: Vera usually rejects if probabilities are off by `≥ b` -/
   b : ℝ
+  /-- Alice's and Bob's failure probability -/
   q : ℝ
+  /-- Basic inequalities -/
   k0 : 0 < k
   c0 : 0 < c := by positivity
   cs : c < s
@@ -619,7 +625,9 @@ structure Params (w d k : ℝ) (t : ℕ) where
   v1 : v ≤ 1
   qv : q ≤ v
   bw : k * b ≤ w
+  /-- Inequality sufficient for completeness -/
   complete : d ≤ (1-v) * (w - k * c - q * (t+1))
+  /-- Inequality sufficient for soundness -/
   sound : d ≤ (1-v) * (1 - q * (t+1)) * (w - k * b)
 
 /-- Completeness for any valid parameters -/
@@ -645,3 +653,32 @@ theorem soundness_p (o : Oracle) (L : o.lipschitz t k) (eve : Alice)
   · apply add_le_add_right m
   · linarith [p.bw]
   · apply pow_nonneg; linarith [p.q1]
+
+/-- Default valid parameters (not tuned) -/
+def defaults (k : ℝ) (t : ℕ) (k0 : 0 < k) : Params (2/3) (3/5) k t where
+  v := 1/100
+  c := 1/(100*k)
+  s := 2/(100*k)
+  b := 5/(100*k)
+  q := 1/(100*(t+1))
+  k0 := k0
+  cs := by rw [div_lt_div_right]; norm_num; positivity
+  sb := by rw [div_lt_div_right]; norm_num; positivity
+  q1 := by
+    rw [div_le_one]; apply one_le_mul_of_one_le_of_one_le (by norm_num)
+    simp only [le_add_iff_nonneg_left, Nat.cast_nonneg]; positivity
+  v1 := by norm_num
+  qv := by
+    rw [←div_div]; apply div_le_self (by norm_num)
+    simp only [le_add_iff_nonneg_left, Nat.cast_nonneg]
+  bw := by
+    simp only [div_eq_mul_inv, mul_inv, ←mul_assoc, mul_comm _ k⁻¹, inv_mul_cancel (ne_of_gt k0)]
+    norm_num
+  complete := by
+    simp only [←mul_div_assoc, mul_one, mul_comm _ k, ←div_div, div_self (ne_of_gt k0)]
+    rw [mul_comm_div, div_self (Nat.cast_add_one_ne_zero t)]; norm_num
+  sound := by
+    simp only [←mul_div_assoc, mul_one, mul_comm _ k, ←div_div, div_self (ne_of_gt k0)]
+    rw [mul_comm k 5, mul_div_assoc, div_self (ne_of_gt k0), mul_comm_div,
+      div_self (Nat.cast_add_one_ne_zero t)]
+    norm_num