ArithmeticContradiction.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.WeakPinned.sequence_bounded_subsequence line 13

theorem OAI.WeakPinned.arithmetic_sequence_impossible line 37

Source documentation

Both alternatives of the genuine arithmetic sequence have been eliminated.

theorem arithmetic_sequence_impossible
    (G : ∀ j,Core.Fibers (V j) (I j)) (θ γ c : ℝ) (η : ℕ → ℝ)
    (Z₁ Z₂ : ∀ j,V j → K j) (h₁ : ∀ j,Function.Injective (Z₁ j)) (h₂ : ∀ j,Function.Injective (Z₂ j))
    (hθ : 0<θ) (hγ : 0<γ) (hγ1 : γ<1) (hc : 0<c) (hcγ : c<γ)
    (hn : Tendsto (fun j => (Fintype.card (V j):ℝ)) atTop atTop)
    (hη : Tendsto η atTop (𝓝 0)) (hη0 : ∀ j,0≤η j) (hηb : ∀ j,η j≤θ/2)
    (hG : ∀ j,PreparedGraph (V j) (I j) (G j) θ γ c (η j))
    (t : ∀ j,I j → K j) (ht : ∀ j e y,y∈(G j).targets e →
      (Z₁ j ((G j).source e)-Z₁ j y)*(Z₂ j ((G j).source e)-Z₂ j y)=t j e) : False := by
…

Mentions: OAI.WeakPinned.Core.Fibers, OAI.WeakPinned.PreparedGraph