OAI/Combinatorics/EditApproximation/Refinement/ComputedGroupNumerical.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Computed parameters discharge the group scale-count and H^-4 tail bounds.

  1. theorem OAI.EditApproximation.computed_group_scale_count line 10
  2. theorem OAI.EditApproximation.computed_height_exp_upper line 22
  3. theorem OAI.EditApproximation.computed_group_member_exp_bound line 34
  4. theorem OAI.EditApproximation.computed_group_union_failure line 68