FirstCrossing.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The actual first crossing of a finite action band

The crossing index is computed from the fixed child tables for analysis. It is independent of parent sampling. The lemmas separate the prefixPayoff, the single crossing, and the nonpositive later clipped regrets.

def OAI.EditApproximation.firstCrossing line 18
theorem OAI.EditApproximation.firstCrossing_le line 22
theorem OAI.EditApproximation.before_firstCrossing line 30
theorem OAI.EditApproximation.at_firstCrossing line 43

theorem OAI.EditApproximation.after_firstCrossing_parent line 55

Source documentation

At every later time, the previous-index Bellman option uses the same crossing action. Child-table monotonicity keeps its cost below c.

theorem after_firstCrossing_parent {α : Type*} (band : Finset α)
    (S : ℕ) (actionCost : ℕ → α → ℝ) (c : ℝ) (parent : ℕ → ℝ)
    (hmono : ∀ action ∈ band, Antitone (fun t => actionCost t action))
    (hbellman : ∀ t < S, ∀ action ∈ band, parent (t + 1) ≤ actionCost t action)
    {t : ℕ} (hafter : firstCrossing band S actionCost c < t) (ht : t < S) :
    max c (parent t) = c := by
…

Mentions: OAI.EditApproximation.firstCrossing

theorem OAI.EditApproximation.firstCrossing_sum_bound line 72

Source documentation

A finite first-crossing partition charges the crossing only once. All failure indicators may be correlated with the sampled actions.

theorem firstCrossing_sum_bound (S crossing : ℕ) (regret prefixPayoff failure : ℕ → ℝ)
    (crossingCharge failureCharge : ℝ) (hcrossing : crossing ≤ S)
    (hcharge : 0 ≤ crossingCharge) (hfailureCharge : 0 ≤ failureCharge)
    (hfailure : ∀ t < S, 0 ≤ failure t)
    (hprefixPayoff : ∀ t < crossing, regret t ≤ prefixPayoff t + failureCharge * failure t)
    (hcross : crossing < S → regret crossing ≤ crossingCharge + failureCharge * failure crossing)
    (hafter : ∀ t < S, crossing < t → regret t ≤ 0) :
    (∑ t ∈ range S, regret t) ≤
      (∑ t ∈ range crossing, prefixPayoff t) + crossingCharge +
        failureCharge * ∑ t ∈ range S, failure t := by
…