OAI/Computability/PerfectCompleteness/Foundations/DualQuotientRowsLemmas.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.DualQuotientRows.quotientRowEquiv line 21
  2. theorem OAI.PerfectCompleteness.DualQuotientRows.quotientRowEquiv_val line 26
  3. theorem OAI.PerfectCompleteness.DualQuotientRows.codim_dualAnnihilator_eq line 29
  4. theorem OAI.PerfectCompleteness.DualQuotientRows.uniform_quotientRowEquiv line 36
  5. theorem OAI.PerfectCompleteness.DualQuotientRows.uniform_pullback_rows line 43
  6. theorem OAI.PerfectCompleteness.DualQuotientRows.uniform_affine_pullback_rows line 56
  7. def OAI.PerfectCompleteness.DualQuotientRows.nativeRowMap line 74
  8. theorem OAI.PerfectCompleteness.DualQuotientRows.apply_nativeRowMap line 79
  9. theorem OAI.PerfectCompleteness.DualQuotientRows.nativeRowMap_injective line 86
  10. theorem OAI.PerfectCompleteness.DualQuotientRows.range_nativeRowMap line 94
  11. def OAI.PerfectCompleteness.DualQuotientRows.nativeRowLinear line 113
  12. def OAI.PerfectCompleteness.DualQuotientRows.nativeRowEquiv line 119
  13. theorem OAI.PerfectCompleteness.DualQuotientRows.nativeRowEquiv_val line 133
  14. theorem OAI.PerfectCompleteness.DualQuotientRows.codim_dualCoannihilator_eq line 137
  15. theorem OAI.PerfectCompleteness.DualQuotientRows.uniform_nativeRowEquiv line 143
  16. def OAI.PerfectCompleteness.LevelPairCounting.winCount line 165
  17. def OAI.PerfectCompleteness.LevelPairCounting.pairProbability line 168
  18. theorem OAI.PerfectCompleteness.LevelPairCounting.pairProbability_self line 172
  19. theorem OAI.PerfectCompleteness.LevelPairCounting.pairProbability_comm line 179
  20. theorem OAI.PerfectCompleteness.LevelPairCounting.expectation_indicator line 186
  21. theorem OAI.PerfectCompleteness.LevelPairCounting.expectation_indicator_mul line 190
  22. theorem OAI.PerfectCompleteness.LevelPairCounting.first_moment_eq_sum line 200
  23. theorem OAI.PerfectCompleteness.LevelPairCounting.second_moment_eq_sum line 208
  24. theorem OAI.PerfectCompleteness.LevelPairCounting.second_moment_decomposition line 217
  25. theorem OAI.PerfectCompleteness.LevelPairCounting.second_moment_le_mean_add line 235
  26. theorem OAI.PerfectCompleteness.LevelPairCounting.exists_level_pair line 254
  27. theorem OAI.PerfectCompleteness.LevelPairReserve.exists_pair line 307
  28. def OAI.PerfectCompleteness.SmallBiasSlice.bitSign line 363
  29. def OAI.PerfectCompleteness.SmallBiasSlice.maskChar line 365
  30. theorem OAI.PerfectCompleteness.SmallBiasSlice.maskChar_zero line 369
  31. theorem OAI.PerfectCompleteness.SmallBiasSlice.abs_maskChar line 373
  32. theorem OAI.PerfectCompleteness.SmallBiasSlice.maskChar_xor line 381
  33. theorem OAI.PerfectCompleteness.SmallBiasSlice.maskChar_kernel line 390
  34. theorem OAI.PerfectCompleteness.SmallBiasSlice.expectation_const_mul line 416
  35. def OAI.PerfectCompleteness.SmallBiasSlice.sliceNumerator line 424
  36. def OAI.PerfectCompleteness.SmallBiasSlice.sliceMass line 428
  37. theorem OAI.PerfectCompleteness.SmallBiasSlice.slice_expansion line 431
  38. theorem OAI.PerfectCompleteness.SmallBiasSlice.sliceMass_lower line 465
  39. theorem OAI.PerfectCompleteness.SmallBiasSlice.slice_coefficient_witness line 499
  40. def OAI.PerfectCompleteness.SmallBiasSlice.rowCombination line 525
  41. theorem OAI.PerfectCompleteness.SmallBiasSlice.rowCombination_zero line 529
  42. theorem OAI.PerfectCompleteness.SmallBiasSlice.character_rowCombination line 533
  43. theorem OAI.PerfectCompleteness.SmallBiasSlice.coset_coefficient_witness line 553
  44. theorem OAI.PerfectCompleteness.SmallBiasSlice.affine_coset_heavy_witness line 567