OAI/Dynamics/StandardMap/Coupling/SequentialChunkCoupling.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HyperbolicCoding.finiteName line 15
  2. lemma OAI.HyperbolicCoding.finiteName_measurable line 18
  3. lemma OAI.HyperbolicCoding.finiteName_cons line 23
  4. def OAI.HyperbolicCoding.independentNameWeights line 30
  5. lemma OAI.HyperbolicCoding.independentNameWeights_cons line 35
  6. lemma OAI.HyperbolicCoding.mass_equiv_inverse line 46
  7. lemma OAI.HyperbolicCoding.nameCost_split line 55
  8. theorem OAI.HyperbolicCoding.sequential_chunk_coupling line 60
  9. lemma OAI.HyperbolicCoding.LawClose.nonneg line 132
  10. lemma OAI.HyperbolicCoding.lawClose_pair_factor_left line 135
  11. lemma OAI.HyperbolicCoding.lawClose_pair_swap line 146
  12. lemma OAI.HyperbolicCoding.map_observation_comp line 155
  13. lemma OAI.HyperbolicCoding.lawClose_pair_comp line 160
  14. def OAI.HyperbolicCoding.chunkObservation line 181
  15. lemma OAI.HyperbolicCoding.chunkObservation_measurable line 185
  16. def OAI.HyperbolicCoding.selectChunks line 190
  17. lemma OAI.HyperbolicCoding.selectChunks_word line 198
  18. lemma OAI.HyperbolicCoding.chunkName_translate line 210
  19. theorem OAI.HyperbolicCoding.stationary_chunk_coupling line 220
  20. def OAI.HyperbolicCoding.productWeights line 281
  21. def OAI.HyperbolicCoding.finiteExpectation line 282
  22. lemma OAI.HyperbolicCoding.productWeights_sum line 285
  23. lemma OAI.HyperbolicCoding.productWeights_nonneg line 292
  24. lemma OAI.HyperbolicCoding.expectation_product line 295
  25. lemma OAI.HyperbolicCoding.product_one_coordinate line 302
  26. lemma OAI.HyperbolicCoding.expectation_coordinate line 306
  27. lemma OAI.HyperbolicCoding.expectation_distinct_coordinates line 320
  28. lemma OAI.HyperbolicCoding.finiteExpectation_add line 341
  29. lemma OAI.HyperbolicCoding.finiteExpectation_sub line 344
  30. lemma OAI.HyperbolicCoding.finiteExpectation_const line 347
  31. lemma OAI.HyperbolicCoding.finiteExpectation_smul line 349
  32. lemma OAI.HyperbolicCoding.finiteExpectation_sum line 355
  33. lemma OAI.HyperbolicCoding.finiteExpectation_mono line 359
  34. lemma OAI.HyperbolicCoding.MatrixCoupling.symm_cost line 373
  35. theorem OAI.HyperbolicCoding.MatrixCoupling.exists_power line 383
  36. lemma OAI.HyperbolicCoding.symbolCost_comm line 432
  37. lemma OAI.HyperbolicCoding.nameCost_comm line 435
  38. lemma OAI.HyperbolicCoding.coupling_of_observation_lawClose line 438
  39. theorem OAI.HyperbolicCoding.chunk_process_transport line 455