OAI/Combinatorics/EditApproximation/Probability/ExpectedRegret.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Averaging the first-crossing regret

All parent random choices may be represented by one finite uniform sample. Only the separate marginal laws of online draws and group failures are used. In particular, these two families may be correlated with one another.

  1. theorem OAI.EditApproximation.firstCrossing_expected_sum_bound line 18
  2. theorem OAI.EditApproximation.node_expected_failure_charge line 43

    Source documentation

    Integrating a fixed child-table environment uses only finite linearity. The failure cost is the manuscript's 2 S H^-4 F c.

    theorem node_expected_failure_charge {S H : ℕ} {F c failureBudget : ℝ}
    (hF : 0 ≤ F) (hc : 0 ≤ c)
    (hbudget : failureBudget ≤ (S : ℝ) / (H : ℝ) ^ 4) :
    2 * F * c * failureBudget ≤ 2 * S * (1 / (H : ℝ) ^ 4) * F * c := by
…