PolicyRootDecay.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Absorbing the finite branch factor into the root potential gain

theorem OAI.Falconer.eventual_policy_root_decay line 10

Source documentation

The fixed branching factor costs an arbitrarily small power.

theorem eventual_policy_root_decay (D : ℕ) {gain : ℝ}
    (hgain : 0 < gain) (hgain1 : gain ≤ 1) :
    ∃ N₀ : ℕ, ∀ N ≥ N₀, ∀ E x : ℝ, E ≤ -2*gain →
      x ≤ 4^(D+1)*(((2:ℝ)^N)^E+((2:ℝ)^N)^(-10:ℝ)) →
      x ≤ ((2:ℝ)^N)^(-gain) := by
…