OAI/Dynamics/ConditionalShuffle/InstrumentAppend.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Revealed.Instrument.base_snoc line 12
2. lemma OAI.Revealed.Instrument.weights_snoc line 21
3. lemma OAI.Revealed.Instrument.kernels_snoc line 28
4. lemma OAI.Revealed.Instrument.base_append line 35
5. lemma OAI.Revealed.Instrument.weights_append line 46
6. lemma OAI.Revealed.Instrument.kernels_append line 57
7. lemma OAI.Revealed.Instrument.realConv_assoc line 70
8. lemma OAI.Revealed.Instrument.realConv_dirac_one line 80
9. lemma OAI.Revealed.Instrument.realProduct_snoc line 84
10. lemma OAI.Revealed.Instrument.realProduct_append line 88