OAI/NumberTheory/DukePrimeDegree/Geometry/RootPrefixCompatibility.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Compatible normalized restrictions of remaining-root box kernels

  1. lemma OAI.DukePrimeDegree.RootPrefixBox.coordinateMeasure_apply line 18
  2. def OAI.DukePrimeDegree.RootPrefixBox.shrink line 34
  3. theorem OAI.DukePrimeDegree.RootPrefixBox.shrink_coordinateMeasure line 42
  4. theorem OAI.DukePrimeDegree.RootPrefixBox.shrink_conditionalKernel line 56
  5. theorem OAI.DukePrimeDegree.RootPrefixBox.shrink_marginal line 69
  6. lemma OAI.DukePrimeDegree.RootPrefixBox.shrink_marginal_absolutelyContinuous line 79
  7. lemma OAI.DukePrimeDegree.RootPrefixBox.shrink_marginal_ae_anchor_pos line 88
  8. theorem OAI.DukePrimeDegree.RootPrefixBox.overlap_anchorNormalize line 100
  9. theorem OAI.DukePrimeDegree.RootPrefixBox.overlap_anchorNormalize_restrict line 130
  10. lemma OAI.DukePrimeDegree.RootPrefixBox.shrink_full_time_marginal line 143
  11. theorem OAI.DukePrimeDegree.RootPrefixBox.base_overlap_anchorNormalize line 155
  12. theorem OAI.DukePrimeDegree.RootPrefixBox.base_anchor_restrict line 179
  13. theorem OAI.DukePrimeDegree.RootPrefixBox.base_overlap_restrict line 199