OAI/Probability/LogConcave/Sampling/Jet.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LogConcaveSampling.TimeJet.jet line 17
2. lemma OAI.LogConcaveSampling.TimeJet.smooth line 21
3. lemma OAI.LogConcaveSampling.TimeJet.hasDerivAt line 27
4. lemma OAI.LogConcaveSampling.TimeJet.eq_iteratedDeriv line 33
5. lemma OAI.LogConcaveSampling.RMSIntegral.integral_norm_sq_eq_eLpNorm line 46
6. lemma OAI.LogConcaveSampling.RMSIntegral.integral_norm_sq_le_of_eLpNorm line 55
7. lemma OAI.LogConcaveSampling.gaussian_operator_sq line 65
8. def OAI.LogConcaveSampling.terminalActionChain line 109
9. lemma OAI.LogConcaveSampling.terminalActionChain_smooth line 114
10. lemma OAI.LogConcaveSampling.terminalActionChain_hasDerivAt line 122
11. lemma OAI.LogConcaveSampling.terminalActionChain_first_zero line 137
12. theorem OAI.LogConcaveSampling.terminalActionChain_sq line 144