OAI/Computability/PerfectCompleteness/Algebra/OutputCharacters.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.OutputCharacters.sliceNumerator_const_mul line 20
  2. theorem OAI.PerfectCompleteness.OutputCharacters.abs_sliceNumerator_le_mass line 32
  3. def OAI.PerfectCompleteness.OutputCharacters.sliceCorrelation line 55
  4. def OAI.PerfectCompleteness.OutputCharacters.conditionalEquality line 59
  5. theorem OAI.PerfectCompleteness.OutputCharacters.abs_sliceCorrelation_le_one line 64
  6. theorem OAI.PerfectCompleteness.OutputCharacters.sliced_output_kernel line 73
  7. theorem OAI.PerfectCompleteness.OutputCharacters.sum_output_correlations line 102
  8. theorem OAI.PerfectCompleteness.OutputCharacters.exists_large_outside line 111
  9. theorem OAI.PerfectCompleteness.OutputCharacters.equality_implies_nonbad_correlation line 140
  10. theorem OAI.PerfectCompleteness.OutputCharacters.abs_conditional_sign_transport line 160
  11. theorem OAI.PerfectCompleteness.OutputCharacters.equality_implies_affine_heavy_witness line 179