OAI/Probability/LogConcave/OraclePrograms/SlotTransformAddShift.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.SeedCompiler.slotTransform_add_shift line 17
2. lemma OAI.LogConcaveSampling.SeedCompiler.slotTransform_scalar_mul line 27
3. lemma OAI.LogConcaveSampling.SeedCompiler.inverse_shift_identity line 39
4. lemma OAI.LogConcaveSampling.SeedCompiler.inverse_shift_energy line 49
5. lemma OAI.LogConcaveSampling.SeedCompiler.measurable_slotTransform line 58
6. theorem OAI.LogConcaveSampling.SeedCompiler.transformed_mean_equivariant line 63