OAI/Probability/LogConcave/JetEstimates/JetRightSlice.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.JetCalculus.jet_right_slice_at line 16
2. lemma OAI.LogConcaveSampling.JetCalculus.timeSmooth_jet line 26
3. lemma OAI.LogConcaveSampling.JetCalculus.timeSmooth_dir line 29
4. lemma OAI.LogConcaveSampling.jointMean_timeSmooth line 34
5. lemma OAI.LogConcaveSampling.jointScore_timeSmooth line 40
6. lemma OAI.LogConcaveSampling.joint_mean_transport line 46
7. lemma OAI.LogConcaveSampling.JetCalculus.gadj_right_slice_at line 98
8. theorem OAI.LogConcaveSampling.material_mean_jet line 111
9. lemma OAI.LogConcaveSampling.JetCalculus.mdir_time_at line 208
10. lemma OAI.LogConcaveSampling.JetCalculus.mdir_time_mul_at line 220
11. lemma OAI.LogConcaveSampling.JetCalculus.hasDerivAt_inv_nat_pow line 229