Execution.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

inductive OAI.PlanarL1.Execution line 12
Source documentation
Finite adaptive execution trees. Every node makes an actual uniform finite choice; its continuation, including the number of later choices, may depend on that choice. This is the finite probability law used by the manuscript.
```
inductive Execution (α : Type*) where
…
```
def OAI.PlanarL1.Execution.mean line 20
def OAI.PlanarL1.Execution.prob line 24
def OAI.PlanarL1.Execution.bind line 28
lemma OAI.PlanarL1.Execution.mean_const line 32
lemma OAI.PlanarL1.Execution.mean_add line 37
lemma OAI.PlanarL1.Execution.mean_smul line 43
lemma OAI.PlanarL1.Execution.mean_mono line 49
lemma OAI.PlanarL1.Execution.mean_nonneg line 55
lemma OAI.PlanarL1.Execution.mean_bind line 58
lemma OAI.PlanarL1.Execution.prob_bind line 64
lemma OAI.PlanarL1.Execution.prob_nonneg line 67
lemma OAI.PlanarL1.Execution.prob_le_one line 71
lemma OAI.PlanarL1.Execution.prob_compl line 76
lemma OAI.PlanarL1.Execution.prob_mono line 89
lemma OAI.PlanarL1.Execution.mean_lower_of_event line 98

lemma OAI.PlanarL1.Execution.conditional_loss line 110

Source documentation

Conditional failure bounds compose even when later grids and cell choices are chosen using the entire previous history.

lemma conditional_loss (E : Execution α) (F : α → Execution β)
    (P : α → Prop) (Q : β → Prop) {ε : ℝ} (hε : 0 ≤ ε)
    (h : ∀ x, P x → (F x).prob (fun y => ¬Q y) ≤ ε) :
    (E.bind F).prob (fun y => ¬Q y) ≤ E.prob (fun x => ¬P x)+ε := by
…

Mentions: OAI.PlanarL1.Execution, OAI.PlanarL1.Execution.prob

lemma OAI.PlanarL1.Execution.conditional_success line 130
def OAI.PlanarL1.Execution.evolve line 138
Source documentation
Evolution retains the complete state, which can itself contain the past.
```
def evolve (step : ℕ → α → Execution α) (start : Execution α) : ℕ → Execution α
  | 0 => start
  | k+1 => (evolve step start k).bind (step k)
```
Mentions: OAI.PlanarL1.Execution, OAI.PlanarL1.Execution.bind
lemma OAI.PlanarL1.Execution.evolve_loss line 142

theorem OAI.PlanarL1.Execution.surviving_success line 156

Source documentation

The source's 1/2 · p · br/2 calculation, including adaptive first loss.

theorem surviving_success (E : Execution α) (F : α → Execution β)
    (P : α → Prop) (Q : β → Prop) {p c d : ℝ} (hp : 0 ≤ p) (hc : 0 ≤ c)
    (hloss : E.prob (fun x => ¬P x) ≤ 1/2)
    (hs : ∀ x, P x → p ≤ (F x).prob Q)
    (value : β → ℝ) (hv : ∀ y, 0 ≤ value y)
    (hq : ∀ y, Q y → c ≤ value y) (hd : d ≤ c*p/2) :
    d ≤ (E.bind F).mean value := by
…

Mentions: OAI.PlanarL1.Execution, OAI.PlanarL1.Execution.prob, OAI.PlanarL1.Execution.mean

def OAI.PlanarL1.Execution.uniform line 176
lemma OAI.PlanarL1.Execution.mean_uniform line 183
lemma OAI.PlanarL1.Execution.prob_uniform line 197
lemma OAI.PlanarL1.Execution.mean_sum line 205