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

structure LongTails.OracleTemplate.Algorithm (Query : Type uQ) (Reply : Type uR) (Output : Type uO) (numOracles : ℕ := 1) : Type (max (max (uO + 1) (uQ + 1)) (uR + 1))

An oracle algorithm with an internal state and its own random seed.

• Seed : Type

  Random seed used to initialize the algorithm.

• seedSpace : MeasurableSpace self.Seed

  Measurable structure on algorithm seeds.

• law : MeasureTheory.ProbabilityMeasure self.Seed

  Probability law of the algorithm seed.

• State : Type (max uQ uR uO)

  Internal state retained between oracle calls.

• initial : self.Seed → self.State

  Initial state chosen from the algorithm seed.

• query : self.State → Fin numOracles × Query

  Oracle index and query selected by the current state.

• update : self.State → Reply → self.State

  State after receiving the reply to the selected query.

• output : self.State → Output

  Point reported when the query budget is exhausted.

structure LongTails.OracleTemplate.Oracle (Query : Type uQ) (Reply : Type uR) (numOracles : ℕ := 1) : Type (max (max 1 uQ) uR)

A sequence of oracle replies, with an arbitrary joint law for the query samples.

• Seed : ℕ → Type

  Sample type at each query index.

• seedSpace (k : ℕ) : MeasurableSpace (self.Seed k)

  Measurable structure on each query sample.

• law : MeasureTheory.ProbabilityMeasure ((k : ℕ) → self.Seed k)

  Joint probability law of all samples; independence is not assumed.

• answer (k : ℕ) : Fin numOracles × Query → self.Seed k → Reply

  Reply at a query index, oracle index, query and sample.

def LongTails.OracleTemplate.executeLoop {Query : Type uQ} {Reply : Type uR} {Output : Type uO} {numOracles : ℕ} (oracle : ℕ → Fin numOracles × Query → Reply) (A : Algorithm Query Reply Output numOracles) : ℕ → ℕ → (Fin numOracles → ℕ) → A.State → Output

Run at most the supplied fuel, decrementing the budget of each queried oracle.

Equations

• One or more equations did not get rendered due to their size.
• LongTails.OracleTemplate.executeLoop oracle A 0 x✝² x✝¹ x✝ = A.output x✝

def LongTails.OracleTemplate.execute {Query : Type uQ} {Reply : Type uR} {Output : Type uO} {numOracles : ℕ} (oracle : Oracle Query Reply numOracles) (A : Algorithm Query Reply Output numOracles) (budget : Fin numOracles → ℕ) (seed : A.Seed := by exact ()) (oracleSeed : (k : ℕ) → oracle.Seed k := by exact fun _ => ()) : Output

Execute an algorithm using explicit per-oracle call budgets and fixed random seeds.

Equations

• One or more equations did not get rendered due to their size.

structure LongTails.OracleTemplate.Setup : Type (max (max (max (max (max (uD + 1) (uI + 1)) (uO + 1)) (uP + 1)) (uQ + 1)) (uR + 1))

The public information, admissible instances and success criterion of an oracle problem.

• numOracles : ℕ

  Number of available oracle interfaces.

• Params : Type uP

  Parameters of a guarantee, including hidden accuracy targets.

• Public : Type uD

  Information available to the algorithm.

• Instance : self.Public → Type uI

  Mathematical instance hidden behind the oracle.

• Query : self.Public → Type uQ

  Type of query accepted by each oracle.

• Reply : self.Public → Type uR

  Type of oracle reply.

• Output : self.Public → Type uO

  Type of result returned by the algorithm.

• publicInput : self.Params → self.Public

  Public information extracted from guarantee parameters.

• valid : self.Params → Prop

  Admissible numerical regimes for the guarantee parameters.

• admissible (p : self.Params) : self.Instance (self.publicInput p) → Oracle (self.Query (self.publicInput p)) (self.Reply (self.publicInput p)) self.numOracles → Prop

  Mathematical assumptions on the instance and its oracle.

• successful {Ω : Type} [MeasurableSpace Ω] (p : self.Params) : self.Instance (self.publicInput p) → (Ω → self.Output (self.publicInput p)) → MeasureTheory.ProbabilityMeasure Ω → Prop

  Accuracy criterion evaluated under the supplied law of seeds.

• allowedAlgorithm (p : self.Public) : Algorithm (self.Query p) (self.Reply p) (self.Output p) self.numOracles → Prop

  Optional restrictions on the algorithm family.

def LongTails.OracleTemplate.Convergence (S : Setup) (budget : S.Params → Fin S.numOracles → ℕ) : Prop

One algorithm family meets the setup criterion within the stated query budgets.

Equations

• One or more equations did not get rendered due to their size.