OAI/Analysis/BiholderTransport/Calculus/TrueCenterJet.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.WeakMTWTransport.TrueCenterJet line 24
2. def OAI.WeakMTWTransport.TrueCenterJet.fullRay line 45
3. def OAI.WeakMTWTransport.TrueCenterJet.shortRay line 47
4. def OAI.WeakMTWTransport.TrueCenterJet.matrix line 50
5. def OAI.WeakMTWTransport.TrueCenterJet.curvature line 53
6. lemma OAI.WeakMTWTransport.exists_true_center_jet_gain line 57
7. lemma OAI.WeakMTWTransport.TrueCenterJet.det_pos line 75