AdaptiveTrials.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Finite adaptive trials

The draws are independent, but whether an attempt succeeds may depend on the entire current state. The head-tail identity below performs the conditioning explicitly. No independence assumption is made about success indicators.

def OAI.LeanBlast.SecondKahnKalai.trialSplitEquiv line 24
Source documentation
Split a finite draw sequence into its first draw and remaining sequence.
```
def trialSplitEquiv (Ω : Type v) (n : ℕ) : Ω × (Fin n → Ω) ≃ (Fin (n + 1) → Ω) where
…
```
theorem OAI.LeanBlast.SecondKahnKalai.FiniteLaw.iid_weight_cons line 36
theorem OAI.LeanBlast.SecondKahnKalai.FiniteLaw.iid_expectation_succ line 41
Source documentation
Exact finite conditional-expectation identity for a fresh independent draw.
```
theorem iid_expectation_succ (μ : FiniteLaw Ω) (n : ℕ)
    (f : (Fin (n + 1) → Ω) → ℝ) :
    (μ.iid (n + 1)).expectation f =
      μ.expectation (fun head => (μ.iid n).expectation (fun tail => f (Fin.cases head tail))) := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.FiniteLaw.expectation

def OAI.LeanBlast.SecondKahnKalai.adaptiveRun line 61

Source documentation

A deterministic adaptive update iterated over a finite sequence of draws.

def adaptiveRun (step : State → Ω → State) :
    (n : ℕ) → State → (Fin n → Ω) → State
  | 0, state, _ => state
  | n + 1, state, draws => adaptiveRun step n (step state (draws 0)) (fun i => draws i.succ)

/-- Number of failed attempts along the actual adaptive state trajectory. -/

def OAI.LeanBlast.SecondKahnKalai.adaptiveFailureCount line 67

Source documentation

Number of failed attempts along the actual adaptive state trajectory.

def adaptiveFailureCount (step : State → Ω → State) (bad : State → Ω → Bool) :
    (n : ℕ) → State → (Fin n → Ω) → ℕ
  | 0, _, _ => 0
  | n + 1, state, draws =>
      (if bad state (draws 0) then 1 else 0) +
        adaptiveFailureCount step bad n (step state (draws 0)) (fun i => draws i.succ)

/-- A uniform state-dependent failure bound controls expected total failures.
This proof conditions at every step on the actual preceding draw and state. -/

theorem OAI.LeanBlast.SecondKahnKalai.adaptiveFailureCount_expectation_le line 76

Source documentation

A uniform state-dependent failure bound controls expected total failures. This proof conditions at every step on the actual preceding draw and state.

theorem adaptiveFailureCount_expectation_le [Fintype Ω]
    (μ : FiniteLaw Ω) (step : State → Ω → State) (bad : State → Ω → Bool)
    (q : ℝ) (hbad : ∀ state, μ.prob (fun draw => bad state draw = true) ≤ q)
    (n : ℕ) (initial : State) :
    (μ.iid n).expectation (fun draws => (adaptiveFailureCount step bad n initial draws : ℝ)) ≤
      (n : ℝ) * q := by
…

Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.adaptiveFailureCount

def OAI.LeanBlast.SecondKahnKalai.rankFailure line 114
Source documentation
Once the rank is zero, later draws are declared successful for the purpose of counting failures. Before then, success means a strict rank decrease.
```
def rankFailure (rank : State → ℕ) (step : State → Ω → State)
    (state : State) (draw : Ω) : Bool :=
…
```
theorem OAI.LeanBlast.SecondKahnKalai.adaptiveRun_rank_le line 118

theorem OAI.LeanBlast.SecondKahnKalai.adaptiveRun_rank_failure_bound line 129

Source documentation

On a trajectory that is still incomplete, every nonfailed attempt consumes at least one unit of rank. The conclusion includes the final positive rank.

theorem adaptiveRun_rank_failure_bound (rank : State → ℕ) (step : State → Ω → State)
    (hstep : ∀ state draw, rank (step state draw) ≤ rank state)
    (n : ℕ) (initial : State) (draws : Fin n → Ω)
    (hincomplete : rank (adaptiveRun step n initial draws) ≠ 0) :
    n + rank (adaptiveRun step n initial draws) ≤
      rank initial + adaptiveFailureCount step (rankFailure rank step) n initial draws := by
…

Mentions: OAI.LeanBlast.SecondKahnKalai.adaptiveRun, OAI.LeanBlast.SecondKahnKalai.adaptiveFailureCount, OAI.LeanBlast.SecondKahnKalai.rankFailure

theorem OAI.LeanBlast.SecondKahnKalai.rankFailure_probability_le line 158

theorem OAI.LeanBlast.SecondKahnKalai.adaptive_incomplete_many_failures line 174

Source documentation

Noncompletion by time 4*s forces at least 3*s+1 failed attempts.

theorem adaptive_incomplete_many_failures (rank : State → ℕ) (step : State → Ω → State)
    (hstep : ∀ state draw, rank (step state draw) ≤ rank state)
    (s : ℕ) (initial : State) (hinitial : rank initial ≤ s)
    (draws : Fin (4 * s) → Ω)
    (hincomplete : rank (adaptiveRun step (4 * s) initial draws) ≠ 0) :
    3 * s + 1 ≤ adaptiveFailureCount step (rankFailure rank step) (4 * s) initial draws := by
…

Mentions: OAI.LeanBlast.SecondKahnKalai.adaptiveRun, OAI.LeanBlast.SecondKahnKalai.adaptiveFailureCount, OAI.LeanBlast.SecondKahnKalai.rankFailure

theorem OAI.LeanBlast.SecondKahnKalai.adaptive_rank_completion line 186

Source documentation

Adaptive finite completion bound. Only fresh draws are independent. The chance of progress can depend arbitrarily on the current state. The case s=0 is included.

theorem adaptive_rank_completion [Fintype Ω] (μ : FiniteLaw Ω)
    (rank : State → ℕ) (step : State → Ω → State)
    (hstep : ∀ state draw, rank (step state draw) ≤ rank state)
    (hprogress : ∀ state, rank state ≠ 0 →
      (3 / 4 : ℝ) ≤ μ.prob (fun draw => rank (step state draw) < rank state))
    (s : ℕ) (initial : State) (hinitial : rank initial ≤ s) :
    (2 / 3 : ℝ) ≤ (μ.iid (4 * s)).prob
      (fun draws => rank (adaptiveRun step (4 * s) initial draws) = 0) := by
…

Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.adaptiveRun

theorem OAI.LeanBlast.SecondKahnKalai.adaptive_counter_completion line 228

Source documentation

Counter form for the tree reduction: counters never decrease, and while fewer than s successful rounds have occurred the chance of an increase is at least three quarters. No finite-state assumption is needed.

theorem adaptive_counter_completion [Fintype Ω] (μ : FiniteLaw Ω)
    (counter : State → ℕ) (step : State → Ω → State)
    (hstep : ∀ state draw, counter state ≤ counter (step state draw))
    (s : ℕ)
    (hprogress : ∀ state, counter state < s →
      (3 / 4 : ℝ) ≤ μ.prob (fun draw => counter state < counter (step state draw)))
    (initial : State) :
    (2 / 3 : ℝ) ≤ (μ.iid (4 * s)).prob
      (fun draws => s ≤ counter (adaptiveRun step (4 * s) initial draws)) := by
…

Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.adaptiveRun