OAI/Geometry/CAT0Fillings/Chord/Bubble.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CAT0Fillings.Conformal.averageProfile_bound line 11
  2. lemma OAI.CAT0Fillings.Conformal.averageProfile_deriv_bound line 18
  3. lemma OAI.CAT0Fillings.Conformal.averageProfile_identity line 27
  4. def OAI.CAT0Fillings.Conformal.chordBubble line 59
  5. def OAI.CAT0Fillings.Conformal.chordBubbleD line 60
  6. def OAI.CAT0Fillings.Conformal.chordBubbleDD line 61
  7. lemma OAI.CAT0Fillings.Conformal.chordBubble_contDiff line 63
  8. lemma OAI.CAT0Fillings.Conformal.chordBubbleD_contDiff line 67
  9. lemma OAI.CAT0Fillings.Conformal.chordBubble_hasDerivAt line 72
  10. lemma OAI.CAT0Fillings.Conformal.chordBubbleD_hasDerivAt line 80
  11. lemma OAI.CAT0Fillings.Conformal.chordBubble_pos line 90
  12. lemma OAI.CAT0Fillings.Conformal.chordBubble_le_one line 92