OAI/Combinatorics/EditApproximation/Coarse/CoarseParameters.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Computed numerical premises of the initial seed

The literal dyadic estimator uses the input-computed branching factor, threshold and precision. Its depth and distortion bounds follow from those integer parameters.

  1. theorem OAI.EditApproximation.computed_coarse_branching line 22
  2. theorem OAI.EditApproximation.computed_coarse_depth line 39
  3. theorem OAI.EditApproximation.computed_coarse_structuralFactor line 53
  4. theorem OAI.EditApproximation.computed_coarse_distortion line 71