OAI/Analysis/BernoulliCone/CylindricalCalculus.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Bernoulli.Cylindrical.axis line 15
2. def OAI.Bernoulli.Cylindrical.transverse line 16
3. def OAI.Bernoulli.Cylindrical.radiusSq line 17
4. theorem OAI.Bernoulli.Cylindrical.transverse_inner line 20
5. theorem OAI.Bernoulli.Cylindrical.transverse_sq line 23
6. lemma OAI.Bernoulli.Cylindrical.radiusSq_nonneg line 28
7. lemma OAI.Bernoulli.Cylindrical.axis_contDiff line 31
8. lemma OAI.Bernoulli.Cylindrical.radiusSq_contDiff line 32
9. lemma OAI.Bernoulli.Cylindrical.gradient_axis line 34
10. lemma OAI.Bernoulli.Cylindrical.gradient_norm_sq line 41
11. lemma OAI.Bernoulli.Cylindrical.laplacian_axis line 49
12. lemma OAI.Bernoulli.Cylindrical.laplacian_norm_sq line 57
13. lemma OAI.Bernoulli.Cylindrical.gradient_radiusSq line 69
14. lemma OAI.Bernoulli.Cylindrical.laplacian_radiusSq line 84
15. def OAI.Bernoulli.Cylindrical.lift line 97

    Source documentation

    A smooth cylindrical cap, expressed using the squared transverse radius so that the symmetry axis is included without a singular-coordinate convention.

    def lift (e:E) (y k h:ℝ→ℝ) (x:E) : ℝ := y (radiusSq e x)*h (axis e x*k (radiusSq e x))

    Mentions: OAI.Bernoulli.Cylindrical.radiusSq, OAI.Bernoulli.Cylindrical.axis

16. lemma OAI.Bernoulli.Cylindrical.contDiffAt_lift line 98
17. lemma OAI.Bernoulli.Cylindrical.gradient_lift line 104
18. lemma OAI.Bernoulli.Cylindrical.laplacian_lift line 125