Research proof index

A particular application of the determinant bound used in subcase 2.1

Proposition 2.5. The bulk of the proof is in the section NiceFactorization.

Some basic consequences of Proposition 2.5, phrased in a way that make them more useful in the proof of Proposition 2.6.

The set that we are taking the infimum over in the geometry bound is a finite set.

The union of B-sets used in the proof of proposition 2.6. -/ noncomputable def BUnion (α β γ : ℝ) {d : ℕ} (x : ℕ) (ε : ℝ) : Finset ((Fin d → ℕ) × (Fin d → ℕ) × (Fin d → ℕ) × (Fin 3 → ℕ)) := (indexSet' α β γ d x ε).sup fun ⟨r, s, t, c⟩ ↦ B_finset d c (fun i ↦ 2^r i) (fun i ↦ 2^s i) (fun i ↦ 2^t i) theorem similar_pow_log {x : ℕ} (hx : 0 < x) : x ~ 2 ^ Na...

The value of d chosen in proposition 2.6 -/ noncomputable def d (ε : ℝ) : ℕ := ⌊10 * ε⁻¹ ^ 4⌋₊ /- Proposition 2.7. Reformulated slightly in terms of the existence of a Finset whose elements have certain properties. As it stands the statement in the blueprint implicitly assumes that this Finset is nonempty. That might be true, but is rather annoying...