Occurrence-preserving canonical box profiles

Profiles are sorted multisets of labels, not sets of labels. Distinct prime sets with the same multiplicities give the same profile.

noncomputable def MathlibNt.SieveTheory.LiLiuPrereqWF.boxProfile (label : ℕ → ℕ) (S : Finset ℕ) : List ℕ

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.boxProfile label S = (Multiset.map label S.val).sort fun (x1 x2 : ℕ) => x1 ≥ x2

@[simp]

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.boxProfile_length (label : ℕ → ℕ) (S : Finset ℕ) : (boxProfile label S).length = S.card

@[simp]

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.mem_boxProfile (label : ℕ → ℕ) (S : Finset ℕ) (j : ℕ) : j ∈ boxProfile label S ↔ ∃ p ∈ S, label p = j

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.boxProfile_count (label : ℕ → ℕ) (S : Finset ℕ) (j : ℕ) : List.count j (boxProfile label S) = {p ∈ S | label p = j}.card

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.boxProfile_pairwise (label : ℕ → ℕ) (S : Finset ℕ) : List.Pairwise (fun (x1 x2 : ℕ) => x1 ≥ x2) (boxProfile label S)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.boxProfile_eq_of_counts {label : ℕ → ℕ} {S T : Finset ℕ} (h : ∀ (j : ℕ), List.count j (boxProfile label S) = List.count j (boxProfile label T)) : boxProfile label S = boxProfile label T

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.boxProfile_eq_map_sort (label : ℕ → ℕ) (S : Finset ℕ) (hmono : ∀ p ∈ S, ∀ q ∈ S, p ≤ q → label p ≤ label q) : boxProfile label S = List.map label (S.sort fun (x1 x2 : ℕ) => x1 ≥ x2)

The prime order gives exactly the same occurrence list whenever the labels respect that order. Equal labels are retained, not collapsed.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.boxProfile_nodup_iff (label : ℕ → ℕ) (S : Finset ℕ) : (boxProfile label S).Nodup ↔ Set.InjOn label ↑S

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.boxProfile_prod (label : ℕ → ℕ) (b : ℕ → ℝ) (S : Finset ℕ) : (List.map b (boxProfile label S)).prod = ∏ p ∈ S, b (label p)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.cubicPrefixBound_map_iff (upper : Bool) (b : ℕ → ℝ) (D : ℝ) (label : ℕ → ℕ) (l : List ℕ) : LiLiuPrereqWFAdmissibility.CubicPrefixBound upper b D (List.map label l) ↔ LiLiuPrereqWFAdmissibility.CubicPrefixBound upper (fun (p : ℕ) => b (label p)) D l

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.admissible_map_iff (upper : Bool) (b : ℕ → ℝ) (D : ℝ) (label : ℕ → ℕ) (l : List ℕ) : LiLiuPrereqWFAdmissibility.Admissible upper b D (List.map label l) ↔ LiLiuPrereqWFAdmissibility.Admissible upper (fun (p : ℕ) => b (label p)) D l

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.roundedSupport_boxProfile_iff (upper : Bool) (label : ℕ → ℕ) (b : ℕ → ℝ) (D : ℝ) (S : Finset ℕ) (hmono : ∀ p ∈ S, ∀ q ∈ S, p ≤ q → label p ≤ label q) : RoundedSupport upper (fun (p : ℕ) => b (label p)) D S ↔ (List.map b (boxProfile label S)).prod < D ∧ LiLiuPrereqWFAdmissibility.CubicPrefixBound upper b D (boxProfile label S)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.boxProfile_matches_iff (label : ℕ → ℕ) (B : ℕ → Finset ℕ) (B₀ N : Finset ℕ) (t : List ℕ) (ht : List.Pairwise (fun (x1 x2 : ℕ) => x1 ≥ x2) t) (hdisj : ∀ (i j : ℕ), i ≠ j → Disjoint (B i) (B j)) (hsep : ∀ (j : ℕ), Disjoint B₀ (B j)) (hcover : ∀ p ∈ N \ B₀, p ∈ B (label p)) : (N ⊆ B₀ ∪ t.toFinset.biUnion B ∧ ∀ j ∈ t.toFinset, (N ∩ B j).card = List.count j t) ↔ t = boxProfile label (N \ B₀)

The box-count test singles out the canonical occurrence profile. The inputs are only membership and disjointness of finite sets.