OAI/Analysis/PlanarEndpoint/Information/JointLaws.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite information laws, entropy and convergence of probability measures.

  1. def OAI.PlanarEndpoint.TransverseInformation.informationVector line 17
  2. def OAI.PlanarEndpoint.TransverseInformation.sampledJointLaw line 21
  3. lemma OAI.PlanarEndpoint.TransverseInformation.sampledJointLaw_nonneg line 26
  4. lemma OAI.PlanarEndpoint.TransverseInformation.sampledJointLaw_integrable line 36
  5. lemma OAI.PlanarEndpoint.TransverseInformation.sampledJointLaw_integral line 43
  6. lemma OAI.PlanarEndpoint.TransverseInformation.sampledJointLaw_mass_tail_le line 50
  7. lemma OAI.PlanarEndpoint.TransverseInformation.sampledJointLaw_expected_tail_le line 68