OAI/Analysis/BernoulliCone/ExteriorCalibration.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Bernoulli.DeSilvaJerison.upperFamily_outer_gradient line 10
2. theorem OAI.Bernoulli.DeSilvaJerison.upperCalibration_outer_affine line 38

   Source documentation

   On the actual exterior branch the inverse leaf parameter cancels completely. The calibration extends affinely to the lower graph; there is no cube-root singularity in the field itself.

   theorem upperCalibration_outer_affine {p:Space 7×ℝ} (hp:U p.1<p.2)
       (hq:(upperParameter p.1 p.2)^2<Cylindrical.radiusSq axis p.1) :
       upperCalibration p=κ • gradient Zsigned p.1+
         ((p.2-κ*Zsigned p.1)/KSup p.1) • gradient KSup p.1 := by
   …

   Mentions: OAI.Bernoulli.DeSilvaJerison.p, OAI.Bernoulli.Space, OAI.Bernoulli.DeSilvaJerison.U, OAI.Bernoulli.DeSilvaJerison.upperParameter, OAI.Bernoulli.Cylindrical.radiusSq, OAI.Bernoulli.DeSilvaJerison.axis, OAI.Bernoulli.DeSilvaJerison.upperCalibration, OAI.Bernoulli.DeSilvaJerison.κ, OAI.Bernoulli.DeSilvaJerison.Zsigned, OAI.Bernoulli.DeSilvaJerison.KSup