OAI/Combinatorics/EditApproximation/Geometry/GroupNumerical.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Explicit numerical slack for the shared group estimator and online increments.

  1. theorem OAI.EditApproximation.group_normalized_exponent line 10
  2. theorem OAI.EditApproximation.group_exponent_polynomial_slack line 32
  3. theorem OAI.EditApproximation.group_union_failure_numeric line 51

    Source documentation

    The union bound is below H^-4 once its literal count bounds and the computed height/representative growth bounds have been substituted.

    theorem group_union_failure_numeric {ell H members scales : ℝ}
    (hell : 8 ≤ ell) (hH : 0 < H) (hHexp : H ≤ Real.exp ell)
    (_hmembers : 0 ≤ members) (hmembersBound : members ≤ 4 * Real.exp (2 * ell ^ 2))
    (hscales : 0 ≤ scales) (hscalesBound : scales ≤ 2 * ell) :
    members * scales * (2 * Real.exp (-(ell ^ 37 / 3000))) ≤ 1 / H ^ 4 := by
…