OAI/Analysis/BernoulliCone/UpperSeam.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Bernoulli.Cylindrical.axis_add_axis line 12
2. lemma OAI.Bernoulli.Cylindrical.radiusSq_add_axis line 15
3. lemma OAI.Bernoulli.DeSilvaJerison.cap_boundary_slope_lt line 23
4. lemma OAI.Bernoulli.DeSilvaJerison.smoothCap_boundary_slope_lt line 34
5. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.V_one line 41
6. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.D_one line 42
7. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.E_one line 43
8. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.H_one line 44
9. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Y_one line 45
10. lemma OAI.Bernoulli.DeSilvaJerison.CapAlgebra.Y1_one line 47
11. lemma OAI.Bernoulli.DeSilvaJerison.smoothCap_at_seam line 52
12. lemma OAI.Bernoulli.DeSilvaJerison.upper_seam_agreement line 55
13. lemma OAI.Bernoulli.DeSilvaJerison.outerSigned_axis_at_seam line 58
14. lemma OAI.Bernoulli.DeSilvaJerison.outerSigned_transverse_at_seam line 73
15. lemma OAI.Bernoulli.DeSilvaJerison.smoothCap_transverse_at_seam line 86
16. theorem OAI.Bernoulli.DeSilvaJerison.upper_seam_jump line 100

    Source documentation

    Actual normal derivative jump of the glued Euclidean supersolution.

    theorem upper_seam_jump {x:Space 7} (hq:Cylindrical.radiusSq axis x=1)
        (ha:|Cylindrical.axis axis x|≤3/4) :
        inner ℝ (gradient outerSigned x-gradient smoothCap x) (Cylindrical.transverse axis x)≤0 := by
    …

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