OAI/Analysis/BernoulliCone/OuterSlope.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Bernoulli.DeSilvaJerison.Zsigned_gradient line 11
2. lemma OAI.Bernoulli.DeSilvaJerison.outerSigned_gradient line 17
3. lemma OAI.Bernoulli.DeSilvaJerison.outer_zero_coefficient line 25
4. lemma OAI.Bernoulli.DeSilvaJerison.GSup_even line 34
5. lemma OAI.Bernoulli.DeSilvaJerison.GSup_abs line 37
6. lemma OAI.Bernoulli.DeSilvaJerison.outer_zero_slope line 41
7. lemma OAI.Bernoulli.DeSilvaJerison.outer_zero_angle line 56
8. theorem OAI.Bernoulli.DeSilvaJerison.outer_zero_slope_lt line 73

   Source documentation

   Strict free-boundary slope for the actual exterior function, not just its one-variable numerical certificate.

   theorem outer_zero_slope_lt {x:Space 7} (hq:1≤Cylindrical.radiusSq axis x) (hz:outerSigned x=0) :
       ‖gradient outerSigned x‖^2<c7 := by
   …

   Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.Cylindrical.radiusSq, OAI.Bernoulli.DeSilvaJerison.axis, OAI.Bernoulli.DeSilvaJerison.outerSigned, OAI.Bernoulli.DeSilvaJerison.c7