OAI/Combinatorics/EditApproximation/Binary/BinaryTriangularSpace.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.triangularMassAllocation_le_work line 12
2. theorem OAI.EditApproximation.triangularChoiceAllocation_le_work line 27

   Source documentation

   Allocate the exact threshold words visited by the triangular sampler. The sampled integer and thresholds are already bounded finite words.

   theorem triangularChoiceAllocation_le_work (K : ℕ) (integer : Fin (optimizerTriangularMass K)) :
       triangularChoiceAllocation K integer ≤ (triangularChoiceWithWork K integer).2 := by
   …

   Mentions: OAI.EditApproximation.optimizerTriangularMass, OAI.EditApproximation.triangularChoiceAllocation, OAI.EditApproximation.triangularChoiceWithWork