OAI/Combinatorics/IndependentSets/Reduction/UniformLaw.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.LargeIndependentSets.BooleanJunta.cubeMeasurable line 10
  2. instance OAI.LargeIndependentSets.BooleanJunta.cubeSingleton line 11
  3. def OAI.LargeIndependentSets.BooleanJunta.uniformLaw line 13
  4. instance OAI.LargeIndependentSets.BooleanJunta.uniformLaw_probability line 16
  5. lemma OAI.LargeIndependentSets.BooleanJunta.integral_uniformLaw line 19
  6. def OAI.LargeIndependentSets.BooleanJunta.unitLaw line 28
  7. instance OAI.LargeIndependentSets.BooleanJunta.unitLaw_probability line 30
  8. lemma OAI.LargeIndependentSets.BooleanJunta.integral_unitLaw line 34
  9. def OAI.LargeIndependentSets.BooleanJunta.scalarSampler line 37
  10. lemma OAI.LargeIndependentSets.BooleanJunta.scalarSampler_measurable line 39
  11. theorem OAI.LargeIndependentSets.BooleanJunta.scalarSampler_preserving line 42