MinimizerStationarity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Bernoulli.GlobalMinimizer.nonneg_of_continuous line 13
theorem OAI.Bernoulli.GlobalMinimizer.stationarity line 26
Source documentation
Compact rank-one domain variations give the Bernoulli stress identity from unrestricted Sobolev minimality, including the volume term.
```
theorem GlobalMinimizer.stationarity {u : Space d → ℝ} {L : ℝ≥0}
    (hm : GlobalMinimizer u) (huLip : LipschitzWith L u)
    {a : Space d} {R : ℝ} (hR : 0 < R)
    {φ : Space d → ℝ} (hφ : Test (ball a R) φ) (e : Space d) :
    (∫ x in ball a R, Shape.stressTerm u φ e x) = 0 := by
…
```
Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.GlobalMinimizer, OAI.Bernoulli.Test, OAI.Bernoulli.Shape.stressTerm