OAI/Analysis/BernoulliCone/HalfspaceUnitSlope.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Bernoulli.Shape.small_parameter_bounds line 12
2. theorem OAI.Bernoulli.Shape.positiveLinear_minimizer_unit line 38

   Source documentation

   Domain comparisons for the actual Bernoulli energy force the unit slope of a minimizing halfspace. No boundary condition is assumed.

   theorem positiveLinear_minimizer_unit {e : Space d} (he : e ≠ 0)
       (hm : GlobalMinimizer (positiveLinear e)) : ‖e‖=1 := by
   …

   Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.GlobalMinimizer, OAI.Bernoulli.Shape.positiveLinear