SelectedNaturalFinalContradiction.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The original final comparison from explicit prime-range data

theorem OAI.Ostmann.selected_natural_final_contradiction line 15

Source documentation

The final second-moment estimate has no assumed energy or pair bound. The two thresholds are uniform over the growing word and constituent lists.

theorem selected_natural_final_contradiction {I : Type u} [Fintype I]
    (role : I → CopyScheduleRole) (n Aw Kr : ℕ) (s C S H z α β γ c : ℝ)
    (hs : 0 ≤ s) (hC : 0 ≤ C) (hS : 1 ≤ S) (hH : 0 ≤ H) (hz : 0 ≤ z)
    (hα : 0 < α) (hαβ : α < β) (hγβ : γ < β) (hc : 0 < c)
    (ψ : 𝓢(ℝ, ℂ)) (hreal : ∀ y, conj (ψ y) = ψ y)
    (C₀ K d ε : ℝ) (hd : 0 ≤ d) (hε : 0 < ε)
    (B₁ Cfinal : ℝ) (hB₁ : 0 ≤ B₁)
    (hentropy : Cfinal + (d + 1) + 2 * B₁ + 1 ≤ (n : ℝ) * Real.log 2 - 1)
    (hψ : SchwartzMap.seminorm ℝ 0 0 (𝓕 ψ : 𝓢(ℝ, ℂ)) ≤ Real.exp K) :
    ∃ M₀ : ℝ, ∀ᶠ L : ℝ in atTop,
    ∀ (size : I → ℕ) (Smax : ℕ) (_hSmax : 1 ≤ Smax) (_hsize : ∀ i, size i ≤ Smax)
      (M : ℝ) (_hM₀ : M₀ ≤ M) (_hm : 0 ≤ M) (_hmL : M ≤ z * L) (_hSm : (Smax : ℝ) ≤ s * (1 + M)),
…

Mentions: OAI.Ostmann.CopyScheduleRole