OAI/Analysis/BernoulliCone/UpperFamily.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Bernoulli.Cylindrical.axis_smul line 12
  2. lemma OAI.Bernoulli.Cylindrical.radiusSq_smul line 14
  3. lemma OAI.Bernoulli.DeSilvaJerison.angle_smul line 20
  4. lemma OAI.Bernoulli.DeSilvaJerison.Zsigned_smul line 23
  5. lemma OAI.Bernoulli.DeSilvaJerison.KSup_smul line 26
  6. lemma OAI.Bernoulli.DeSilvaJerison.outerSigned_cylindrical line 32
  7. lemma OAI.Bernoulli.DeSilvaJerison.outer_positive_sector line 60
  8. lemma OAI.Bernoulli.DeSilvaJerison.capH_nonneg_iff line 74
  9. lemma OAI.Bernoulli.DeSilvaJerison.outer_nonnegative_sector line 82
  10. lemma OAI.Bernoulli.DeSilvaJerison.outer_nonnegative_angle line 95
  11. def OAI.Bernoulli.DeSilvaJerison.upperSigned line 111

    Source documentation

    The actual signed glued DSJ upper profile, including the symmetry axis.

    def upperSigned (x:Space 7) :ℝ := if Cylindrical.radiusSq axis x≤1 then smoothCap x else outerSigned x

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

  12. def OAI.Bernoulli.DeSilvaJerison.upperFamily line 113
  13. lemma OAI.Bernoulli.DeSilvaJerison.upperSigned_cap line 114
  14. lemma OAI.Bernoulli.DeSilvaJerison.upperSigned_outer line 115
  15. lemma OAI.Bernoulli.DeSilvaJerison.upperFamily_nonneg line 119
  16. lemma OAI.Bernoulli.DeSilvaJerison.upperSigned_continuous line 123
  17. lemma OAI.Bernoulli.DeSilvaJerison.upperFamily_continuous line 138
  18. lemma OAI.Bernoulli.DeSilvaJerison.upperFamily_joint_continuous line 143