OAI/Probability/GaussianPropeller/HeatMaximum.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GaussianPropeller.HeatMaximum.second_deriv_nonneg_of_localMin line 24
2. lemma OAI.GaussianPropeller.HeatMaximum.deriv_nonpos_of_min_on_left line 57
3. lemma OAI.GaussianPropeller.HeatMaximum.square_norm_difference_bound line 67
4. lemma OAI.GaussianPropeller.HeatMaximum.weighted_linear_le_quadratic line 78
5. lemma OAI.GaussianPropeller.HeatMaximum.reaction_bound line 84
6. def OAI.GaussianPropeller.HeatMaximum.deficit line 121
7. lemma OAI.GaussianPropeller.HeatMaximum.hasDerivAt_line line 124
8. lemma OAI.GaussianPropeller.HeatMaximum.min_gradient_left line 130
9. lemma OAI.GaussianPropeller.HeatMaximum.min_gradient_right line 162
10. lemma OAI.GaussianPropeller.HeatMaximum.min_hessian_diagonal line 174
11. lemma OAI.GaussianPropeller.HeatMaximum.min_laplacian_bound line 209
12. lemma OAI.GaussianPropeller.HeatMaximum.no_forbidden_minimum line 224
13. lemma OAI.GaussianPropeller.HeatMaximum.deficit_lower line 265
14. lemma OAI.GaussianPropeller.HeatMaximum.exists_negative_minimum line 294
15. lemma OAI.GaussianPropeller.HeatMaximum.deficit_coercive_radius line 335
16. lemma OAI.GaussianPropeller.HeatMaximum.heat_deficit_nonneg line 368
17. lemma OAI.GaussianPropeller.HeatMaximum.heat_concave line 416