OAI/MeasureTheory/Falconer/Graphs/PolicyGraphError.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Cap counts and error orders for the actual policy graph step

  1. theorem OAI.Falconer.policyGraphRadius_inv_bound line 11
  2. theorem OAI.Falconer.policyGraphCap_count line 36
  3. theorem OAI.Falconer.exists_policy_graph_error_order line 52