ConstituentFinalPairDecay.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The original final pair decays from explicit prime and history bounds

theorem OAI.Ostmann.eventual_constituent_final_pair_decay line 17

Source documentation

The threshold is uniform over the growing constituent coordinate space. The ranged-character error and the discarded prime guards are both derived from the stated scalar size bounds.

theorem eventual_constituent_final_pair_decay
    (n : ℕ) (a₀ b₀ d₀ C S H z α₀ β γ c : ℝ)
    (ha₀ : 0 ≤ a₀) (hb₀ : 0 ≤ b₀) (hd₀ : 0 ≤ d₀) (hC : 0 ≤ C) (hS : 1 ≤ S)
    (hH : 0 ≤ H) (hz : 0 ≤ z)
    (hα₀ : 0 < α₀) (hαβ : α₀ < β) (hγβ : γ < β) (hc : 0 < c) :
    ∀ᶠ L : ℝ in atTop,
    ∀ (I : Type u) [Fintype I] (role : I → CopyScheduleRole) (size : I → ℕ)
      (χ : (Σ i, Fin (size i)) → ∀ p : ℕ, DirichletCharacter ℂ p)
      (κ : (Σ i, Fin (size i)) → ℕ → ℂ) (pivot : ℕ → (Σ i, Fin (size i)))
      (_hκ : ∀ i p, ‖κ i p‖ ≤ 1)
      (e : Equiv.Perm (SurvivingConstituent role size n))
      (_hχ : ∀ i, χ (copyScheduleOrigin n (e i).val) = χ (copyScheduleOrigin n i.val))
…

Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.SurvivingConstituent, OAI.Ostmann.copyScheduleOrigin