OAI/Dynamics/StandardMap/Coupling/IidFiniteWindowApprox.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HyperbolicCoding.centeredWindow line 14
  2. lemma OAI.HyperbolicCoding.measurable_centeredWindow line 16
  3. lemma OAI.HyperbolicCoding.centeredWindow_comap_monotone line 20
  4. lemma OAI.HyperbolicCoding.centeredWindow_generates line 36
  5. lemma OAI.HyperbolicCoding.centeredWindow_as_word line 65
  6. theorem OAI.HyperbolicCoding.iid_finite_window_approx line 71
  7. lemma OAI.HyperbolicCoding.mass_comp_factor line 88
  8. lemma OAI.HyperbolicCoding.rate_of_factor line 96
  9. theorem OAI.HyperbolicCoding.relative_iid_window_graph line 119
  10. theorem OAI.HyperbolicCoding.coupling_step_finite line 182
  11. lemma OAI.HyperbolicCoding.cond_constant line 270
  12. lemma OAI.HyperbolicCoding.lawClose_of_mutual_information line 279
  13. lemma OAI.HyperbolicCoding.lawClose_entropy_budget line 297
  14. def OAI.HyperbolicCoding.sequenceEntropyDefect line 310
  15. lemma OAI.HyperbolicCoding.obs_finiteName_zero line 313
  16. lemma OAI.HyperbolicCoding.sequenceEntropyDefect_cons line 321
  17. lemma OAI.HyperbolicCoding.independentNameWeights_cons_finite line 341
  18. lemma OAI.HyperbolicCoding.mass_equiv_inverse_finite line 353
  19. theorem OAI.HyperbolicCoding.entropy_product_transport line 362
  20. theorem OAI.HyperbolicCoding.sequential_coupling_budgets line 432
  21. lemma OAI.HyperbolicCoding.finiteName_entropy_chain line 498