OAI/NumberTheory/GaussianMoat/Information.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.GaussianMoat.FinLaw.mix_map_left line 15
  2. lemma OAI.GaussianMoat.FinLaw.mix_assoc line 26
  3. lemma OAI.GaussianMoat.FinLaw.joint_observation line 37
  4. lemma OAI.GaussianMoat.FinLaw.joint_associate line 42
  5. structure OAI.GaussianMoat.ForwardKernel line 53
  6. def OAI.GaussianMoat.addOffsets line 57
  7. def OAI.GaussianMoat.ForwardKernel.then line 60
  8. def OAI.GaussianMoat.differenceKernel line 65
  9. def OAI.GaussianMoat.smoothingKernel line 70
  10. def OAI.GaussianMoat.commonSchedule line 74
  11. lemma OAI.GaussianMoat.commonSchedule_bound line 77
  12. lemma OAI.GaussianMoat.commonSchedule_cons line 85
  13. def OAI.GaussianMoat.TimeLaw.advance line 88
  14. lemma OAI.GaussianMoat.ForwardKernel.displacement_entropy line 92
  15. lemma OAI.GaussianMoat.TimeLaw.advance_displacement_entropy line 103
  16. lemma OAI.GaussianMoat.entropy_step_deficit line 115
  17. theorem OAI.GaussianMoat.TimeLaw.step_deficit line 140
  18. lemma OAI.GaussianMoat.deficit_iteration line 156
  19. lemma OAI.GaussianMoat.FinLaw.joint_observation_fun line 174
  20. lemma OAI.GaussianMoat.FinLaw.mix_comm line 178
  21. lemma OAI.GaussianMoat.TimeLaw.advance_difference line 192
  22. def OAI.GaussianMoat.FinLaw.cIf line 217
  23. lemma OAI.GaussianMoat.FinLaw.cIf_nonneg line 220
  24. lemma OAI.GaussianMoat.FinLaw.cIf_comm line 223
  25. lemma OAI.GaussianMoat.FinLaw.cIf_le_cHf line 235
  26. lemma OAI.GaussianMoat.FinLaw.cIf_le_Hf line 241
  27. lemma OAI.GaussianMoat.FinLaw.cIf_chain line 246
  28. lemma OAI.GaussianMoat.FinLaw.cIf_conditioning_cost line 261
  29. theorem OAI.GaussianMoat.FinLaw.cIf_transport line 287
  30. lemma OAI.GaussianMoat.FinLaw.cHf_eq_conditionOn line 317
  31. theorem OAI.GaussianMoat.SplitSieve.pointEntropy_shift line 335
  32. lemma OAI.GaussianMoat.residue_observation_shift line 360