Plain-language statement
Alice produces (p,y) with p close to o.probs y with good probability
Exact Lean statement
lemma alices_close (o : Oracle) (e0 : 0 < e) (q0 : 0 < q) (q1 : q ≤ 1) (n : ℕ) :
(1 - q : ℝ)^n ≤ (alices o (alice e q) n).pr (fun (p,y) ↦ close p (o.probs y) e)Formal artifact
Lean source
lemma alices_close (o : Oracle) (e0 : 0 < e) (q0 : 0 < q) (q1 : q ≤ 1) (n : ℕ) : (1 - q : ℝ)^n ≤ (alices o (alice e q) n).pr (fun (p,y) ↦ close p (o.probs y) e) := by induction' n with n h · simp only [Nat.zero_eq, pow_zero, alices, close_nil, pr_pure, if_true, le_refl] · simp only [pow_succ, alices, Oracle.probs, pr_bind, pr_pure, Vector.tail_cons, close_cons, ite_and_one_zero, exp_const_mul, exp_const, exp_mul_const] apply le_exp_of_cut (fun (p,y) ↦ close p (o.probs y) e) ((1 - q)^n) (1 - q) · apply h · intro (p,y) _ c; simp only at c; simp only [c, if_true, mul_one] exact le_alice_pr o _ e0 q0 y · intro _ _ _; apply mul_nonneg; apply exp_nonneg; intro _ _; repeat apply ite_one_zero_nonneg · linarith- Project
- debate
- License
- Apache-2.0
- Commit
- de3a6e500ae1
- Source
- Debate/Details.lean:294-305
Reuse this declaration
Bring the exact result into your workflow
The import identifies the source module. Your project still needs the pinned package dependency shown on this page.
What this badge means
This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.
Continue in this project
Related declarations
Alice pr le
alice_pr_le
Plain-language statement
Honest Alice has error ≥ e with probability ≤ q
Source project: debate
Person-level attribution pending.
Alice steps cost
alice_steps_cost
Plain-language statement
Alice makes few queries, regardless of Bob and Vera
Source project: debate
Person-level attribution pending.
Alices success
alices_success
Plain-language statement
Alice produces (p,y) with p close and y true with good probability, since if we condition on Alice being close she does as least as well as a close oracle.
Source project: debate
Person-level attribution pending.