Adapted from k3nfalt/longtails, commit 269cbc764dd36851fd0b64f2f950f329ee127de4. Modified for Lean Pool: module visibility, namespace isolation, and current Mathlib.

theorem LongTails.OracleTemplate.execute_eq_of_answer_eq {Query : Type u_1} {Reply : Type u_2} {Output : Type u_3} (oracle : Oracle Query Reply) (g : Query → Reply) (h : ∀ (k : ℕ) (query : Query) (seed : oracle.Seed 1 k), oracle.answer 1 k (0, query) seed = g query) (A : Algorithm Query Reply Output) (K : ℕ) (seed : A.Seed 1) (oracleSeed : (k : ℕ) → oracle.Seed 1 k) : execute oracle A (fun (x : Fin 1) => K) seed oracleSeed = execute { seedSpace := fun (k : ℕ) => PUnit.instMeasurableSpace, law := ⟨MeasureTheory.Measure.dirac fun (x : ℕ) => (), ⋯⟩, answer := fun (x : ℕ) (query : Fin 1 × Query) (x_1 : Unit) => g query.2 } A (fun (x : Fin 1) => K) seed fun (x : ℕ) => ()

theorem LongTails.OracleTemplate.execute_indexed {Query : Type u_1} {Reply : Type u_2} {Output : Type u_3} (oracle : Oracle Query Reply) (A : Algorithm Query Reply Output) (K : ℕ) (seed : A.Seed 1) (ξ : (k : ℕ) → oracle.Seed 1 k) : execute oracle A (fun (x : Fin 1) => K) seed ξ = A.output 1 ((fun (sc : A.State 1 × ℕ) => (A.update 1 sc.1 (oracle.answer 1 sc.2 (A.query 1 sc.1) (ξ sc.2)), sc.2 + 1))^[K] (A.initial 1 seed, 0)).1

theorem LongTails.OracleTemplate.execute_iterate {Query : Type u_1} {Reply : Type u_2} {Output : Type u_3} (oracle : Query → Reply) (A : Algorithm Query Reply Output) (K : ℕ) (seed : A.Seed 1) : (execute { seedSpace := fun (k : ℕ) => PUnit.instMeasurableSpace, law := ⟨MeasureTheory.Measure.dirac fun (x : ℕ) => (), ⋯⟩, answer := fun (x : ℕ) (query : Fin 1 × Query) (x_1 : Unit) => oracle query.2 } A (fun (x : Fin 1) => K) seed fun (x : ℕ) => ()) = A.output 1 ((fun (s : A.State 1) => A.update 1 s (oracle (A.query 1 s).2))^[K] (A.initial 1 seed))

theorem LongTails.OracleTemplate.execute_eq_of_safe_prefix {Query : Type u_1} {Reply : Type u_2} {Output : Type u_3} {n : ℕ} (O : Oracle Query Reply n) (A : Algorithm Query Reply Output n) (budget : Fin n → ℕ) (seed : A.Seed) (ξ : (k : ℕ) → O.Seed k) (state : ℕ → A.State) (remaining : ℕ → Fin n → ℕ) (T : ℕ) (output : Output) (hstate : state 0 = A.initial seed) (hstep : ∀ (k : ℕ), state (k + 1) = A.update (state k) (O.answer k (A.query (state k)) (ξ k))) (hremaining : remaining 0 = budget) (hconsume : ∀ (k : ℕ), remaining (k + 1) = Function.update (remaining k) (A.query (state k)).1 (remaining k (A.query (state k)).1 - 1)) (hsafe : ∀ k < T, 0 < remaining k (A.query (state k)).1) (houtput : ∀ (k : ℕ), T ≤ k → A.output (state k) = output) (hT : T ≤ ∑ i : Fin n, budget i) : execute O A budget seed ξ = output

theorem LongTails.OracleTemplate.convergence_of_public_budget {S : Setup} (B : S.Public → ℕ) (h : ∃ (make : (p : S.Public) → Algorithm (S.Query p) (S.Reply p) (S.Output p) S.numOracles), (∀ (p : S.Params), S.valid p → ∀ (I : S.Instance (S.publicInput p)) (O : Oracle (S.Query (S.publicInput p)) (S.Reply (S.publicInput p)) S.numOracles), S.admissible p I O → let A := make (S.publicInput p); S.successful p I (fun (seed : A.Seed × ((k : ℕ) → O.Seed k)) => execute O A (fun (x : Fin S.numOracles) => B (S.publicInput p)) seed.1 seed.2) ⟨(↑A.law).prod ↑O.law, ⋯⟩) ∧ ∀ (p : S.Params), S.valid p → S.allowedAlgorithm (S.publicInput p) (make (S.publicInput p))) : Convergence S fun (p : S.Params) (x : Fin S.numOracles) => B (S.publicInput p)

theorem LongTails.OracleTemplate.convergence_of_call_budget {S : Setup} (budget : S.Params → ℕ) (h : ∃ (make : (p : S.Public) → Algorithm (S.Query p) (S.Reply p) (S.Output p) S.numOracles), (∀ (p : S.Params), S.valid p → ∀ (K : ℕ), budget p ≤ K → ∀ (I : S.Instance (S.publicInput p)) (O : Oracle (S.Query (S.publicInput p)) (S.Reply (S.publicInput p)) S.numOracles), S.admissible p I O → let A := make (S.publicInput p); S.successful p I (fun (seed : A.Seed × ((k : ℕ) → O.Seed k)) => execute O A (fun (x : Fin S.numOracles) => K) seed.1 seed.2) ⟨(↑A.law).prod ↑O.law, ⋯⟩) ∧ ∀ (p : S.Params), S.valid p → S.allowedAlgorithm (S.publicInput p) (make (S.publicInput p))) : Convergence S fun (p : S.Params) (x : Fin S.numOracles) => budget p

theorem LongTails.OracleTemplate.convergence_of_block_budget {S : Setup} (B : S.Params → ℕ) (m : S.Public → ℕ) (h : ∃ (make : (p : S.Public) → Algorithm (S.Query p) (S.Reply p) (S.Output p) S.numOracles), (∀ (p : S.Params), S.valid p → ∀ (N : ℕ), B p ≤ N → ∀ (I : S.Instance (S.publicInput p)) (O : Oracle (S.Query (S.publicInput p)) (S.Reply (S.publicInput p)) S.numOracles), S.admissible p I O → let A := make (S.publicInput p); S.successful p I (fun (seed : A.Seed × ((k : ℕ) → O.Seed k)) => execute O A (fun (x : Fin S.numOracles) => m (S.publicInput p) * N) seed.1 seed.2) ⟨(↑A.law).prod ↑O.law, ⋯⟩) ∧ ∀ (p : S.Params), S.valid p → S.allowedAlgorithm (S.publicInput p) (make (S.publicInput p))) : Convergence S fun (p : S.Params) (x : Fin S.numOracles) => m (S.publicInput p) * B p