OAI/Combinatorics/EditApproximation/Refinement/ComputedNumericalParameters.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

All-seed numerical dimension and source-range bounds after substituting the computed grid size. These bounds do not use an accuracy event.

  1. theorem OAI.EditApproximation.wide_coordinate_budget_le line 12
  2. theorem OAI.EditApproximation.optimizer_parameter_budget_le line 28
  3. theorem OAI.EditApproximation.optimizerTriangularMass_le_square line 40
  4. theorem OAI.EditApproximation.localOnlineMassBound_polynomial line 45
  5. theorem OAI.EditApproximation.computed_localOnlineMassBound_polynomial line 58
  6. theorem OAI.EditApproximation.computed_localOnlineMassBound_bits line 66
  7. theorem OAI.EditApproximation.rejectionBitCount_le_size line 72
  8. theorem OAI.EditApproximation.computed_localOnlineMassBound_rejection_bits line 76