OAI/Dynamics/ConditionalShuffle/FiniteMinorization.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Thorp.Conditional.Reset.sum_uniform_deficit line 10
  2. lemma OAI.Thorp.Conditional.Reset.uniform_overlap line 29
  3. def OAI.Thorp.Conditional.Reset.squareKernel line 55
  4. lemma OAI.Thorp.Conditional.Reset.square_minorization line 57
  5. def OAI.Thorp.Conditional.Reset.acceptance line 65
  6. def OAI.Thorp.Conditional.Reset.markedKernel line 67
  7. lemma OAI.Thorp.Conditional.Reset.acceptance_bounds line 70
  8. lemma OAI.Thorp.Conditional.Reset.marked_true line 80
  9. lemma OAI.Thorp.Conditional.Reset.marked_marginal line 88
  10. lemma OAI.Thorp.Conditional.Reset.marked_nonneg line 93
  11. lemma OAI.Thorp.Conditional.Reset.marked_sum line 102
  12. lemma OAI.Thorp.Conditional.Reset.accepted_uniform line 105