OAI/Combinatorics/EditApproximation/Coarse/CoarseLevelMagnitude.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.BinaryFraction.coarseLevelMagnitude line 10

   Source documentation

   Loose magnitude bound for all partial child sums. Its bit length is linear in the depth and parameter bit lengths.

   def coarseLevelMagnitude (N k B d : ℕ) : ℕ :=
   …

2. theorem OAI.EditApproximation.BinaryFraction.coarseLevelMagnitude_pos line 13
3. theorem OAI.EditApproximation.BinaryFraction.coarseLevelMagnitude_ge line 17
4. theorem OAI.EditApproximation.BinaryFraction.coarseLevelMagnitude_mono line 24
5. theorem OAI.EditApproximation.BinaryFraction.coarseLevelMagnitude_succ line 30
6. theorem OAI.EditApproximation.BinaryFraction.coarseLevelMagnitude_bits line 42