ProperPositiveSupport.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The finite-family argument in Lemma 7.6 of paper 082-03.

theorem OAI.HarmonicArtin.ParabolicIntersections.proper_positive_support line 13

Source documentation

Common positive extensions preserving a bound, together with the absence of infinitely many complete passes, give one common proper support for all permitted continuations of a suitable endpoint.

theorem proper_positive_support
    (cancel : ∀ a b c : PositiveArtin M, a*c=b*c → a=b)
    (P : PositiveArtin M → Prop) (hOne : P 1)
    (hcommon : ∀ F : Finset (PositiveArtin M), (∀ a ∈ F, P a) →
      ∃ c, P c ∧ ∀ a ∈ F, ∃ q, c=q*a)
    (hchain : ∀ a b : ℕ → PositiveArtin M, a 0=1 → (∀ n, P (a n)) →
      (∀ n, a (n+1)=b n*a n) → (∀ n, positiveSupport M (b n)=Set.univ) → False) :
    ∃ p, P p ∧ ∃ J : Set S, J ⊂ Set.univ ∧
      ∀ b, P (b*p) → positiveSupport M b ⊆ J := by
…

Mentions: OAI.HarmonicArtin.PositiveArtin, OAI.HarmonicArtin.ParabolicIntersections.positiveSupport