OAI/Combinatorics/IndependentSets/Repetition/ScalarCell.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargeIndependentSets.BooleanJunta.scalarCell line 11
  2. lemma OAI.LargeIndependentSets.BooleanJunta.scalarCell_mem line 15
  3. lemma OAI.LargeIndependentSets.BooleanJunta.scalarCell_lipschitz line 25
  4. def OAI.LargeIndependentSets.BooleanJunta.scalarAvg line 45
  5. def OAI.LargeIndependentSets.BooleanJunta.variation line 48
  6. def OAI.LargeIndependentSets.BooleanJunta.halfInput line 50
  7. lemma OAI.LargeIndependentSets.BooleanJunta.halfInput_lipschitz line 52
  8. lemma OAI.LargeIndependentSets.BooleanJunta.scalarAvg_cons line 62
  9. lemma OAI.LargeIndependentSets.BooleanJunta.variation_nonneg line 65
  10. lemma OAI.LargeIndependentSets.BooleanJunta.variation_half_sum line 68
  11. lemma OAI.LargeIndependentSets.BooleanJunta.half_integral_sum line 102
  12. lemma OAI.LargeIndependentSets.BooleanJunta.mean_scalarAvg line 117
  13. lemma OAI.LargeIndependentSets.BooleanJunta.scalarAvg_difference line 130
  14. lemma OAI.LargeIndependentSets.BooleanJunta.influence_succ line 155
  15. theorem OAI.LargeIndependentSets.BooleanJunta.dyadic_total_influence line 161