OAI/InformationTheory/BooleanNoise/FiniteNoise.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LeanBlast.CourtadeKumar.card_cube line 20
  2. theorem OAI.LeanBlast.CourtadeKumar.cube_denominator_pos line 23
  3. theorem OAI.LeanBlast.CourtadeKumar.cubeAverage_const line 25
  4. theorem OAI.LeanBlast.CourtadeKumar.cubeAverage_zeroDim line 29
  5. theorem OAI.LeanBlast.CourtadeKumar.cubeAverage_add line 34
  6. theorem OAI.LeanBlast.CourtadeKumar.cubeAverage_sub line 38
  7. theorem OAI.LeanBlast.CourtadeKumar.cubeAverage_neg line 42
  8. theorem OAI.LeanBlast.CourtadeKumar.cubeAverage_smul line 46
  9. theorem OAI.LeanBlast.CourtadeKumar.cubeAverage_sum line 50
  10. theorem OAI.LeanBlast.CourtadeKumar.cubeAverage_nonneg line 55
  11. theorem OAI.LeanBlast.CourtadeKumar.cubeAverage_mono line 59
  12. theorem OAI.LeanBlast.CourtadeKumar.cubeAverage_strict_mono line 64
  13. theorem OAI.LeanBlast.CourtadeKumar.cubeAverage_lt line 71
  14. theorem OAI.LeanBlast.CourtadeKumar.IsInterior.cubeAverage line 75
  15. theorem OAI.LeanBlast.CourtadeKumar.cubeAverage_le_const line 81
  16. theorem OAI.LeanBlast.CourtadeKumar.const_le_cubeAverage line 85
  17. theorem OAI.LeanBlast.CourtadeKumar.noiseKernel_symm line 89
  18. theorem OAI.LeanBlast.CourtadeKumar.noiseKernel_nonneg line 97
  19. theorem OAI.LeanBlast.CourtadeKumar.noiseKernel_pos line 103
  20. theorem OAI.LeanBlast.CourtadeKumar.noiseKernel_row_sum line 109
  21. theorem OAI.LeanBlast.CourtadeKumar.noiseKernel_col_sum line 121
  22. theorem OAI.LeanBlast.CourtadeKumar.noiseKernel_split_coord line 126
  23. theorem OAI.LeanBlast.CourtadeKumar.noiseOperator_const line 132
  24. theorem OAI.LeanBlast.CourtadeKumar.noiseOperator_add line 136
  25. theorem OAI.LeanBlast.CourtadeKumar.noiseOperator_sub line 140
  26. theorem OAI.LeanBlast.CourtadeKumar.noiseOperator_neg line 144
  27. theorem OAI.LeanBlast.CourtadeKumar.noiseOperator_smul line 148
  28. theorem OAI.LeanBlast.CourtadeKumar.cubeAverage_noiseOperator line 152
  29. theorem OAI.LeanBlast.CourtadeKumar.noiseOperator_prod line 158
  30. theorem OAI.LeanBlast.CourtadeKumar.noiseKernel_zero line 166
  31. theorem OAI.LeanBlast.CourtadeKumar.noiseOperator_zero_correlation line 170
  32. theorem OAI.LeanBlast.CourtadeKumar.noiseKernel_one line 176
  33. theorem OAI.LeanBlast.CourtadeKumar.noiseOperator_one line 182
  34. theorem OAI.LeanBlast.CourtadeKumar.noiseOperator_mono line 186
  35. theorem OAI.LeanBlast.CourtadeKumar.noiseOperator_bounds line 192
  36. theorem OAI.LeanBlast.CourtadeKumar.noiseOperator_strict_mono line 199
  37. theorem OAI.LeanBlast.CourtadeKumar.exists_signs_of_nonconstant line 208
  38. theorem OAI.LeanBlast.CourtadeKumar.noiseOperator_isInterior_of_exists_signs line 217
  39. theorem OAI.LeanBlast.CourtadeKumar.noiseOperator_isInterior line 235
  40. theorem OAI.LeanBlast.CourtadeKumar.cubeAverage_mem_Ioo_of_signValued_nonconstant line 241
  41. theorem OAI.LeanBlast.CourtadeKumar.meanVariance_pos_of_signValued_nonconstant line 247