OAI/Probability/LatticePassage/ResamplingMoment.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CompanionFPP.upwardResampling line 10
2. lemma OAI.CompanionFPP.measurable_upwardResampling line 16
3. lemma OAI.CompanionFPP.upwardResampling_le line 22
4. theorem OAI.CompanionFPP.upwardResampling_lmoment_le line 38
5. theorem OAI.CompanionFPP.sum_upwardResampling_lmoment line 62