OAI/NumberTheory/DukePrimeDegree/Geometry/UpperRootRestrictions.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Compatible restrictions of full upper-root conditionals

Shrinking an actual upper-root quotient box restricts its coordinate measure. The disintegrated kernels therefore agree projectively on intersections, with the normalization fixed by a common smaller box.

  1. lemma OAI.DukePrimeDegree.UpperRootBox.coordinateMeasure_apply line 23
  2. def OAI.DukePrimeDegree.UpperRootBox.shrink line 39
  3. theorem OAI.DukePrimeDegree.UpperRootBox.shrink_coordinateMeasure line 47
  4. theorem OAI.DukePrimeDegree.UpperRootBox.shrink_conditionalKernel line 61
  5. theorem OAI.DukePrimeDegree.UpperRootBox.shrink_marginal line 74
  6. lemma OAI.DukePrimeDegree.UpperRootBox.shrink_marginal_absolutelyContinuous line 84
  7. lemma OAI.DukePrimeDegree.UpperRootBox.shrink_marginal_ae_anchor_pos line 93
  8. theorem OAI.DukePrimeDegree.UpperRootBox.overlap_anchorNormalize line 105
  9. theorem OAI.DukePrimeDegree.UpperRootBox.overlap_anchorNormalize_restrict line 135
  10. lemma OAI.DukePrimeDegree.UpperRootBox.shrink_full_time_marginal line 148
  11. theorem OAI.DukePrimeDegree.UpperRootBox.base_overlap_anchorNormalize line 160
  12. theorem OAI.DukePrimeDegree.UpperRootBox.base_anchor_restrict line 184
  13. theorem OAI.DukePrimeDegree.UpperRootBox.base_overlap_restrict line 204