OAI/Analysis/BernoulliCone/PositiveQuotient.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Bernoulli.Halfspace.positiveSquareRatio line 13

   Source documentation

   The square perspective on the nonnegative cone, with its zero value at zero denominator. Used on actual admissible Lipschitz variations.

   def positiveSquareRatio (v u : Space d → ℝ) (x : Space d) : ℝ :=
   …

   Mentions: OAI.Bernoulli.Space

2. lemma OAI.Bernoulli.Halfspace.positiveSquareRatio_nonneg line 16
3. lemma OAI.Bernoulli.Halfspace.positiveSquareRatio_bound line 22
4. lemma OAI.Bernoulli.Halfspace.positiveSquareRatio_lipschitz line 34