OAI/InformationTheory/BooleanNoise/Rearrangement.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LeanBlast.CourtadeKumar.setBit line 15
  2. theorem OAI.LeanBlast.CourtadeKumar.setBit_apply_same line 17
  3. theorem OAI.LeanBlast.CourtadeKumar.setBit_self line 20
  4. theorem OAI.LeanBlast.CourtadeKumar.setBit_setBit line 23
  5. theorem OAI.LeanBlast.CourtadeKumar.setBit_comm line 26
  6. def OAI.LeanBlast.CourtadeKumar.IsIncreasingIn line 33
  7. def OAI.LeanBlast.CourtadeKumar.sortCoordinate line 36
  8. theorem OAI.LeanBlast.CourtadeKumar.sortCoordinate_false line 40
  9. theorem OAI.LeanBlast.CourtadeKumar.sortCoordinate_true line 45
  10. theorem OAI.LeanBlast.CourtadeKumar.sortCoordinate_signValued line 50
  11. theorem OAI.LeanBlast.CourtadeKumar.sortCoordinate_increasingIn line 57
  12. theorem OAI.LeanBlast.CourtadeKumar.sortCoordinate_preserves_increasingIn line 63
  13. theorem OAI.LeanBlast.CourtadeKumar.increasingIn_setBit_mono line 77
  14. theorem OAI.LeanBlast.CourtadeKumar.isIncreasing_of_forall_increasingIn line 86
  15. theorem OAI.LeanBlast.CourtadeKumar.isIncreasing_increasingIn line 107
  16. theorem OAI.LeanBlast.CourtadeKumar.pair_sum_setBit line 116
  17. theorem OAI.LeanBlast.CourtadeKumar.sum_comp_flip line 125
  18. theorem OAI.LeanBlast.CourtadeKumar.sum_setBit_pair line 130
  19. theorem OAI.LeanBlast.CourtadeKumar.cubeAverage_sortCoordinate line 136
  20. def OAI.LeanBlast.CourtadeKumar.coordinatePairMean line 146
  21. def OAI.LeanBlast.CourtadeKumar.coordinatePairDifference line 149
  22. def OAI.LeanBlast.CourtadeKumar.coordinateOffKernel line 152
  23. def OAI.LeanBlast.CourtadeKumar.coordinateOffNoise line 156
  24. theorem OAI.LeanBlast.CourtadeKumar.coordinateOffKernel_setBit_left line 159
  25. theorem OAI.LeanBlast.CourtadeKumar.coordinateOffKernel_setBit_right line 165
  26. theorem OAI.LeanBlast.CourtadeKumar.noiseKernel_setBit_pair line 171
  27. theorem OAI.LeanBlast.CourtadeKumar.coordinateOffKernel_nonneg line 180
  28. theorem OAI.LeanBlast.CourtadeKumar.coordinateOffNoise_add line 186
  29. theorem OAI.LeanBlast.CourtadeKumar.coordinateOffNoise_smul line 191
  30. theorem OAI.LeanBlast.CourtadeKumar.coordinateOffNoise_mono line 195
  31. theorem OAI.LeanBlast.CourtadeKumar.coordinateOffNoise_nonneg line 201
  32. theorem OAI.LeanBlast.CourtadeKumar.coordinateOffNoise_abs_bound line 207
  33. theorem OAI.LeanBlast.CourtadeKumar.noiseOperator_setBit line 220
  34. theorem OAI.LeanBlast.CourtadeKumar.coordinatePairMean_sortCoordinate line 240
  35. theorem OAI.LeanBlast.CourtadeKumar.coordinatePairDifference_sortCoordinate line 245
  36. theorem OAI.LeanBlast.CourtadeKumar.isIncreasing_noiseOperator line 256
  37. theorem OAI.LeanBlast.CourtadeKumar.psi_symmetric_pair_mono line 268
  38. theorem OAI.LeanBlast.CourtadeKumar.rearrangement_sign_bounds line 298
  39. theorem OAI.LeanBlast.CourtadeKumar.psi_noise_sortCoordinate_pair line 303
  40. theorem OAI.LeanBlast.CourtadeKumar.cubeAverage_psi_noise_sortCoordinate line 345
  41. theorem OAI.LeanBlast.CourtadeKumar.informationDeficit_eq_psi_difference line 357
  42. theorem OAI.LeanBlast.CourtadeKumar.informationDeficit_noise_sortCoordinate line 363
  43. def OAI.LeanBlast.CourtadeKumar.sortCoordinates line 371
  44. theorem OAI.LeanBlast.CourtadeKumar.sortCoordinates_signValued line 375
  45. theorem OAI.LeanBlast.CourtadeKumar.cubeAverage_sortCoordinates line 381
  46. theorem OAI.LeanBlast.CourtadeKumar.sortCoordinates_increasingIn line 387
  47. theorem OAI.LeanBlast.CourtadeKumar.informationDeficit_noise_sortCoordinates line 401
  48. theorem OAI.LeanBlast.CourtadeKumar.exists_increasing_informationDeficit_ge line 411