OAI/Topology/ArtinGroups/ParabolicIntersections/RelativePeaks.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Last occupied levels and lower-edge harmonic comparisons for the pointed family.

  1. def OAI.HarmonicArtin.ParabolicIntersections.relativePeakSupport line 11
  2. def OAI.HarmonicArtin.ParabolicIntersections.relativePeak line 14
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.relativePeakSupport_mem line 17
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.relativePeak_bound line 26
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.relativePeak_above line 30
  6. lemma OAI.HarmonicArtin.ParabolicIntersections.relativePeak_nonzero line 35
  7. lemma OAI.HarmonicArtin.ParabolicIntersections.relativePeak_positive line 44
  8. lemma OAI.HarmonicArtin.ParabolicIntersections.relativePeak_nonzero_of_pos line 52
  9. def OAI.HarmonicArtin.ParabolicIntersections.relativeLowerLevel line 60
  10. lemma OAI.HarmonicArtin.ParabolicIntersections.relativePeak_le_lowerLevel line 63
  11. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeProfile_eq_of_lower_open line 69
  12. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeProfile_lower_comparison line 87
  13. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeProfile_lower_comparison_rev line 101
  14. lemma OAI.HarmonicArtin.ParabolicIntersections.relativeProfile_eq_above_lower line 115