Finite families of run-compressed multiplicity profiles

For an original multiplicity function ml, every run-compressed multiplicity lies coordinatewise in Fin (ml a + 1). This gives a finite profile carrier of size at most 2 ^ ∑ a, ml a, and hence the same bound for every realized image. The final section packages exact finite regrouping by these profiles and a uniform nonnegative fiber bound.

@[reducible, inline]

abbrev Anderson4D.MergeMultiplicityProfile {α : Type u_1} (ml : α → ℕ) : Type u_1

Coordinatewise-bounded multiplicity profiles produced by run compression.

Equations

• Anderson4D.MergeMultiplicityProfile ml = ((a : α) → Fin (ml a + 1))

@[reducible, inline]

abbrev Anderson4D.MergeValidWord {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) : Type u_1

A valid original word, retained as a subtype so its multiplicity proof is available when its compressed profile is constructed.

Equations

• Anderson4D.MergeValidWord ml = ↥(Anderson4D.validWords ml)

def Anderson4D.mergedMultiplicityProfile {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) (w : MergeValidWord ml) : MergeMultiplicityProfile ml

The merged multiplicity of a valid word, packaged in the finite profile carrier.

Equations

• Anderson4D.mergedMultiplicityProfile ml w a = ⟨Anderson4D.mergedMultiplicity (↑w) a, ⋯⟩

@[simp]

theorem Anderson4D.mergedMultiplicityProfile_val {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) (w : MergeValidWord ml) (a : α) : ↑(mergedMultiplicityProfile ml w a) = mergedMultiplicity (↑w) a

def Anderson4D.MergeMultiplicityProfile.toNat {α : Type u_1} {ml : α → ℕ} (p : MergeMultiplicityProfile ml) : α → ℕ

The natural-valued function underlying a finite profile.

Equations

• p.toNat a = ↑(p a)

@[simp]

theorem Anderson4D.mergedMultiplicityProfile_toNat {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) (w : MergeValidWord ml) : (mergedMultiplicityProfile ml w).toNat = mergedMultiplicity ↑w

theorem Anderson4D.sum_mergedMultiplicityProfile {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) (w : MergeValidWord ml) : ∑ a : α, ↑(mergedMultiplicityProfile ml w a) = (mergedWordList ↑w).length

The entries of the packaged profile sum to the compressed word length.

theorem Anderson4D.card_mergeMultiplicityProfile {α : Type u_1} [Fintype α] [DecidableEq α] (ml : α → ℕ) : Fintype.card (MergeMultiplicityProfile ml) = ∏ a : α, (ml a + 1)

Exact cardinality of the full coordinatewise profile carrier.

theorem Anderson4D.card_mergeMultiplicityProfile_le_two_pow_sum {α : Type u_1} [Fintype α] [DecidableEq α] (ml : α → ℕ) : Fintype.card (MergeMultiplicityProfile ml) ≤ 2 ^ ∑ a : α, ml a

The full finite profile carrier has at most 2 ^ ∑ a, ml a elements.

def Anderson4D.mergeMultiplicityProfileImage {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) (s : Finset (MergeValidWord ml)) : Finset (MergeMultiplicityProfile ml)

Profiles realized by an arbitrary finite family of valid words.

Equations

• Anderson4D.mergeMultiplicityProfileImage ml s = Finset.image (Anderson4D.mergedMultiplicityProfile ml) s

theorem Anderson4D.card_mergeMultiplicityProfileImage_le_two_pow_sum {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) (s : Finset (MergeValidWord ml)) : (mergeMultiplicityProfileImage ml s).card ≤ 2 ^ ∑ a : α, ml a

The realized image is no larger than the full profile carrier.

def Anderson4D.possibleMergeMultiplicityProfiles {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) : Finset (MergeMultiplicityProfile ml)

All compressed multiplicity profiles realized by valid words.

Equations

• Anderson4D.possibleMergeMultiplicityProfiles ml = Anderson4D.mergeMultiplicityProfileImage ml Finset.univ

theorem Anderson4D.card_possibleMergeMultiplicityProfiles_le_two_pow_sum {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) : (possibleMergeMultiplicityProfiles ml).card ≤ 2 ^ ∑ a : α, ml a

The set of all possible compressed profiles has the same exponential cardinality bound.

theorem Anderson4D.sum_eq_sum_mergeMultiplicityProfile_fibers {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) (s : Finset (MergeValidWord ml)) (F : MergeValidWord ml → ℝ) : ∑ w ∈ s, F w = ∑ p ∈ mergeMultiplicityProfileImage ml s, ∑ w ∈ s with mergedMultiplicityProfile ml w = p, F w

Exact regrouping of an arbitrary finite weighted sum by its packaged run-compressed multiplicity profile.

theorem Anderson4D.sum_mergeMultiplicityProfileImage_le_two_pow_mul {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) (s : Finset (MergeValidWord ml)) (G : MergeMultiplicityProfile ml → ℝ) (B : ℝ) (hB : 0 ≤ B) (hGB : ∀ p ∈ mergeMultiplicityProfileImage ml s, G p ≤ B) : ∑ p ∈ mergeMultiplicityProfileImage ml s, G p ≤ (2 ^ ∑ a : α, ml a) * B

A nonnegative uniformly bounded statistic on realized profiles costs at most the profile-carrier cardinality.

theorem Anderson4D.sum_le_two_pow_mul_of_profileFiber_le {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) (s : Finset (MergeValidWord ml)) (F : MergeValidWord ml → ℝ) (B : ℝ) (hB : 0 ≤ B) (hfiber : ∀ p ∈ mergeMultiplicityProfileImage ml s, ∑ w ∈ s with mergedMultiplicityProfile ml w = p, F w ≤ B) : ∑ w ∈ s, F w ≤ (2 ^ ∑ a : α, ml a) * B

Uniform nonnegative fiber estimate after exact profile regrouping.

theorem Anderson4D.sum_nonneg_and_le_two_pow_mul_of_profileFiber_le {α : Type u_1} [Fintype α] [DecidableEq α] {M : ℕ} (ml : α → ℕ) (s : Finset (MergeValidWord ml)) (F : MergeValidWord ml → ℝ) (B : ℝ) (hB : 0 ≤ B) (hF0 : ∀ w ∈ s, 0 ≤ F w) (hfiber : ∀ p ∈ mergeMultiplicityProfileImage ml s, ∑ w ∈ s with mergedMultiplicityProfile ml w = p, F w ≤ B) : 0 ≤ ∑ w ∈ s, F w ∧ ∑ w ∈ s, F w ≤ (2 ^ ∑ a : α, ml a) * B

Bundled nonnegative version of the uniform fiber interface.