OAI/Analysis/PlanarEndpoint/Information/Expectations.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Finite information laws, entropy and convergence of probability measures.

  1. def OAI.PlanarEndpoint.TransverseInformation.informationClip line 17
  2. lemma OAI.PlanarEndpoint.TransverseInformation.informationClip_nonneg line 19
  3. lemma OAI.PlanarEndpoint.TransverseInformation.informationClip_le_bound line 22
  4. lemma OAI.PlanarEndpoint.TransverseInformation.informationClip_eq line 25
  5. lemma OAI.PlanarEndpoint.TransverseInformation.continuous_informationClip line 29
  6. def OAI.PlanarEndpoint.TransverseInformation.clippedInformation line 32
  7. lemma OAI.PlanarEndpoint.TransverseInformation.informationClip_error_le line 46
  8. lemma OAI.PlanarEndpoint.TransverseInformation.integral_informationClip_error_le line 57
  9. theorem OAI.PlanarEndpoint.TransverseInformation.expected_information_tendsto line 71