OAI/Combinatorics/ThinTrees/Sparsification/IterationPotential.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Iteration potential.

  1. def OAI.AlgorithmicThinTrees.Iteration.lossB line 14
  2. def OAI.AlgorithmicThinTrees.Iteration.potential line 15
  3. lemma OAI.AlgorithmicThinTrees.Iteration.lossB_pos line 17
  4. lemma OAI.AlgorithmicThinTrees.Iteration.potential_pos line 20
  5. lemma OAI.AlgorithmicThinTrees.Iteration.potential_one_le line 21
  6. lemma OAI.AlgorithmicThinTrees.Iteration.potential_le line 23
  7. lemma OAI.AlgorithmicThinTrees.Iteration.potential_step line 28
  8. lemma OAI.AlgorithmicThinTrees.Iteration.coefficient_step line 50