OAI/Analysis/BernoulliCone/SeamCalibration.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Bernoulli.DeSilvaJerison.polarGradient_span line 11
2. lemma OAI.Bernoulli.DeSilvaJerison.outerGradient_span line 16
3. lemma OAI.Bernoulli.DeSilvaJerison.cylindrical_projection line 33
4. lemma OAI.Bernoulli.DeSilvaJerison.smoothCap_gradient_at_seam line 48
5. lemma OAI.Bernoulli.DeSilvaJerison.outer_gradient_at_seam line 56
6. def OAI.Bernoulli.DeSilvaJerison.seamGradient line 63

   Source documentation

   Tangential matching gives the gradient of the one-homogeneous seam height.

   def seamGradient (x:Space 7) : Space 7 :=
   …

   Mentions: OAI.Bernoulli.Space

7. lemma OAI.Bernoulli.DeSilvaJerison.seamGradient_matching line 67
8. theorem OAI.Bernoulli.DeSilvaJerison.upperCalibration_seam line 82

   Source documentation

   The actual cap/exterior calibration has the required nonpositive seam flux. This verifies the jump, rather than inserting a comparison premise.

   theorem upperCalibration_seam {x:Space 7} (hq:Cylindrical.radiusSq axis x=1)
       (hp:0<smoothCap x) :
       ‖κ • gradient smoothCap x‖^2-‖κ • gradient outerSigned x‖^2-
         2*inner ℝ (κ • gradient smoothCap x-κ • gradient outerSigned x) (κ • seamGradient x)≤0 := by
   …

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