OAI/InformationTheory/BooleanNoise/EndpointLimits.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LeanBlast.CourtadeKumar.tendsto_artanh_div_id_zero_right line 14
  2. theorem OAI.LeanBlast.CourtadeKumar.tendsto_id_div_artanh_zero_right line 20
  3. theorem OAI.LeanBlast.CourtadeKumar.tendsto_entropy_inverse_derivative_zero_right line 25
  4. theorem OAI.LeanBlast.CourtadeKumar.tendsto_artanh_mul_id_div_psi_zero_right line 39
  5. theorem OAI.LeanBlast.CourtadeKumar.tendsto_psi_div_sq_zero_right line 73
  6. theorem OAI.LeanBlast.CourtadeKumar.endpoint_one_sub_sq_pos line 90
  7. theorem OAI.LeanBlast.CourtadeKumar.tendsto_artanh_sub_id_div_cube_zero_right line 95
  8. theorem OAI.LeanBlast.CourtadeKumar.tendsto_entropy_inverse_second_derivative_zero_right line 130