OAI/Analysis/BernoulliCone/UpperLimits.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Bernoulli.DeSilvaJerison.p_eq_max_f line 11
  2. lemma OAI.Bernoulli.DeSilvaJerison.U_eq_signed_pospart line 19
  3. lemma OAI.Bernoulli.DeSilvaJerison.upperFamily_outer_formula line 25
  4. lemma OAI.Bernoulli.DeSilvaJerison.upperFamily_tendsto_zero_off_axis line 37
  5. lemma OAI.Bernoulli.DeSilvaJerison.U_zero_of_radiusSq_zero line 48
  6. lemma OAI.Bernoulli.DeSilvaJerison.smoothCap_pos_zero line 60
  7. lemma OAI.Bernoulli.DeSilvaJerison.smoothCap_le_at_zero line 67
  8. lemma OAI.Bernoulli.DeSilvaJerison.upperFamily_axis_bound line 78
  9. lemma OAI.Bernoulli.DeSilvaJerison.upperFamily_tendsto_zero line 83