OAI/Combinatorics/EditApproximation/Probability/SampledRegret.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact sampled action costs

The sampler's finite law translates the computed rational vector into its expected linear cost. Correlation with a group-estimation failure is not excluded or needed in this identity.

  1. theorem OAI.EditApproximation.uniformMean_mono line 19

    Distinct definitions of this name: OAI/Combinatorics/EditApproximation/Coarse/CoarseWork.lean:67 (different declaration text). Qualify references as OAI.EditApproximation.uniformMean_mono@path.

  2. theorem OAI.EditApproximation.uniformMean_add line 23
  3. theorem OAI.EditApproximation.uniformMean_mul line 27
  4. theorem OAI.EditApproximation.uniformMean_const line 31
  5. theorem OAI.EditApproximation.uniformMean_sum line 37
  6. theorem OAI.EditApproximation.finiteRationalOptimizer_sampler_linear_mean line 42
  7. theorem OAI.EditApproximation.actionVector_child_cost_identity line 61
  8. theorem OAI.EditApproximation.actionVector_comparator_cost_identity line 84