OAI/Dynamics/StandardMap/Coupling/FiniteMaximalCoupling.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HyperbolicCoding.finite_maximal_coupling_equal_mass line 12
  2. theorem OAI.HyperbolicCoding.finite_maximal_coupling line 93
  3. lemma OAI.HyperbolicCoding.positive_mass_difference_le line 109
  4. theorem OAI.HyperbolicCoding.finite_coupling_of_lawClose line 128
  5. structure OAI.HyperbolicCoding.MatrixCoupling line 149
  6. lemma OAI.HyperbolicCoding.MatrixCoupling.left_nonneg line 158
  7. lemma OAI.HyperbolicCoding.MatrixCoupling.right_nonneg line 161
  8. lemma OAI.HyperbolicCoding.MatrixCoupling.le_left line 164
  9. lemma OAI.HyperbolicCoding.MatrixCoupling.le_right line 167
  10. def OAI.HyperbolicCoding.MatrixCoupling.glueWeight line 171
  11. lemma OAI.HyperbolicCoding.MatrixCoupling.glueWeight_nonneg line 174
  12. lemma OAI.HyperbolicCoding.MatrixCoupling.glueWeight_row line 177
  13. lemma OAI.HyperbolicCoding.MatrixCoupling.glueWeight_col line 185
  14. def OAI.HyperbolicCoding.MatrixCoupling.comp line 193
  15. def OAI.HyperbolicCoding.MatrixCoupling.cost line 199
  16. lemma OAI.HyperbolicCoding.MatrixCoupling.comp_cost_le line 201
  17. lemma OAI.StandardMapEntropy.Entropy.integrable_finite_observation line 240
  18. def OAI.StandardMapEntropy.Entropy.information line 248
  19. lemma OAI.StandardMapEntropy.Entropy.information_measurable line 251
  20. lemma OAI.StandardMapEntropy.Entropy.information_integrable line 254
  21. lemma OAI.StandardMapEntropy.Entropy.integral_information line 258
  22. lemma OAI.StandardMapEntropy.Entropy.information_nonneg line 264
  23. lemma OAI.StandardMapEntropy.Entropy.ae_mass_positive line 269
  24. lemma OAI.StandardMapEntropy.Entropy.weighted_positive_log_ratio_le line 282
  25. theorem OAI.StandardMapEntropy.Entropy.information_reference_excess line 298
  26. def OAI.HyperbolicCoding.MatrixCoupling.symm line 321
  27. def OAI.HyperbolicCoding.MatrixCoupling.diagonal line 327
  28. lemma OAI.HyperbolicCoding.MatrixCoupling.diagonal_cost line 335
  29. def OAI.HyperbolicCoding.MatrixCoupling.product line 341
  30. lemma OAI.HyperbolicCoding.MatrixCoupling.product_cost line 348
  31. def OAI.HyperbolicCoding.MatrixCoupling.observations line 395
  32. lemma OAI.HyperbolicCoding.MatrixCoupling.observations_cost line 402
  33. lemma OAI.HyperbolicCoding.continuous_cdf_atomless line 418
  34. theorem OAI.HyperbolicCoding.exists_event_real_mass line 427
  35. theorem OAI.HyperbolicCoding.exists_subset_real_mass line 460