OAI/Probability/SKGap/Entropy/ScalarEntropyTarget.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SKGap.gaussian_tanh_integration_by_parts line 14
  2. theorem OAI.SKGap.scalar_entropy_finite line 25
  3. def OAI.SKGap.scalarEntropyTarget line 88
  4. theorem OAI.SKGap.scalarEntropyTarget_nonneg line 92
  5. theorem OAI.SKGap.scalar_entropy_inequality line 98
  6. theorem OAI.SKGap.scalar_entropy_equality_iff line 108
  7. def OAI.SKGap.EntropyTestBound line 137
  8. def OAI.SKGap.realClip line 140
  9. lemma OAI.SKGap.realClip_bounds line 142
  10. lemma OAI.SKGap.realClip_abs line 147
  11. lemma OAI.SKGap.realClip_le line 153
  12. lemma OAI.SKGap.tendsto_realClip line 156
  13. def OAI.SKGap.clippedBC line 165
  14. lemma OAI.SKGap.entropyTestBound_continuous line 170
  15. lemma OAI.SKGap.entropyTestBound_normalized line 201
  16. lemma OAI.SKGap.integrable_exp_boundedContinuous line 208
  17. lemma OAI.SKGap.boundedContinuous_mgf_deriv line 219
  18. lemma OAI.SKGap.entropyTestBound_zero_eq line 226
  19. lemma OAI.SKGap.entropyTestBound_nonneg line 246