OAI/Analysis/AllenCahn/BernsteinGradient.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DeGiorgi.unbounded_bernstein_bound line 14
2. def OAI.DeGiorgi.linearLogGradientBound line 79
3. lemma OAI.DeGiorgi.log_gradient_bound_no_growth line 84
4. lemma OAI.DeGiorgi.linearLogGradientBound_nonneg line 144
5. lemma OAI.DeGiorgi.positive_linear_log_gradient line 149
6. lemma OAI.DeGiorgi.positive_linear_log_lipschitz line 165
7. lemma OAI.DeGiorgi.positive_linear_harnack line 182
8. lemma OAI.DeGiorgi.positive_linear_relative_gradient line 193