OAI/Combinatorics/IndependentSets/Reduction/AuxiliaryJointMeasurable.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LargeIndependentSets.PhaseTest.auxiliary_joint_measurable line 16
  2. theorem OAI.LargeIndependentSets.PhaseTest.deleted_zero_from_junta line 25
  3. def OAI.LargeIndependentSets.Coefficient.value line 79
  4. lemma OAI.LargeIndependentSets.Coefficient.value_nonneg line 80
  5. lemma OAI.LargeIndependentSets.Coefficient.value_le_one line 81
  6. lemma OAI.LargeIndependentSets.Coefficient.value_abs_le_one line 84
  7. lemma OAI.LargeIndependentSets.Coefficient.value_zero line 86
  8. lemma OAI.LargeIndependentSets.Coefficient.value_full line 87
  9. lemma OAI.LargeIndependentSets.Coefficient.value_lower line 90
  10. theorem OAI.LargeIndependentSets.PhaseTest.subchain_juntas line 105
  11. lemma OAI.LargeIndependentSets.PhaseTest.terminal_list_card line 139
  12. lemma OAI.LargeIndependentSets.PhaseTest.rotations_bounded_ae line 150
  13. theorem OAI.LargeIndependentSets.PhaseTest.actual_coefficient_mean_square line 160