Qualities of tuples and sets of tuples

noncomputable def tupleQuality {n : ℕ} (a : Fin n → ℤ) : ENNReal

The quality of a single tuple. This depends on Lean defining log -x = log x for all real x.

Equations

• tupleQuality a = ENNReal.ofReal (Real.log ↑(maxAbs a) / Real.log ↑(UniqueFactorizationMonoid.radical (∏ i : Fin n, a i)))

noncomputable def quality {n : ℕ} (A : Set (Fin n → ℤ)) : ENNReal

The quality of a set of tuples, defined as the infimum of those numbers where only finitely many tuples in the set have a strictly higher quality.

Equations

• quality A = sInf {q : ENNReal | {a : Fin n → ℤ | a ∈ A ∧ q < tupleQuality a}.Finite}

theorem quality_mono {n : ℕ} {A B : Set (Fin n → ℤ)} (h : A ⊆ B) : quality A ≤ quality B

theorem quality_le_of_finite {n : ℕ} {A : Set (Fin n → ℤ)} {q : ENNReal} (hq : {a : Fin n → ℤ | a ∈ A ∧ q < tupleQuality a}.Finite) : quality A ≤ q

theorem quality_finite {n : ℕ} {A : Set (Fin n → ℤ)} (hA : A.Finite) : quality A = 0

theorem quality_empty {n : ℕ} : quality ∅ = 0

theorem quality_union_finite {n : ℕ} {A B : Set (Fin n → ℤ)} (h : B.Finite) : quality (A ∪ B) = quality A

theorem quality_ge_of_liminf {n : ℕ} {A : Set (Fin n → ℤ)} {q : ENNReal} (f : ℕ → Fin n → ℤ) (s : Set ℕ) (infs : s.Infinite) (injs : Set.InjOn f s) (ms : ∀ i ∈ s, f i ∈ A) (qf : q ≤ Filter.liminf (tupleQuality ∘ f) Filter.atTop) : q ≤ quality A

theorem quality_ge_of_liminf_univ {n : ℕ} {A : Set (Fin n → ℤ)} {q : ENNReal} (f : ℕ ↪ Fin n → ℤ) (ms : ∀ (i : ℕ), f i ∈ A) (qf : q ≤ Filter.liminf (tupleQuality ∘ ⇑f) Filter.atTop) : q ≤ quality A

A specialisation of quality_ge_of_liminf to s = univ.