OAI/Topology/ArtinGroups/ParabolicIntersections/RelativeHeight.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

The relative harmonic height

The finite-support, highest-level-first height of §6.2 of paper 082-03. The last coordinate is the full closed-type sign mask. The cutoff is an arbitrary integer; null signs can occur at the cutoff itself.

  1. def OAI.HarmonicArtin.ParabolicIntersections.relativeSign line 20
  2. def OAI.HarmonicArtin.ParabolicIntersections.relativeSignMask line 23
  3. abbrev OAI.HarmonicArtin.ParabolicIntersections.RelativeBlock line 27
  4. def OAI.HarmonicArtin.ParabolicIntersections.relativeBlock line 30
  5. def OAI.HarmonicArtin.ParabolicIntersections.relativeZeroBlock line 34
  6. def OAI.HarmonicArtin.ParabolicIntersections.RelativeBlockOccurs line 36
  7. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeSignMask_bounds line 39
  8. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeBlock_of_vector_zero line 44
  9. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeZeroBlock_le line 56
  10. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeBlock_bounded_finite line 73
  11. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeBlock_predecessors_finite line 89
  12. def OAI.HarmonicArtin.ParabolicIntersections.relativeBlockRank line 95
  13. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeBlockRank_strictMono line 98
  14. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeBlockRank_eq_iff line 106
  15. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeBlockRank_lt_iff line 119
  16. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeBlockRank_zero line 130
  17. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeBlockRank_support_finite line 140
  18. def OAI.HarmonicArtin.ParabolicIntersections.relativeHeight line 149
  19. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeHeight_eq_blocks line 154
  20. theorem OAI.HarmonicArtin.ParabolicIntersections.relativeHeight_wellFounded line 160