OAI/Probability/SKRatio/Dynamics/Propagation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKRatio.Calculus.backward_observable_hasDerivAt line 14
2. lemma OAI.SKRatio.Calculus.semigroup_subsolution_comparison line 37
3. lemma OAI.SKRatio.Calculus.gradient_flow_hasDerivAt line 58
4. lemma OAI.SKRatio.Calculus.gradient_comparison_of_drift line 66
5. lemma OAI.SKRatio.Calculus.gradient_envelope_of_drift line 76
6. lemma OAI.SKRatio.Calculus.semigroup_subsolution_small_set line 89
7. lemma OAI.SKRatio.Calculus.unweightedGradient_nonneg line 213
8. theorem OAI.SKRatio.Calculus.gradient_propagation_small_set line 217
9. lemma OAI.SKRatio.Calculus.tanh_mono line 236
10. lemma OAI.SKRatio.Calculus.gradientWeight_exp_lower line 240
11. lemma OAI.SKRatio.Calculus.unweightedGradient_le_exp_weighted line 262
12. lemma OAI.SKRatio.Calculus.field_gradient_expectation line 280
13. lemma OAI.SKRatio.Calculus.backward_gradient_propagation line 309
14. lemma OAI.SKRatio.Calculus.energy_comparison_from_gradient line 337
15. theorem OAI.SKRatio.Calculus.smoothing_of_small_set_gradient line 380