OAI/InformationTheory/BooleanNoise/SemigroupFlow.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LeanBlast.CourtadeKumar.noiseFlow line 17
  2. theorem OAI.LeanBlast.CourtadeKumar.noiseKernel_flip_derivative_term line 20
  3. theorem OAI.LeanBlast.CourtadeKumar.hasDerivAt_noise_factor line 38
  4. theorem OAI.LeanBlast.CourtadeKumar.hasDerivAt_noiseKernel_flow line 50
  5. theorem OAI.LeanBlast.CourtadeKumar.cubeDerivative_noiseOperator line 60
  6. theorem OAI.LeanBlast.CourtadeKumar.hasDerivAt_noiseFlow line 67
  7. theorem OAI.LeanBlast.CourtadeKumar.continuous_noiseFlow line 79
  8. theorem OAI.LeanBlast.CourtadeKumar.noiseFlow_zero line 84
  9. theorem OAI.LeanBlast.CourtadeKumar.cubeAverage_noiseFlow line 88
  10. theorem OAI.LeanBlast.CourtadeKumar.meanVariance_noiseFlow line 92
  11. theorem OAI.LeanBlast.CourtadeKumar.isInterior_noiseFlow line 96
  12. theorem OAI.LeanBlast.CourtadeKumar.isIncreasing_noiseFlow line 103
  13. theorem OAI.LeanBlast.CourtadeKumar.hasDerivAt_entropyAverage_noiseFlow_of_isInterior line 109
  14. theorem OAI.LeanBlast.CourtadeKumar.hasDerivAt_entropyAverage_noiseFlow line 121
  15. theorem OAI.LeanBlast.CourtadeKumar.hasDerivAt_informationDeficit_noiseFlow_of_isInterior line 128
  16. theorem OAI.LeanBlast.CourtadeKumar.hasDerivAt_informationDeficit_noiseFlow line 136
  17. theorem OAI.LeanBlast.CourtadeKumar.continuous_entropyAverage_noiseFlow line 143
  18. theorem OAI.LeanBlast.CourtadeKumar.continuous_informationDeficit_noiseFlow line 148
  19. theorem OAI.LeanBlast.CourtadeKumar.entropyAverage_eq_zero_of_signValued line 153
  20. theorem OAI.LeanBlast.CourtadeKumar.tendsto_entropyAverage_noiseFlow_zero line 160
  21. theorem OAI.LeanBlast.CourtadeKumar.tendsto_entropyAverage_noiseFlow_zero_right line 166
  22. theorem OAI.LeanBlast.CourtadeKumar.entropyAverage_noiseFlow_pos line 171
  23. theorem OAI.LeanBlast.CourtadeKumar.meanVariance_noiseFlow_pos line 178