OAI/Topology/ArtinGroups/ParabolicIntersections/SphericalCommonExtension.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ParabolicIntersections.restrictedPointedFamily line 19
2. lemma OAI.HarmonicArtin.ParabolicIntersections.restrictedPointedFamily_word line 23
3. lemma OAI.HarmonicArtin.ParabolicIntersections.testUpper_eventually line 37
4. theorem OAI.HarmonicArtin.ParabolicIntersections.spherical_common_extension line 52

   Source documentation

   Lemma 7.5: a common positive left extension preserves a common bound on the total test heights. Only published admissible-folding gcd preservation is assumed; the top-test argument is proved here.

   theorem spherical_common_extension (Y : Set S) (hY : IsSpherical M Y)
       (hGcd : PublishedFoldingGcd M Y hY) (x : Artin M)
       (a b : Artin (restrictedMatrix M Y)) (t : ℤ)
       (ha : ∀ L, ClassTestUpper Q (restrictedPointedFamily M f Y x a L)
         (Set.range (unfoldedInclusion M Y)) t)
       (hb : ∀ L, ClassTestUpper Q (restrictedPointedFamily M f Y x b L)
         (Set.range (unfoldedInclusion M Y)) t) :
       ∃ p q : PositiveArtin (restrictedMatrix M Y),
         positiveToArtin _ p*a=positiveToArtin _ q*b ∧
         ∀ L, ClassTestUpper Q
           (restrictedPointedFamily M f Y x (positiveToArtin _ p*a) L)
           (Set.range (unfoldedInclusion M Y)) t := by
   …

   Mentions: OAI.HarmonicArtin.IsSpherical, OAI.HarmonicArtin.ParabolicIntersections.PublishedFoldingGcd, OAI.HarmonicArtin.Artin, OAI.HarmonicArtin.ParabolicIntersections.restrictedPointedFamily, OAI.HarmonicArtin.unfoldedInclusion, OAI.HarmonicArtin.PositiveArtin, OAI.HarmonicArtin.positiveToArtin