OAI/Probability/SKSupport/Diffusion/TerminalShapes.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ZeroTemperatureSK.Heat.tanhDrift line 12
2. lemma OAI.ZeroTemperatureSK.Heat.tanh_scaled_derivative line 14
3. lemma OAI.ZeroTemperatureSK.Heat.tanhDrift_derivative line 19
4. lemma OAI.ZeroTemperatureSK.Heat.tanhDrift_second line 23
5. lemma OAI.ZeroTemperatureSK.Heat.tanhDrift_rate line 31
6. lemma OAI.ZeroTemperatureSK.Heat.tanhDrift_wronskian line 38
7. lemma OAI.ZeroTemperatureSK.Heat.tanh_sq_gap_pos line 54
8. lemma OAI.ZeroTemperatureSK.Heat.tanh_nonneg_of_nonneg line 58
9. lemma OAI.ZeroTemperatureSK.Heat.tanhDrift_initial_signs line 62
10. lemma OAI.ZeroTemperatureSK.Heat.gaussianBurgers_terminal line 81
11. lemma OAI.ZeroTemperatureSK.Heat.gaussianBurgers_softAbs_terminal line 88