OAI/Analysis/AffineBernstein/JointTubeMetrics.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.AffineBernstein.dirDeriv_prod_left line 20
  2. lemma OAI.AffineBernstein.flatInverseTrace_prod_left line 27
  3. lemma OAI.AffineBernstein.flatInversePair_prod_left line 35
  4. def OAI.AffineBernstein.tubeBasePair line 43
  5. def OAI.AffineBernstein.tubeBaseTrace line 46
  6. def OAI.AffineBernstein.tubeAngularPair line 49
  7. def OAI.AffineBernstein.tubeAngularTrace line 55
  8. lemma OAI.AffineBernstein.contDiffAt_tubeBasePair line 61
  9. lemma OAI.AffineBernstein.contDiffAt_tubeBaseTrace line 72
  10. lemma OAI.AffineBernstein.continuousAt_tubeMeasureDensity line 83
  11. lemma OAI.AffineBernstein.continuousOn_tubeAngularPair line 92
  12. lemma OAI.AffineBernstein.continuousOn_tubeAngularTrace line 107