OAI/Combinatorics/IndependentSets/Expansion/Supported.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LargeIndependentSets.BooleanJunta.degree_eq_sum line 10
  2. def OAI.LargeIndependentSets.BooleanJunta.Supported line 21
  3. def OAI.LargeIndependentSets.BooleanJunta.walsh line 24
  4. lemma OAI.LargeIndependentSets.BooleanJunta.synth_eq_sum line 28
  5. lemma OAI.LargeIndependentSets.BooleanJunta.walsh_depends line 43
  6. def OAI.LargeIndependentSets.BooleanJunta.truncate line 59
  7. lemma OAI.LargeIndependentSets.BooleanJunta.truncate_depends line 62
  8. lemma OAI.LargeIndependentSets.BooleanJunta.truncate_error line 72
  9. def OAI.LargeIndependentSets.BooleanJunta.influence line 81
  10. lemma OAI.LargeIndependentSets.BooleanJunta.influence_nonneg line 84
  11. lemma OAI.LargeIndependentSets.BooleanJunta.diff_bounded line 87
  12. lemma OAI.LargeIndependentSets.BooleanJunta.diff_square_le_influence line 96
  13. lemma OAI.LargeIndependentSets.BooleanJunta.weighted_fourier_energy line 103
  14. lemma OAI.LargeIndependentSets.BooleanJunta.noise_small_influence line 115
  15. lemma OAI.LargeIndependentSets.BooleanJunta.noise_weight_cancel line 125
  16. lemma OAI.LargeIndependentSets.BooleanJunta.low_degree_coefficient line 130