OAI/Combinatorics/IndependentSets/Reduction/Mix.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LargeIndependentSets.ProductAveraging.mix line 12
  2. lemma OAI.LargeIndependentSets.ProductAveraging.mix_measurable line 15
  3. lemma OAI.LargeIndependentSets.ProductAveraging.mix_preserving line 23
  4. lemma OAI.LargeIndependentSets.ProductAveraging.update_measurable line 38
  5. lemma OAI.LargeIndependentSets.ProductAveraging.update_preserving line 46
  6. lemma OAI.LargeIndependentSets.ProductAveraging.integral_preserving line 64
  7. lemma OAI.LargeIndependentSets.ProductAveraging.integral_update line 71
  8. def OAI.LargeIndependentSets.BooleanJunta.unitCubeLaw line 88
  9. instance OAI.LargeIndependentSets.BooleanJunta.unitCubeLaw_probability line 89
  10. lemma OAI.LargeIndependentSets.BooleanJunta.unitCubeLaw_absolutelyContinuous line 92
  11. lemma OAI.LargeIndependentSets.BooleanJunta.update_lipschitz line 98
  12. lemma OAI.LargeIndependentSets.BooleanJunta.slice_lipschitz line 110
  13. lemma OAI.LargeIndependentSets.BooleanJunta.variation_eq_integral_coordinate line 115
  14. lemma OAI.LargeIndependentSets.BooleanJunta.total_integral_slice_variation line 126
  15. def OAI.LargeIndependentSets.BooleanJunta.seedLaw line 145
  16. instance OAI.LargeIndependentSets.BooleanJunta.seedLaw_probability line 146
  17. def OAI.LargeIndependentSets.BooleanJunta.seedCubeLaw line 147
  18. instance OAI.LargeIndependentSets.BooleanJunta.seedCubeLaw_probability line 149
  19. def OAI.LargeIndependentSets.BooleanJunta.cubeSampler line 152
  20. lemma OAI.LargeIndependentSets.BooleanJunta.cubeSampler_preserving line 155
  21. lemma OAI.LargeIndependentSets.BooleanJunta.cubeSampler_update line 160
  22. def OAI.LargeIndependentSets.BooleanJunta.flipSeed line 167
  23. lemma OAI.LargeIndependentSets.BooleanJunta.flipSeed_measurable line 170
  24. def OAI.LargeIndependentSets.BooleanJunta.sampledDiff line 173
  25. lemma OAI.LargeIndependentSets.BooleanJunta.sampledDiff_measurable line 177
  26. lemma OAI.LargeIndependentSets.BooleanJunta.sampledDiff_le_one line 185
  27. lemma OAI.LargeIndependentSets.BooleanJunta.sampledDiff_integrable line 195
  28. lemma OAI.LargeIndependentSets.BooleanJunta.sampledDiff_fiber line 203
  29. lemma OAI.LargeIndependentSets.BooleanJunta.integral_sampledDiff_fiber line 211
  30. theorem OAI.LargeIndependentSets.BooleanJunta.total_sampled_influence line 227