claimroutine

Choose F_0 so nu/F_0 is small

Picks F0>2/θF_0>2/\theta so that ν/F0<ε0/3\nu/F_0<\varepsilon_0/3
first third of the error budget
Claim·§4 Choice of parameters and proof of Theorem~thm:main·inside thmIrrationality exponent of pi is 2

Statement (paper)

Fix ν>2\nu>2 and suppose that there are arbitrarily large positive integers qq for which some p∈Zp\in\ZZ satisfies ∣π−pq∣≤q−ν\left|\pi-\frac pq\right|\le q^{-\nu}. Then, with θ,A,B,C,η,g\theta,A,B,C,\eta,g fixed from Lemma  and ε0=min⁡(g/2,1/2)\varepsilon_0=\min(g/2,1/2), one can choose F0>2/θF_0>2/\theta so large that ν/F0<ε0/3\nu/F_0<\varepsilon_0/3.

In plain English

Assume, for a fixed ν>2\nu>2, that arbitrarily large qq admit pp with ∣π−p/q∣≤q−ν|\pi-p/q|\le q^{-\nu}. With the constants θ,A,B,C,η,g\theta,A,B,C,\eta,g from the parameter lemma and ε0=min⁡(g/2,1/2)\varepsilon_0=\min(g/2,1/2), one can pick F0>2/θF_0>2/\theta large enough that ν/F0<ε0/3\nu/F_0<\varepsilon_0/3.

Why it's here

This sets the first parameter in the contradiction argument, by which the ν/F0\nu/F_0 term of the total error becomes a small fraction of the margin ε0\varepsilon_0, which is positive because g>0g>0. The later claims on dimension, weights and the combined error margin build on this choice of F0F_0.
Classified routine:
Follows directly from the positivity of \varepsilon_0 supplied by Lemma : choosing F_0>\max\{2/\theta,3\nu/\varepsilon_0\} gives both inequalities.

Uses

lemExistence of admissible parameters for exponent nu

Used by

claimDimension choice makes errors small, savings largeclaimApproximants chosen with center-independent weight thresholdsclaimCombined error margins contradict determinant comparison

Sources

PaperOpen
Section
§4 Choice of parameters and proof of Theorem~thm:main
Page
—
Label
—
Line
sections/conclusion.tex:55
Leannot aligned

Phase 2 aligns this node to a Lean declaration.