OAI/NumberTheory/DukePrimeDegree/Geometry/UpperRootCoordinatesMeasure.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Support and ambient null sets in upper-root coordinate measures

  1. lemma OAI.DukePrimeDegree.UpperRootBox.coordinateMeasure_ae_domain line 18
  2. lemma OAI.DukePrimeDegree.UpperRootBox.coordinateMeasure_fst_ae_transverse line 25
  3. lemma OAI.DukePrimeDegree.UpperRootBox.conditionalKernel_ae_time line 32
  4. lemma OAI.DukePrimeDegree.UpperRootBox.conditionalKernel_time_mass line 41
  5. lemma OAI.DukePrimeDegree.UpperRootBox.ae_coordinate_of_ambient line 48