OAI/Dynamics/ConditionalShuffle/Instrument.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Revealed.Instrument.fairMass_bind line 10
  2. lemma OAI.Revealed.Instrument.fairMass_snoc line 18
  3. structure OAI.Revealed.Instrument.Data line 23
  4. def OAI.Revealed.Instrument.joint line 31
  5. def OAI.Revealed.Instrument.probability line 32
  6. def OAI.Revealed.Instrument.kernel line 33
  7. lemma OAI.Revealed.Instrument.joint_nonneg line 35
  8. lemma OAI.Revealed.Instrument.probability_nonneg line 41
  9. lemma OAI.Revealed.Instrument.probability_sum line 42
  10. lemma OAI.Revealed.Instrument.kernel_nonneg line 45
  11. lemma OAI.Revealed.Instrument.kernel_sum line 46
  12. lemma OAI.Revealed.Instrument.probability_mul_kernel line 49
  13. def OAI.Revealed.Instrument.base line 52
  14. def OAI.Revealed.Instrument.weights line 56
  15. def OAI.Revealed.Instrument.kernels line 60
  16. def OAI.Revealed.Instrument.observed line 65
  17. def OAI.Revealed.Instrument.groupRun line 70
  18. def OAI.Revealed.Instrument.pathJoint line 75
  19. lemma OAI.Revealed.Instrument.kernels_nonneg line 78
  20. lemma OAI.Revealed.Instrument.kernels_sum line 87
  21. lemma OAI.Revealed.Instrument.weights_nonneg line 96
  22. lemma OAI.Revealed.Instrument.sum_snoc line 101
  23. lemma OAI.Revealed.Instrument.weights_sum line 109
  24. lemma OAI.Revealed.Instrument.snoc_eq_iff line 117
  25. lemma OAI.Revealed.Instrument.realConv_right line 125
  26. lemma OAI.Revealed.Instrument.transition_mass line 131
  27. lemma OAI.Revealed.Instrument.pathJoint_succ line 144
  28. theorem OAI.Revealed.Instrument.pathJoint_factor line 163