OAI/NumberTheory/DukePrimeDegree/Geometry/RootPrefixSupport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Supports of actual remaining-root conditional kernels

  1. lemma OAI.DukePrimeDegree.RootPrefixBox.coordinateMeasure_ae_domain line 17
  2. lemma OAI.DukePrimeDegree.RootPrefixBox.coordinateMeasure_fst_ae_transverse line 24
  3. lemma OAI.DukePrimeDegree.RootPrefixBox.conditionalKernel_ae_time line 31
  4. lemma OAI.DukePrimeDegree.RootPrefixBox.conditionalKernel_time_mass line 40