OAI/Analysis/PlanarEndpoint/Information/Logarithms.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Finite information laws, entropy and convergence of probability measures.

  1. lemma OAI.PlanarEndpoint.TransverseInformation.bad_conditioning_mass_le line 13
  2. lemma OAI.PlanarEndpoint.TransverseInformation.bad_conditioning_probability_le line 25
  3. lemma OAI.PlanarEndpoint.TransverseInformation.mixture_bad_conditioning_probability_le line 31
  4. lemma OAI.PlanarEndpoint.TransverseInformation.low_probability_mass_le line 44
  5. lemma OAI.PlanarEndpoint.TransverseInformation.restricted_low_probability_mass_le line 55
  6. def OAI.PlanarEndpoint.TransverseInformation.information line 64
  7. lemma OAI.PlanarEndpoint.TransverseInformation.information_difference_eq line 66
  8. lemma OAI.PlanarEndpoint.TransverseInformation.information_bad_iff line 72
  9. lemma OAI.PlanarEndpoint.TransverseInformation.conditioning_information_exception_le line 80