OAI/Analysis/BernoulliCone/HalfspaceQuotient.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   The perspective of the square, with its zero trace value.

   def squareQuotient (u : Space d → ℝ) (e : Space d) (x : Space d) : ℝ :=
   …

   Mentions: OAI.Bernoulli.Space

2. lemma OAI.Bernoulli.Halfspace.height_bound line 16
3. lemma OAI.Bernoulli.Halfspace.perspective_estimate line 31
4. lemma OAI.Bernoulli.Halfspace.squareQuotient_lipschitz line 64