OAI/NumberTheory/DirichletL/Moments/FirstMixedRightTransport.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentFirstMixedRightTransport.swapIndex line 20
2. lemma OAI.SevenEighths.CenteredMomentFirstMixedRightTransport.swapIndex_val line 26
3. def OAI.SevenEighths.CenteredMomentFirstMixedRightTransport.swapSubset line 29
4. lemma OAI.SevenEighths.CenteredMomentFirstMixedRightTransport.swapSubset_product line 32
5. lemma OAI.SevenEighths.CenteredMomentFirstMixedRightTransport.swapSubset_generator line 36
6. lemma OAI.SevenEighths.CenteredMomentFirstMixedRightTransport.swapSubset_inactive line 42
7. lemma OAI.SevenEighths.CenteredMomentFirstMixedRightTransport.swapped_modulus_factor line 64
8. theorem OAI.SevenEighths.CenteredMomentFirstMixedRightTransport.right_modulus line 71
9. lemma OAI.SevenEighths.CenteredMomentFirstMixedRightTransport.nominal_swap line 80
10. lemma OAI.SevenEighths.CenteredMomentFirstMixedRightTransport.nominalLog_swap line 87
11. theorem OAI.SevenEighths.CenteredMomentFirstMixedRightTransport.right_main_saving line 92
12. theorem OAI.SevenEighths.CenteredMomentFirstMixedRightTransport.right_error_saving line 107