OAI/Analysis/BernoulliCone/CapGeometry.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Bernoulli.DeSilvaJerison.capH_abs line 11
2. lemma OAI.Bernoulli.DeSilvaJerison.capHP_sq_abs line 15
3. lemma OAI.Bernoulli.DeSilvaJerison.capH_boundary line 19
4. lemma OAI.Bernoulli.DeSilvaJerison.capHP_sq_boundary line 21
5. lemma OAI.Bernoulli.DeSilvaJerison.capC_pos line 23
6. lemma OAI.Bernoulli.DeSilvaJerison.capC_sq line 24
7. lemma OAI.Bernoulli.DeSilvaJerison.cap_boundary_slope_bound line 25
8. lemma OAI.Bernoulli.DeSilvaJerison.gradient_smoothCap line 37
9. theorem OAI.Bernoulli.DeSilvaJerison.smoothCap_boundary_gradient line 68

   Source documentation

   Constant free-boundary slope of the actual cylindrical cap, including the transverse axis. The result is for the genuine Euclidean gradient.

   theorem smoothCap_boundary_gradient {x:Space 7} (hx:Cylindrical.radiusSq axis x≤1)
       (hs:|Cylindrical.axis axis x/CapAlgebra.V (Cylindrical.radiusSq axis x) capB|=3/4) :
       ‖gradient smoothCap x‖^2=capC^2*(capHP (3/4))^2 := by
   …

   Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.Cylindrical.radiusSq, OAI.Bernoulli.DeSilvaJerison.axis, OAI.Bernoulli.Cylindrical.axis, OAI.Bernoulli.DeSilvaJerison.CapAlgebra.V, OAI.Bernoulli.DeSilvaJerison.capB, OAI.Bernoulli.DeSilvaJerison.smoothCap, OAI.Bernoulli.DeSilvaJerison.capC, OAI.Bernoulli.DeSilvaJerison.capHP

10. theorem OAI.Bernoulli.DeSilvaJerison.smoothCap_boundary_slope line 112