Decreasing rearrangements of nonnegative null families

The decreasing rearrangement lists the values of a nonnegative null family in descending order, with multiplicities. It is padded by zeros when only finitely many values are positive, including for an empty index type. The characterization by finite superlevel sets avoids choosing an enumeration of the original index type.

For a family tending to zero along the cofinite filter, its rearrangement tends to zero and bounds every finite product by the product of the same number of initial terms. This supplies ordered bounds for determinants with arbitrarily indexed rows.

noncomputable def TauCeti.decreasingRearrangement {ι : Type u_1} (r : ι → ℝ) (n : ℕ) : ℝ

The decreasing rearrangement of a bounded nonnegative family, padded by zeros. The term at n is the supremum of the lower bounds on n + 1 distinct entries, together with zero. For a null family, a positive rearranged term is attained by an entry.

theorem TauCeti.decreasingRearrangement_def {ι : Type u_1} (r : ι → ℝ) (n : ℕ) : decreasingRearrangement r n = sSup (insert 0 {a : ℝ | ∃ (s : Finset ι), s.card = n + 1 ∧ ∀ i ∈ s, a ≤ r i})

theorem TauCeti.decreasingRearrangement_nonneg {ι : Type u_1} {r : ι → ℝ} (hr : BddAbove (Set.range r)) (n : ℕ) : 0 ≤ decreasingRearrangement r n

Rearranged bounds are nonnegative, even when there are no indices.

theorem TauCeti.le_decreasingRearrangement {ι : Type u_1} {r : ι → ℝ} (hr : BddAbove (Set.range r)) {n : ℕ} {s : Finset ι} (hs : s.card = n + 1) {a : ℝ} (ha : ∀ i ∈ s, a ≤ r i) : a ≤ decreasingRearrangement r n

A lower bound on n + 1 distinct entries is bounded by the n-th rearranged entry.

theorem TauCeti.antitone_decreasingRearrangement {ι : Type u_1} {r : ι → ℝ} (hr : BddAbove (Set.range r)) : Antitone (decreasingRearrangement r)

The rearrangement is antitone.

theorem TauCeti.decreasingRearrangement_le_of_card_le {ι : Type u_1} {r : ι → ℝ} {a : ℝ} (ha : 0 ≤ a) {s : Finset ι} {n : ℕ} (hs : s.card ≤ n) (hr : ∀ i ∉ s, r i ≤ a) : decreasingRearrangement r n ≤ a

A finite set containing every entry larger than a bounds the rearrangement from its cardinality onward. In particular finite support gives zero padding.

@[simp]

theorem TauCeti.decreasingRearrangement_zero {ι : Type u_1} (n : ℕ) : decreasingRearrangement 0 n = 0

The rearrangement of the zero family is zero.

theorem TauCeti.lt_decreasingRearrangement_iff {ι : Type u_1} {r : ι → ℝ} (hr : BddAbove (Set.range r)) {a : ℝ} (ha : 0 ≤ a) (n : ℕ) : a < decreasingRearrangement r n ↔ ∃ (s : Finset ι), s.card = n + 1 ∧ ∀ i ∈ s, a < r i

Strict superlevels characterize the rearrangement, retaining repeated values and their multiplicities. The threshold may be zero.

theorem TauCeti.card_le_of_forall_decreasingRearrangement_lt {ι : Type u_1} {r : ι → ℝ} (hr : BddAbove (Set.range r)) {n : ℕ} {s : Finset ι} (hs : ∀ i ∈ s, decreasingRearrangement r n < r i) : s.card ≤ n

At most n entries exceed the n-th rearranged entry.

theorem TauCeti.finite_setOf_decreasingRearrangement_lt {ι : Type u_1} {r : ι → ℝ} (hr : BddAbove (Set.range r)) (n : ℕ) : {i : ι | decreasingRearrangement r n < r i}.Finite

Only finitely many entries exceed a given rearranged entry.

theorem TauCeti.setOf_lt_decreasingRearrangement {ι : Type u_1} {r : ι → ℝ} {a : ℝ} (ha : 0 ≤ a) (hfin : {i : ι | a < r i}.Finite) : {n : ℕ | a < decreasingRearrangement r n} = Set.Iio hfin.toFinset.card

A finite strict superlevel set becomes an initial segment of the same cardinality. Thus the rearrangement preserves multiplicities, including ties.

theorem TauCeti.decreasingRearrangement_comp_subtypeVal {ι : Type u_1} {r : ι → ℝ} (hr : BddAbove (Set.range r)) {S : Set ι} (hS : ∀ (i : ι), 0 < r i → i ∈ S) (n : ℕ) : decreasingRearrangement (fun (i : ↑S) => r ↑i) n = decreasingRearrangement r n

Discarding entries that are not positive does not change the rearrangement: restricting r to a set of indices containing every positive entry has the same rearrangement.

theorem TauCeti.exists_eq_decreasingRearrangement {ι : Type u_1} {r : ι → ℝ} (hr : Filter.Tendsto r Filter.cofinite (nhds 0)) {n : ℕ} (hn : 0 < decreasingRearrangement r n) : ∃ (i : ι), r i = decreasingRearrangement r n

Every positive term of the rearrangement of a null family is an original entry.

theorem TauCeti.tendsto_decreasingRearrangement {ι : Type u_1} {r : ι → ℝ} (hr : Filter.Tendsto r Filter.cofinite (nhds 0)) : Filter.Tendsto (decreasingRearrangement r) Filter.atTop (nhds 0)

A family tending to zero cofinitely has a null decreasing rearrangement.

theorem TauCeti.prod_le_prod_decreasingRearrangement {ι : Type u_1} {r : ι → ℝ} (hr₀ : ∀ (i : ι), 0 ≤ r i) (hr : BddAbove (Set.range r)) (s : Finset ι) : ∏ i ∈ s, r i ≤ ∏ k ∈ Finset.range s.card, decreasingRearrangement r k

Every finite product of entries is bounded by the initial product of the rearrangement.