OAI/Analysis/BernoulliCone/HalfspaceDifferential.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Bernoulli.Halfspace.squareQuotient_hasFDerivAt line 13
2. lemma OAI.Bernoulli.Halfspace.potential_gradient line 36
3. lemma OAI.Bernoulli.Halfspace.potential_nonneg line 47
4. lemma OAI.Bernoulli.Halfspace.potential_pos line 48
5. lemma OAI.Bernoulli.Halfspace.weightedQuotient_directional line 53
6. lemma OAI.Bernoulli.Halfspace.radial_outer_identity line 70