Numerical parameters of the density increment

The thresholds θ, η, and γ attached to an alphabet size and a density, together with their monotonicity and positivity properties.

noncomputable def DensityHalesJewett.Parameters.m₀ (k : ℕ) (δ : ℝ) : ℕ

A positive dimension selected from the density Hales--Jewett assertion when available.

Equations

• DensityHalesJewett.Parameters.m₀ k δ = if h : 0 < δ ∧ DensityHalesJewett.HasDensityHJ k then (Nat.find ⋯).succ else 1

theorem DensityHalesJewett.Parameters.m₀_pos (k : ℕ) (δ : ℝ) : 0 < m₀ k δ

theorem DensityHalesJewett.Parameters.m₀_antitone {k : ℕ} (hDHJ : HasDensityHJ k) {δ ρ : ℝ} (hδ : 0 < δ) (hδρ : δ ≤ ρ) : m₀ k ρ ≤ m₀ k δ

The selected dimension is antitone in the density threshold.

theorem DensityHalesJewett.Parameters.power_difference_mono (k : ℕ) {m n : ℕ} (hmn : m ≤ n) : ↑(k + 1) ^ m - ↑k ^ m ≤ ↑(k + 1) ^ n - ↑k ^ n

The denominator in the parameter definition grows with the selected dimension.

theorem DensityHalesJewett.Parameters.θ_denominator_pos {k : ℕ} (hk : 2 ≤ k) (δ : ℝ) : 0 < ↑(k + 1) ^ m₀ k δ - ↑k ^ m₀ k δ

The denominator defining θ is positive for every admissible alphabet and density.

noncomputable def DensityHalesJewett.Parameters.θ (k : ℕ) (δ : ℝ) : ℝ

The correlated-fibers threshold attached to an alphabet size and density.

Equations

• DensityHalesJewett.Parameters.θ k δ = δ / 4 / (↑(k + 1) ^ DensityHalesJewett.Parameters.m₀ k δ - ↑k ^ DensityHalesJewett.Parameters.m₀ k δ)

theorem DensityHalesJewett.Parameters.θ_mono_of_dhj {k : ℕ} (hk : 2 ≤ k) (hDHJ : HasDensityHJ k) {δ ρ : ℝ} (hδ : 0 < δ) (hδρ : δ ≤ ρ) : θ k δ ≤ θ k ρ

The threshold is monotone in the density parameter.

theorem DensityHalesJewett.Parameters.θ_mono {k : ℕ} (hk : 2 ≤ k) {δ ρ : ℝ} (hδ : 0 < δ) (hδρ : δ ≤ ρ) : θ k δ ≤ θ k ρ

The threshold is monotone even when the density Hales--Jewett assertion is unavailable.

theorem DensityHalesJewett.Parameters.θ_pos {k : ℕ} (hk : 2 ≤ k) {δ : ℝ} (hδ : 0 < δ) : 0 < θ k δ

noncomputable def DensityHalesJewett.Parameters.η (k : ℕ) (δ : ℝ) : ℝ

The error tolerance attached to an alphabet size and density.

Equations

• DensityHalesJewett.Parameters.η k δ = min (δ * DensityHalesJewett.Parameters.θ k δ / 48) (min (DensityHalesJewett.Parameters.θ k δ / 4) (δ / 6))

theorem DensityHalesJewett.Parameters.η_mono {k : ℕ} (hk : 2 ≤ k) {δ ρ : ℝ} (hδ : 0 < δ) (hδρ : δ ≤ ρ) : η k δ ≤ η k ρ

The error tolerance is monotone in the density parameter.

theorem DensityHalesJewett.Parameters.η_pos {k : ℕ} (hk : 2 ≤ k) {δ : ℝ} (hδ : 0 < δ) : 0 < η k δ

noncomputable def DensityHalesJewett.Parameters.γ (k : ℕ) (δ : ℝ) : ℝ

The density increment attached to an alphabet size and density.

Equations

• DensityHalesJewett.Parameters.γ k δ = min (δ * DensityHalesJewett.Parameters.η k δ ^ 2 / ↑k) (min (DensityHalesJewett.Parameters.η k δ ^ 2 / 2) (3 * DensityHalesJewett.Parameters.η k δ))

theorem DensityHalesJewett.Parameters.γ_mono {k : ℕ} (hk : 2 ≤ k) {δ ρ : ℝ} (hδ : 0 < δ) (hδρ : δ ≤ ρ) : γ k δ ≤ γ k ρ

The increment is monotone in the density parameter.

theorem DensityHalesJewett.Parameters.γ_pos {k : ℕ} (hk : 2 ≤ k) {δ : ℝ} (hδ : 0 < δ) : 0 < γ k δ

theorem DensityHalesJewett.Parameters.η_lt_θ_div_two {k : ℕ} (hk : 2 ≤ k) {δ : ℝ} (hδ : 0 < δ) : η k δ < θ k δ / 2

theorem DensityHalesJewett.Parameters.η_le_δ_div_six (k : ℕ) (δ : ℝ) : η k δ ≤ δ / 6

theorem DensityHalesJewett.Parameters.γ_le_η_sq_div_two (k : ℕ) (δ : ℝ) : γ k δ ≤ η k δ ^ 2 / 2

theorem DensityHalesJewett.Parameters.γ_le_three_mul_η (k : ℕ) (δ : ℝ) : γ k δ ≤ 3 * η k δ

theorem DensityHalesJewett.Parameters.γ_mono_lowerBound {k : ℕ} (hk : 2 ≤ k) {δ₀ : ℝ} (hδ₀ : 0 < δ₀) : 0 < γ k δ₀ ∧ ∀ (ρ : ℝ), δ₀ ≤ ρ → γ k δ₀ ≤ γ k ρ

The increment parameters can be chosen uniformly above a fixed positive density floor.

theorem DensityHalesJewett.Parameters.θ_le_one {k : ℕ} (hk : 2 ≤ k) {δ : ℝ} (hδ₁ : δ ≤ 1) : θ k δ ≤ 1

The correlated-fiber threshold is at most one in the admissible parameter range.

theorem DensityHalesJewett.Parameters.large_intersection_complement_gain {k : ℕ} (hk : 2 ≤ k) {δ : ℝ} (hδ₀ : 0 < δ) : (δ + 6 * η k δ) * (1 - θ k δ / 4) ≤ δ - 3 * η k δ

The numerical parameters turn the absolute density left outside a large intersection into the required relative density gain.