Reindexing and sorting finite two-point systems

noncomputable def Feige.descendingPerm {m : ℕ} (γ : Fin m → ℝ) : Equiv.Perm (Fin m)

Permutation which arranges γ in nonincreasing order.

Equations

• Feige.descendingPerm γ = Tuple.sort fun (i : Fin m) => -γ i

theorem Feige.antitone_comp_descendingPerm {m : ℕ} (γ : Fin m → ℝ) : Antitone (γ ∘ ⇑(descendingPerm γ))

theorem Feige.dirichletK_comp_perm {m : ℕ} (y : Fin m → ℝ) (σ : Equiv.Perm (Fin m)) : dirichletK (y ∘ ⇑σ) = dirichletK y

theorem Feige.twoPointKFinset_comp_perm {m : ℕ} (γ β : Fin m → ℝ) (σ : Equiv.Perm (Fin m)) (S : Finset (Fin m)) : twoPointKFinset (γ ∘ ⇑σ) (β ∘ ⇑σ) S = twoPointKFinset γ β (Finset.map (Equiv.toEmbedding σ) S)

theorem Feige.highSetMass_comp_perm {m : ℕ} (p : Fin m → ℝ) (σ : Equiv.Perm (Fin m)) (S : Finset (Fin m)) : highSetMass (p ∘ ⇑σ) S = highSetMass p (Finset.map (Equiv.toEmbedding σ) S)

theorem Feige.twoPointRejectionMass_comp_perm {m : ℕ} (γ β : Fin m → ℝ) (σ : Equiv.Perm (Fin m)) (α : ℝ) : twoPointRejectionMass (γ ∘ ⇑σ) (β ∘ ⇑σ) α = twoPointRejectionMass γ β α

theorem Feige.strictTwoPoint_rejection_le_of_localInsertion (hlocal : StrictOrderedLocalInsertion) {m : ℕ} (γ β : Fin m → ℝ) (hγpos : ∀ (i : Fin m), 0 < γ i) (hγle : ∀ (i : Fin m), γ i ≤ 1) (hβpos : ∀ (i : Fin m), 0 < β i) {α : ℝ} (hα : 0 ≤ α) : twoPointRejectionMass γ β α ≤ α

Arbitrary strict systems reduce to the ordered theorem by sorting the γ coordinates and simultaneously transporting every product coordinate.