5.a. The Quantile Vertex🔗

This is the general-position heart of the proof, playing the role of the original argument's "handles in general position". The idea: give each active index \alpha a distinct threshold t_\alpha \in (0,1); a point q of the polytope, with barycentric weights (w_u)_{u \in \sigma} in a coarse simplex \sigma, is labelled by the vertex at which the cumulative weight — accumulated in a fixed global order on the vertices — first reaches t_\alpha. On a sufficiently fine refinement, each cumulative weight oscillates, over any single top cell, by less than the spacing between thresholds, so at most |\sigma| - 1 \le k of the labellings can be non-constant on that cell.

If P = \emptyset, take any subdivision and any labelling; all conditions are vacuous. So assume P \ne \emptyset and fix p_0 \in P.

This chapter develops the combinatorial core on a single face: cumulative weights in a fixed global vertex order, the quantile vertex, and its three key lemmas. The data of the construction (the coarse subdivision, thresholds, and barycentric coordinate functionals of Section 5.1) and the assembly of the labelling family (Sections 5.3–5.4) are in the next chapter.

A global vertex order. Fix the lexicographic order \preceq on \mathbb R^k (any linear order would do). For a face \sigma, weights w, and a vertex v \in \sigma, the cumulative weight is \mathrm{cum}_\sigma(w, v) \;:=\; \sum_{u \in \sigma,\; u \preceq v} w(u).

The Lean development also needs uniqueness of barycentric weights (stated as part of Section 5.1's conventions: two weight systems on an affinely independent face with unit total mass representing the same point agree):

open scoped BigOperators
open Geometry

namespace Submission
namespace Quantile

variable {k : ℕ}

/-
**Uniqueness of barycentric weights.** Two weight functions supported on an affinely
independent finset `T`, each summing to `1` and representing the same point `q`, agree on
`T`.  (Uniqueness of affine-combination coordinates.)
-/
lemma weights_unique
    {T : Finset (Fin k → ℝ)}
    (hT : AffineIndependent ℝ ((↑) : T → (Fin k → ℝ)))
    {w₁ w₂ : (Fin k → ℝ) → ℝ}
    (hs₁ : ∑ v ∈ T, w₁ v = 1) (hs₂ : ∑ v ∈ T, w₂ v = 1)
    (hq : ∑ v ∈ T, w₁ v • v = ∑ v ∈ T, w₂ v • v) :
    ∀ v ∈ T, w₁ v = w₂ v := byk:ℕT:Finset (Fin k → ℝ)hT:AffineIndependent ℝ Subtype.valw₁:(Fin k → ℝ) → ℝw₂:(Fin k → ℝ) → ℝhs₁:∑ v ∈ T, w₁ v = 1hs₂:∑ v ∈ T, w₂ v = 1hq:∑ v ∈ T, w₁ v • v = ∑ v ∈ T, w₂ v • v⊢ ∀ v ∈ T, w₁ v = w₂ v
  have := hTk:ℕT:Finset (Fin k → ℝ)hT:AffineIndependent ℝ Subtype.valw₁:(Fin k → ℝ) → ℝw₂:(Fin k → ℝ) → ℝhs₁:∑ v ∈ T, w₁ v = 1hs₂:∑ v ∈ T, w₂ v = 1hq:∑ v ∈ T, w₁ v • v = ∑ v ∈ T, w₂ v • vthis:AffineIndependent ℝ Subtype.val⊢ ∀ v ∈ T, w₁ v = w₂ v;
  convert this.eq_of_sum_eq_sum ( show ∑ v ∈ T.attach, w₁ v.1 = ∑ v ∈ T.attach, w₂ v.1 from ?_ ) ( show ∑ v ∈ T.attach, w₁ v.1 • ( v.1 : Fin k → ℝ ) = ∑ v ∈ T.attach, w₂ v.1 • ( v.1 : Fin k → ℝ ) from ?_ ) using 1ak:ℕT:Finset (Fin k → ℝ)hT:AffineIndependent ℝ Subtype.valw₁:(Fin k → ℝ) → ℝw₂:(Fin k → ℝ) → ℝhs₁:∑ v ∈ T, w₁ v = 1hs₂:∑ v ∈ T, w₂ v = 1hq:∑ v ∈ T, w₁ v • v = ∑ v ∈ T, w₂ v • vthis:AffineIndependent ℝ Subtype.val⊢ (∀ v ∈ T, w₁ v = w₂ v) ↔ ∀ i ∈ T.attach, w₁ ↑i = w₂ ↑iconvert_1k:ℕT:Finset (Fin k → ℝ)hT:AffineIndependent ℝ Subtype.valw₁:(Fin k → ℝ) → ℝw₂:(Fin k → ℝ) → ℝhs₁:∑ v ∈ T, w₁ v = 1hs₂:∑ v ∈ T, w₂ v = 1hq:∑ v ∈ T, w₁ v • v = ∑ v ∈ T, w₂ v • vthis:AffineIndependent ℝ Subtype.val⊢ ∑ v ∈ T.attach, w₁ ↑v = ∑ v ∈ T.attach, w₂ ↑vconvert_2k:ℕT:Finset (Fin k → ℝ)hT:AffineIndependent ℝ Subtype.valw₁:(Fin k → ℝ) → ℝw₂:(Fin k → ℝ) → ℝhs₁:∑ v ∈ T, w₁ v = 1hs₂:∑ v ∈ T, w₂ v = 1hq:∑ v ∈ T, w₁ v • v = ∑ v ∈ T, w₂ v • vthis:AffineIndependent ℝ Subtype.val⊢ ∑ v ∈ T.attach, w₁ ↑v • ↑v = ∑ v ∈ T.attach, w₂ ↑v • ↑v;
  ·ak:ℕT:Finset (Fin k → ℝ)hT:AffineIndependent ℝ Subtype.valw₁:(Fin k → ℝ) → ℝw₂:(Fin k → ℝ) → ℝhs₁:∑ v ∈ T, w₁ v = 1hs₂:∑ v ∈ T, w₂ v = 1hq:∑ v ∈ T, w₁ v • v = ∑ v ∈ T, w₂ v • vthis:AffineIndependent ℝ Subtype.val⊢ (∀ v ∈ T, w₁ v = w₂ v) ↔ ∀ i ∈ T.attach, w₁ ↑i = w₂ ↑i simp +decide [ Finset.mem_attach ]All goals completed! 🐙;
  ·convert_1k:ℕT:Finset (Fin k → ℝ)hT:AffineIndependent ℝ Subtype.valw₁:(Fin k → ℝ) → ℝw₂:(Fin k → ℝ) → ℝhs₁:∑ v ∈ T, w₁ v = 1hs₂:∑ v ∈ T, w₂ v = 1hq:∑ v ∈ T, w₁ v • v = ∑ v ∈ T, w₂ v • vthis:AffineIndependent ℝ Subtype.val⊢ ∑ v ∈ T.attach, w₁ ↑v = ∑ v ∈ T.attach, w₂ ↑v convert hs₁.trans hs₂.symm using 1h.e'_2k:ℕT:Finset (Fin k → ℝ)hT:AffineIndependent ℝ Subtype.valw₁:(Fin k → ℝ) → ℝw₂:(Fin k → ℝ) → ℝhs₁:∑ v ∈ T, w₁ v = 1hs₂:∑ v ∈ T, w₂ v = 1hq:∑ v ∈ T, w₁ v • v = ∑ v ∈ T, w₂ v • vthis:AffineIndependent ℝ Subtype.val⊢ ∑ v ∈ T.attach, w₁ ↑v = ∑ v ∈ T, w₁ vh.e'_3k:ℕT:Finset (Fin k → ℝ)hT:AffineIndependent ℝ Subtype.valw₁:(Fin k → ℝ) → ℝw₂:(Fin k → ℝ) → ℝhs₁:∑ v ∈ T, w₁ v = 1hs₂:∑ v ∈ T, w₂ v = 1hq:∑ v ∈ T, w₁ v • v = ∑ v ∈ T, w₂ v • vthis:AffineIndependent ℝ Subtype.val⊢ ∑ v ∈ T.attach, w₂ ↑v = ∑ v ∈ T, w₂ v;
    ·h.e'_2k:ℕT:Finset (Fin k → ℝ)hT:AffineIndependent ℝ Subtype.valw₁:(Fin k → ℝ) → ℝw₂:(Fin k → ℝ) → ℝhs₁:∑ v ∈ T, w₁ v = 1hs₂:∑ v ∈ T, w₂ v = 1hq:∑ v ∈ T, w₁ v • v = ∑ v ∈ T, w₂ v • vthis:AffineIndependent ℝ Subtype.val⊢ ∑ v ∈ T.attach, w₁ ↑v = ∑ v ∈ T, w₁ v conv_rhs => rw [ ← Finset.sum_attach ]k:ℕT:Finset (Fin k → ℝ)hT:AffineIndependent ℝ Subtype.valw₁:(Fin k → ℝ) → ℝw₂:(Fin k → ℝ) → ℝhs₁:∑ v ∈ T, w₁ v = 1hs₂:∑ v ∈ T, w₂ v = 1hq:∑ v ∈ T, w₁ v • v = ∑ v ∈ T, w₂ v • vthis:AffineIndependent ℝ Subtype.val| ∑ x ∈ T.attach, w₁ ↑x ;
    ·h.e'_3k:ℕT:Finset (Fin k → ℝ)hT:AffineIndependent ℝ Subtype.valw₁:(Fin k → ℝ) → ℝw₂:(Fin k → ℝ) → ℝhs₁:∑ v ∈ T, w₁ v = 1hs₂:∑ v ∈ T, w₂ v = 1hq:∑ v ∈ T, w₁ v • v = ∑ v ∈ T, w₂ v • vthis:AffineIndependent ℝ Subtype.val⊢ ∑ v ∈ T.attach, w₂ ↑v = ∑ v ∈ T, w₂ v conv_rhs => rw [ ← Finset.sum_attach ]k:ℕT:Finset (Fin k → ℝ)hT:AffineIndependent ℝ Subtype.valw₁:(Fin k → ℝ) → ℝw₂:(Fin k → ℝ) → ℝhs₁:∑ v ∈ T, w₁ v = 1hs₂:∑ v ∈ T, w₂ v = 1hq:∑ v ∈ T, w₁ v • v = ∑ v ∈ T, w₂ v • vthis:AffineIndependent ℝ Subtype.val| ∑ x ∈ T.attach, w₂ ↑x ;
  ·convert_2k:ℕT:Finset (Fin k → ℝ)hT:AffineIndependent ℝ Subtype.valw₁:(Fin k → ℝ) → ℝw₂:(Fin k → ℝ) → ℝhs₁:∑ v ∈ T, w₁ v = 1hs₂:∑ v ∈ T, w₂ v = 1hq:∑ v ∈ T, w₁ v • v = ∑ v ∈ T, w₂ v • vthis:AffineIndependent ℝ Subtype.val⊢ ∑ v ∈ T.attach, w₁ ↑v • ↑v = ∑ v ∈ T.attach, w₂ ↑v • ↑v convert hq using 1h.e'_2k:ℕT:Finset (Fin k → ℝ)hT:AffineIndependent ℝ Subtype.valw₁:(Fin k → ℝ) → ℝw₂:(Fin k → ℝ) → ℝhs₁:∑ v ∈ T, w₁ v = 1hs₂:∑ v ∈ T, w₂ v = 1hq:∑ v ∈ T, w₁ v • v = ∑ v ∈ T, w₂ v • vthis:AffineIndependent ℝ Subtype.val⊢ ∑ v ∈ T.attach, w₁ ↑v • ↑v = ∑ v ∈ T, w₁ v • vh.e'_3k:ℕT:Finset (Fin k → ℝ)hT:AffineIndependent ℝ Subtype.valw₁:(Fin k → ℝ) → ℝw₂:(Fin k → ℝ) → ℝhs₁:∑ v ∈ T, w₁ v = 1hs₂:∑ v ∈ T, w₂ v = 1hq:∑ v ∈ T, w₁ v • v = ∑ v ∈ T, w₂ v • vthis:AffineIndependent ℝ Subtype.val⊢ ∑ v ∈ T.attach, w₂ ↑v • ↑v = ∑ v ∈ T, w₂ v • v;
    ·h.e'_2k:ℕT:Finset (Fin k → ℝ)hT:AffineIndependent ℝ Subtype.valw₁:(Fin k → ℝ) → ℝw₂:(Fin k → ℝ) → ℝhs₁:∑ v ∈ T, w₁ v = 1hs₂:∑ v ∈ T, w₂ v = 1hq:∑ v ∈ T, w₁ v • v = ∑ v ∈ T, w₂ v • vthis:AffineIndependent ℝ Subtype.val⊢ ∑ v ∈ T.attach, w₁ ↑v • ↑v = ∑ v ∈ T, w₁ v • v conv_rhs => rw [ ← Finset.sum_attach ]k:ℕT:Finset (Fin k → ℝ)hT:AffineIndependent ℝ Subtype.valw₁:(Fin k → ℝ) → ℝw₂:(Fin k → ℝ) → ℝhs₁:∑ v ∈ T, w₁ v = 1hs₂:∑ v ∈ T, w₂ v = 1hq:∑ v ∈ T, w₁ v • v = ∑ v ∈ T, w₂ v • vthis:AffineIndependent ℝ Subtype.val| ∑ x ∈ T.attach, w₁ ↑x • ↑x ;
    ·h.e'_3k:ℕT:Finset (Fin k → ℝ)hT:AffineIndependent ℝ Subtype.valw₁:(Fin k → ℝ) → ℝw₂:(Fin k → ℝ) → ℝhs₁:∑ v ∈ T, w₁ v = 1hs₂:∑ v ∈ T, w₂ v = 1hq:∑ v ∈ T, w₁ v • v = ∑ v ∈ T, w₂ v • vthis:AffineIndependent ℝ Subtype.val⊢ ∑ v ∈ T.attach, w₂ ↑v • ↑v = ∑ v ∈ T, w₂ v • v conv_rhs => rw [ ← Finset.sum_attach ]k:ℕT:Finset (Fin k → ℝ)hT:AffineIndependent ℝ Subtype.valw₁:(Fin k → ℝ) → ℝw₂:(Fin k → ℝ) → ℝhs₁:∑ v ∈ T, w₁ v = 1hs₂:∑ v ∈ T, w₂ v = 1hq:∑ v ∈ T, w₁ v • v = ∑ v ∈ T, w₂ v • vthis:AffineIndependent ℝ Subtype.val| ∑ x ∈ T.attach, w₂ ↑x • ↑x ;

For a face \sigma, weights w, and a threshold t, define the quantile vertex \mathrm{qv}_\sigma(w,t) to be the \preceq-least vertex v \in \sigma with t \le \mathrm{cum}_\sigma(w,v), when one exists.

open scoped Classical in
/-- Cumulative weight up to (and including) `v` in the global lexicographic order. -/
noncomputable def cumWeight (T : Finset (Fin k → ℝ)) (w : (Fin k → ℝ) → ℝ)
    (v : Fin k → ℝ) : ℝ :=
  ∑ u ∈ T.filter (fun u => toLex u ≤ toLex v), w u

open scoped Classical in
/-- The cumulative-mass quantile vertex: the lexicographically least vertex of `T` whose
cumulative weight reaches the threshold `t`.  (Junk value `0` if no such vertex exists.) -/
noncomputable def quantileV (T : Finset (Fin k → ℝ)) (w : (Fin k → ℝ) → ℝ) (t : ℝ) :
    Fin k → ℝ :=
  if h : (T.filter (fun v => t ≤ cumWeight T w v)).Nonempty then
    ofLex (((T.filter (fun v => t ≤ cumWeight T w v)).image toLex).min'
      (byk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝh:{v ∈ T | t ≤ cumWeight T w v}.Nonempty⊢ (Finset.image (⇑toLex) ({v ∈ T | t ≤ cumWeight T w v})).Nonempty simpa using h.image toLexAll goals completed! 🐙))
  else 0

Lemma 5.2.1🔗

Lemma 5.2.1. If w \ge 0 on \sigma, \sum_{u\in\sigma} w(u) = 1, \sigma \ne \emptyset and 0 < t \le 1, then the quantile vertex exists, lies in \sigma, and carries strictly positive weight: w(\mathrm{qv}_\sigma(w,t)) > 0.

Proof. At the \preceq-greatest vertex the cumulative weight is the total weight 1 \ge t, so the defining set is nonempty and v := \mathrm{qv}_\sigma(w,t) \in \sigma. By minimality of v, the total weight of \{u \in \sigma : u \prec v\} is < t: it equals \mathrm{cum}_\sigma(w,u) at the \preceq-greatest such u if one exists, and 0 < t otherwise. Since \mathrm{cum}_\sigma(w,v) = \bigl(\text{total weight below } v\bigr) + w(v) \ge t, we get w(v) > 0. \blacksquare

/-
The quantile vertex lies in `T` (provided some vertex reaches the threshold).
-/
lemma quantileV_mem (T : Finset (Fin k → ℝ)) (w : (Fin k → ℝ) → ℝ) (t : ℝ)
    (h : (T.filter (fun v => t ≤ cumWeight T w v)).Nonempty) :
    quantileV T w t ∈ T := byk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝh:{v ∈ T | t ≤ cumWeight T w v}.Nonempty⊢ quantileV T w t ∈ T
  unfold quantileVk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝh:{v ∈ T | t ≤ cumWeight T w v}.Nonempty⊢ (if h : {v ∈ T | t ≤ cumWeight T w v}.Nonempty then
    ofLex ((Finset.image (⇑toLex) ({v ∈ T | t ≤ cumWeight T w v})).min' ⋯)
  else 0) ∈
  T;
  have := Finset.min'_mem ( Finset.image toLex ( Finset.filter ( fun v => t ≤ cumWeight T w v ) T ) )k:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝh:{v ∈ T | t ≤ cumWeight T w v}.Nonemptythis:∀ (H : (Finset.image (⇑toLex) ({v ∈ T | t ≤ cumWeight T w v})).Nonempty),
  (Finset.image (⇑toLex) ({v ∈ T | t ≤ cumWeight T w v})).min' H ∈ Finset.image (⇑toLex) ({v ∈ T | t ≤ cumWeight T w v})⊢ (if h : {v ∈ T | t ≤ cumWeight T w v}.Nonempty then
    ofLex ((Finset.image (⇑toLex) ({v ∈ T | t ≤ cumWeight T w v})).min' ⋯)
  else 0) ∈
  T ; aesopAll goals completed! 🐙;

/-
If the weights are nonnegative and sum to `1`, and `0 < t ≤ 1`, then the threshold is
reached by some vertex (the lexicographically largest).
-/
lemma quantileV_filter_nonempty (T : Finset (Fin k → ℝ)) (w : (Fin k → ℝ) → ℝ) (t : ℝ)
    (ht1 : t ≤ 1) (hw : ∀ v ∈ T, 0 ≤ w v) (hsum : ∑ v ∈ T, w v = 1) (hTne : T.Nonempty) :
    (T.filter (fun v => t ≤ cumWeight T w v)).Nonempty := byk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonempty⊢ {v ∈ T | t ≤ cumWeight T w v}.Nonempty
  obtain ⟨m, hm⟩ : ∃ m ∈ T.image toLex, ∀ v ∈ T.image toLex, v ≤ m := byk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonempty⊢ ∃ m ∈ Finset.image (⇑toLex) T, ∀ v ∈ Finset.image (⇑toLex) T, v ≤ m
    exact ⟨ Finset.max' _ <| Finset.nonempty_of_ne_empty <| byk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonempty⊢ Finset.image (⇑toLex) T ≠ ∅ aesop_catAll goals completed! 🐙, Finset.max'_mem _ _, fun v hv => Finset.le_max' _ _ hv ⟩;
  obtain ⟨ v, hv, rfl ⟩ := Finset.mem_image.mp hm.1k:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝhv:v ∈ Thm:toLex v ∈ Finset.image (⇑toLex) T ∧ ∀ v_1 ∈ Finset.image (⇑toLex) T, v_1 ≤ toLex v⊢ {v ∈ T | t ≤ cumWeight T w v}.Nonempty;
  refine' ⟨ v, Finset.mem_filter.mpr ⟨ hv, _ ⟩ ⟩k:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝhv:v ∈ Thm:toLex v ∈ Finset.image (⇑toLex) T ∧ ∀ v_1 ∈ Finset.image (⇑toLex) T, v_1 ≤ toLex v⊢ t ≤ cumWeight T w v;
  refine' le_trans ht1 _k:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝhv:v ∈ Thm:toLex v ∈ Finset.image (⇑toLex) T ∧ ∀ v_1 ∈ Finset.image (⇑toLex) T, v_1 ≤ toLex v⊢ 1 ≤ cumWeight T w v;
  rw [ ← hsum, cumWeight ]k:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝhv:v ∈ Thm:toLex v ∈ Finset.image (⇑toLex) T ∧ ∀ v_1 ∈ Finset.image (⇑toLex) T, v_1 ≤ toLex v⊢ ∑ v ∈ T, w v ≤ ∑ u ∈ T with toLex u ≤ toLex v, w u;
  rw [ Finset.filter_true_of_mem fun u hu => hm.2 _ <| Finset.mem_image_of_mem _ hu ]All goals completed! 🐙

/-
**Positive weight at the quantile vertex.** With nonnegative weights summing to `1` and
`0 < t ≤ 1`, the quantile vertex carries strictly positive weight, hence lies in the support
of the point it represents.
-/
set_option maxHeartbeats 1600000 in
lemma quantileV_weight_pos (T : Finset (Fin k → ℝ)) (w : (Fin k → ℝ) → ℝ) (t : ℝ)
    (ht0 : 0 < t) (ht1 : t ≤ 1) (hw : ∀ v ∈ T, 0 ≤ w v) (hsum : ∑ v ∈ T, w v = 1)
    (hTne : T.Nonempty) :
    0 < w (quantileV T w t) := byk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonempty⊢ 0 < w (quantileV T w t)
  classical
  -- Let `v := quantileV T w t`; it lies in `T` and `t ≤ cumWeight T w v`.
  set v := quantileV T w t with hvk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w t⊢ 0 < w v
  have hfilt := quantileV_filter_nonempty T w t ht1 hw hsum hTnek:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonempty⊢ 0 < w v
  have hv_mem : v ∈ T := quantileV_mem T w t hfiltk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ T⊢ 0 < w v
  -- The lexicographic value of `v` is the minimum of the filtered image.
  have hvval : toLex v = ((T.filter (fun u => t ≤ cumWeight T w u)).image toLex).min'
      (byk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ T⊢ (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).Nonempty simpa using hfilt.image toLexAll goals completed! 🐙) := byk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonempty⊢ 0 < w (quantileV T w t)
    rw [hv]k:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ T⊢ toLex (quantileV T w t) = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯; unfold quantileVk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ T⊢ toLex
    (if h : {v ∈ T | t ≤ cumWeight T w v}.Nonempty then
      ofLex ((Finset.image (⇑toLex) ({v ∈ T | t ≤ cumWeight T w v})).min' ⋯)
    else 0) =
  (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯; rw [dif_pos hfilt]k:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ T⊢ toLex (ofLex ((Finset.image (⇑toLex) ({v ∈ T | t ≤ cumWeight T w v})).min' ⋯)) =
  (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯; rflAll goals completed! 🐙
  have hv_cum : t ≤ cumWeight T w v := byk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonempty⊢ 0 < w (quantileV T w t)
    have hmem := Finset.min'_mem ((T.filter (fun u => t ≤ cumWeight T w u)).image toLex)
      (byk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯⊢ (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).Nonempty simpa using hfilt.image toLexAll goals completed! 🐙)
    rw [← hvval] at hmemk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hmem:toLex v ∈ Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})⊢ t ≤ cumWeight T w v
    obtain ⟨u, hu, hu_eq⟩ := Finset.mem_image.mp hmemk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hmem:toLex v ∈ Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})u:Fin k → ℝhu:u ∈ {u ∈ T | t ≤ cumWeight T w u}hu_eq:toLex u = toLex v⊢ t ≤ cumWeight T w v
    have huv : u = v := toLex.injective hu_eqk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hmem:toLex v ∈ Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})u:Fin k → ℝhu:u ∈ {u ∈ T | t ≤ cumWeight T w u}hu_eq:toLex u = toLex vhuv:u = v⊢ t ≤ cumWeight T w v
    rw [← huv]k:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hmem:toLex v ∈ Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})u:Fin k → ℝhu:u ∈ {u ∈ T | t ≤ cumWeight T w u}hu_eq:toLex u = toLex vhuv:u = v⊢ t ≤ cumWeight T w u; exact (Finset.mem_filter.mp hu).2All goals completed! 🐙
  -- `v` is lexicographically minimal in the filter: any `u ∈ T` with `toLex u < toLex v`
  -- is NOT in the filter, so `cumWeight T w u < t`.
  have h_min : ∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < t := byk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonempty⊢ 0 < w (quantileV T w t)
    intro u huk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vu:Fin k → ℝhu:u ∈ T⊢ u ≠ v → toLex u < toLex v → cumWeight T w u < t _k:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vu:Fin k → ℝhu:u ∈ Ta✝:u ≠ v⊢ toLex u < toLex v → cumWeight T w u < t hltk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vu:Fin k → ℝhu:u ∈ Ta✝:u ≠ vhlt:toLex u < toLex v⊢ cumWeight T w u < t
    by_contra hk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vu:Fin k → ℝhu:u ∈ Ta✝:u ≠ vhlt:toLex u < toLex vh:¬cumWeight T w u < t⊢ False
    rw [not_lt] at hk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vu:Fin k → ℝhu:u ∈ Ta✝:u ≠ vhlt:toLex u < toLex vh:t ≤ cumWeight T w u⊢ False
    have hmem : toLex u ∈ (T.filter (fun v => t ≤ cumWeight T w v)).image toLex :=
      Finset.mem_image.mpr ⟨u, Finset.mem_filter.mpr ⟨hu, h⟩, rfl⟩k:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vu:Fin k → ℝhu:u ∈ Ta✝:u ≠ vhlt:toLex u < toLex vh:t ≤ cumWeight T w uhmem:toLex u ∈ Finset.image (⇑toLex) ({v ∈ T | t ≤ cumWeight T w v})⊢ False
    have hle := Finset.min'_le _ _ hmemk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vu:Fin k → ℝhu:u ∈ Ta✝:u ≠ vhlt:toLex u < toLex vh:t ≤ cumWeight T w uhmem:toLex u ∈ Finset.image (⇑toLex) ({v ∈ T | t ≤ cumWeight T w v})hle:(Finset.image (⇑toLex) ({v ∈ T | t ≤ cumWeight T w v})).min' ⋯ ≤ toLex u⊢ False
    rw [← hvval] at hlek:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vu:Fin k → ℝhu:u ∈ Ta✝:u ≠ vhlt:toLex u < toLex vh:t ≤ cumWeight T w uhmem:toLex u ∈ Finset.image (⇑toLex) ({v ∈ T | t ≤ cumWeight T w v})hle:toLex v ≤ toLex u⊢ False
    exact absurd hle (not_le.mpr hlt)All goals completed! 🐙
  -- Write `P := T.filter (fun u => toLex u < toLex v)`. Claim `∑ u ∈ P, w u < t`.
  set P := T.filter (fun u => toLex u < toLex v) with hPk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}⊢ 0 < w v
  have hP_sum : ∑ u ∈ P, w u < t := byk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonempty⊢ 0 < w (quantileV T w t)
    by_cases hP_empty : P.Nonemptyposk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_empty:P.Nonempty⊢ ∑ u ∈ P, w u < tnegk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_empty:¬P.Nonempty⊢ ∑ u ∈ P, w u < t
    ·posk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_empty:P.Nonempty⊢ ∑ u ∈ P, w u < t obtain ⟨u_star, hu_star⟩ : ∃ u_star ∈ P, ∀ u ∈ P, toLex u ≤ toLex u_star := byk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_empty:P.Nonempty⊢ ∃ u_star ∈ P, ∀ u ∈ P, toLex u ≤ toLex u_star
        exact Finset.exists_max_image _ _ hP_emptyAll goals completed! 🐙
      have hus_mem : u_star ∈ T.filter (fun u => toLex u < toLex v) := hP ▸ hu_star.1posk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_empty:P.Nonemptyu_star:Fin k → ℝhu_star:u_star ∈ P ∧ ∀ u ∈ P, toLex u ≤ toLex u_starhus_mem:u_star ∈ {u ∈ T | toLex u < toLex v}⊢ ∑ u ∈ P, w u < t
      have hus_lt : toLex u_star < toLex v := (Finset.mem_filter.mp hus_mem).2posk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_empty:P.Nonemptyu_star:Fin k → ℝhu_star:u_star ∈ P ∧ ∀ u ∈ P, toLex u ≤ toLex u_starhus_mem:u_star ∈ {u ∈ T | toLex u < toLex v}hus_lt:toLex u_star < toLex v⊢ ∑ u ∈ P, w u < t
      have hP_eq : T.filter (fun u => toLex u ≤ toLex u_star) = P := byk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonempty⊢ 0 < w (quantileV T w t)
        rw [hP]k:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_empty:P.Nonemptyu_star:Fin k → ℝhu_star:u_star ∈ P ∧ ∀ u ∈ P, toLex u ≤ toLex u_starhus_mem:u_star ∈ {u ∈ T | toLex u < toLex v}hus_lt:toLex u_star < toLex v⊢ {u ∈ T | toLex u ≤ toLex u_star} = {u ∈ T | toLex u < toLex v}
        ext uhk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_empty:P.Nonemptyu_star:Fin k → ℝhu_star:u_star ∈ P ∧ ∀ u ∈ P, toLex u ≤ toLex u_starhus_mem:u_star ∈ {u ∈ T | toLex u < toLex v}hus_lt:toLex u_star < toLex vu:Fin k → ℝ⊢ u ∈ {u ∈ T | toLex u ≤ toLex u_star} ↔ u ∈ {u ∈ T | toLex u < toLex v}
        simp only [Finset.mem_filter]hk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_empty:P.Nonemptyu_star:Fin k → ℝhu_star:u_star ∈ P ∧ ∀ u ∈ P, toLex u ≤ toLex u_starhus_mem:u_star ∈ {u ∈ T | toLex u < toLex v}hus_lt:toLex u_star < toLex vu:Fin k → ℝ⊢ u ∈ T ∧ toLex u ≤ toLex u_star ↔ u ∈ T ∧ toLex u < toLex v
        constructorh.mpk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_empty:P.Nonemptyu_star:Fin k → ℝhu_star:u_star ∈ P ∧ ∀ u ∈ P, toLex u ≤ toLex u_starhus_mem:u_star ∈ {u ∈ T | toLex u < toLex v}hus_lt:toLex u_star < toLex vu:Fin k → ℝ⊢ u ∈ T ∧ toLex u ≤ toLex u_star → u ∈ T ∧ toLex u < toLex vh.mprk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_empty:P.Nonemptyu_star:Fin k → ℝhu_star:u_star ∈ P ∧ ∀ u ∈ P, toLex u ≤ toLex u_starhus_mem:u_star ∈ {u ∈ T | toLex u < toLex v}hus_lt:toLex u_star < toLex vu:Fin k → ℝ⊢ u ∈ T ∧ toLex u < toLex v → u ∈ T ∧ toLex u ≤ toLex u_star
        ·h.mpk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_empty:P.Nonemptyu_star:Fin k → ℝhu_star:u_star ∈ P ∧ ∀ u ∈ P, toLex u ≤ toLex u_starhus_mem:u_star ∈ {u ∈ T | toLex u < toLex v}hus_lt:toLex u_star < toLex vu:Fin k → ℝ⊢ u ∈ T ∧ toLex u ≤ toLex u_star → u ∈ T ∧ toLex u < toLex v rintro ⟨huT, hule⟩h.mpk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_empty:P.Nonemptyu_star:Fin k → ℝhu_star:u_star ∈ P ∧ ∀ u ∈ P, toLex u ≤ toLex u_starhus_mem:u_star ∈ {u ∈ T | toLex u < toLex v}hus_lt:toLex u_star < toLex vu:Fin k → ℝhuT:u ∈ Thule:toLex u ≤ toLex u_star⊢ u ∈ T ∧ toLex u < toLex v
          exact ⟨huT, lt_of_le_of_lt hule hus_lt⟩All goals completed! 🐙
        ·h.mprk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_empty:P.Nonemptyu_star:Fin k → ℝhu_star:u_star ∈ P ∧ ∀ u ∈ P, toLex u ≤ toLex u_starhus_mem:u_star ∈ {u ∈ T | toLex u < toLex v}hus_lt:toLex u_star < toLex vu:Fin k → ℝ⊢ u ∈ T ∧ toLex u < toLex v → u ∈ T ∧ toLex u ≤ toLex u_star rintro ⟨huT, hult⟩h.mprk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_empty:P.Nonemptyu_star:Fin k → ℝhu_star:u_star ∈ P ∧ ∀ u ∈ P, toLex u ≤ toLex u_starhus_mem:u_star ∈ {u ∈ T | toLex u < toLex v}hus_lt:toLex u_star < toLex vu:Fin k → ℝhuT:u ∈ Thult:toLex u < toLex v⊢ u ∈ T ∧ toLex u ≤ toLex u_star
          refine ⟨huT, hu_star.2 u ?_⟩h.mprk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_empty:P.Nonemptyu_star:Fin k → ℝhu_star:u_star ∈ P ∧ ∀ u ∈ P, toLex u ≤ toLex u_starhus_mem:u_star ∈ {u ∈ T | toLex u < toLex v}hus_lt:toLex u_star < toLex vu:Fin k → ℝhuT:u ∈ Thult:toLex u < toLex v⊢ u ∈ P
          rw [hP]h.mprk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_empty:P.Nonemptyu_star:Fin k → ℝhu_star:u_star ∈ P ∧ ∀ u ∈ P, toLex u ≤ toLex u_starhus_mem:u_star ∈ {u ∈ T | toLex u < toLex v}hus_lt:toLex u_star < toLex vu:Fin k → ℝhuT:u ∈ Thult:toLex u < toLex v⊢ u ∈ {u ∈ T | toLex u < toLex v}; exact Finset.mem_filter.mpr ⟨huT, hult⟩All goals completed! 🐙
      have hne : u_star ≠ v := fun h => absurd hus_lt (h ▸ lt_irrefl _)posk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_empty:P.Nonemptyu_star:Fin k → ℝhu_star:u_star ∈ P ∧ ∀ u ∈ P, toLex u ≤ toLex u_starhus_mem:u_star ∈ {u ∈ T | toLex u < toLex v}hus_lt:toLex u_star < toLex vhP_eq:{u ∈ T | toLex u ≤ toLex u_star} = Phne:u_star ≠ v⊢ ∑ u ∈ P, w u < t
      convert h_min u_star (Finset.mem_filter.mp hus_mem).1 hne hus_lt using 1h.e'_3k:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_empty:P.Nonemptyu_star:Fin k → ℝhu_star:u_star ∈ P ∧ ∀ u ∈ P, toLex u ≤ toLex u_starhus_mem:u_star ∈ {u ∈ T | toLex u < toLex v}hus_lt:toLex u_star < toLex vhP_eq:{u ∈ T | toLex u ≤ toLex u_star} = Phne:u_star ≠ v⊢ ∑ u ∈ P, w u = cumWeight T w u_star
      rw [cumWeight, hP_eq]All goals completed! 🐙
    ·negk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_empty:¬P.Nonempty⊢ ∑ u ∈ P, w u < t rw [Finset.not_nonempty_iff_eq_empty.mp hP_empty, Finset.sum_empty]negk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_empty:¬P.Nonempty⊢ 0 < t; linarithAll goals completed! 🐙
  -- Split `cumWeight T w v = (∑ u ∈ P, w u) + w v`.
  have hsplit_set : (Finset.filter (fun u => toLex u ≤ toLex v) T) = P ∪ {v} := byk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonempty⊢ 0 < w (quantileV T w t)
    rw [hP]k:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_sum:∑ u ∈ P, w u < t⊢ {u ∈ T | toLex u ≤ toLex v} = {u ∈ T | toLex u < toLex v} ∪ {v}
    ext uhk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_sum:∑ u ∈ P, w u < tu:Fin k → ℝ⊢ u ∈ {u ∈ T | toLex u ≤ toLex v} ↔ u ∈ {u ∈ T | toLex u < toLex v} ∪ {v}
    simp only [Finset.mem_filter, Finset.mem_union, Finset.mem_singleton]hk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_sum:∑ u ∈ P, w u < tu:Fin k → ℝ⊢ u ∈ T ∧ toLex u ≤ toLex v ↔ u ∈ T ∧ toLex u < toLex v ∨ u = v
    constructorh.mpk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_sum:∑ u ∈ P, w u < tu:Fin k → ℝ⊢ u ∈ T ∧ toLex u ≤ toLex v → u ∈ T ∧ toLex u < toLex v ∨ u = vh.mprk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_sum:∑ u ∈ P, w u < tu:Fin k → ℝ⊢ u ∈ T ∧ toLex u < toLex v ∨ u = v → u ∈ T ∧ toLex u ≤ toLex v
    ·h.mpk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_sum:∑ u ∈ P, w u < tu:Fin k → ℝ⊢ u ∈ T ∧ toLex u ≤ toLex v → u ∈ T ∧ toLex u < toLex v ∨ u = v rintro ⟨huT, hule⟩h.mpk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_sum:∑ u ∈ P, w u < tu:Fin k → ℝhuT:u ∈ Thule:toLex u ≤ toLex v⊢ u ∈ T ∧ toLex u < toLex v ∨ u = v
      rcases lt_or_eq_of_le hule with h | hh.mp.inlk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_sum:∑ u ∈ P, w u < tu:Fin k → ℝhuT:u ∈ Thule:toLex u ≤ toLex vh:toLex u < toLex v⊢ u ∈ T ∧ toLex u < toLex v ∨ u = vh.mp.inrk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_sum:∑ u ∈ P, w u < tu:Fin k → ℝhuT:u ∈ Thule:toLex u ≤ toLex vh:toLex u = toLex v⊢ u ∈ T ∧ toLex u < toLex v ∨ u = v
      ·h.mp.inlk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_sum:∑ u ∈ P, w u < tu:Fin k → ℝhuT:u ∈ Thule:toLex u ≤ toLex vh:toLex u < toLex v⊢ u ∈ T ∧ toLex u < toLex v ∨ u = v exact Or.inl ⟨huT, h⟩All goals completed! 🐙
      ·h.mp.inrk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_sum:∑ u ∈ P, w u < tu:Fin k → ℝhuT:u ∈ Thule:toLex u ≤ toLex vh:toLex u = toLex v⊢ u ∈ T ∧ toLex u < toLex v ∨ u = v exact Or.inr (toLex.injective h)All goals completed! 🐙
    ·h.mprk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_sum:∑ u ∈ P, w u < tu:Fin k → ℝ⊢ u ∈ T ∧ toLex u < toLex v ∨ u = v → u ∈ T ∧ toLex u ≤ toLex v rintro (⟨huT, hult⟩ | rfl)h.mpr.inlk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_sum:∑ u ∈ P, w u < tu:Fin k → ℝhuT:u ∈ Thult:toLex u < toLex v⊢ u ∈ T ∧ toLex u ≤ toLex vh.mpr.inrk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_sum:∑ u ∈ P, w u < t⊢ v ∈ T ∧ toLex v ≤ toLex v
      ·h.mpr.inlk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_sum:∑ u ∈ P, w u < tu:Fin k → ℝhuT:u ∈ Thult:toLex u < toLex v⊢ u ∈ T ∧ toLex u ≤ toLex v exact ⟨huT, le_of_lt hult⟩All goals completed! 🐙
      ·h.mpr.inrk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_sum:∑ u ∈ P, w u < t⊢ v ∈ T ∧ toLex v ≤ toLex v exact ⟨hv_mem, le_refl _⟩All goals completed! 🐙
  have hdisj : Disjoint P {v} := byk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonempty⊢ 0 < w (quantileV T w t)
    rw [Finset.disjoint_singleton_right, hP]k:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_sum:∑ u ∈ P, w u < thsplit_set:{u ∈ T | toLex u ≤ toLex v} = P ∪ {v}⊢ v ∉ {u ∈ T | toLex u < toLex v}
    intro hmemk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_sum:∑ u ∈ P, w u < thsplit_set:{u ∈ T | toLex u ≤ toLex v} = P ∪ {v}hmem:v ∈ {u ∈ T | toLex u < toLex v}⊢ False
    exact lt_irrefl _ (Finset.mem_filter.mp hmem).2All goals completed! 🐙
  have h_cum_split : cumWeight T w v = (∑ u ∈ P, w u) + w v := byk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonempty⊢ 0 < w (quantileV T w t)
    unfold cumWeightk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonemptyv:Fin k → ℝ := quantileV T w thv:v = quantileV T w thfilt:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv_mem:v ∈ Thvval:toLex v = (Finset.image (⇑toLex) ({u ∈ T | t ≤ cumWeight T w u})).min' ⋯hv_cum:t ≤ cumWeight T w vh_min:∀ u ∈ T, u ≠ v → toLex u < toLex v → cumWeight T w u < tP:Finset (Fin k → ℝ) := {u ∈ T | toLex u < toLex v}hP:P = {u ∈ T | toLex u < toLex v}hP_sum:∑ u ∈ P, w u < thsplit_set:{u ∈ T | toLex u ≤ toLex v} = P ∪ {v}hdisj:Disjoint P {v}⊢ ∑ u ∈ T with toLex u ≤ toLex v, w u = ∑ u ∈ P, w u + w v
    rw [hsplit_set, Finset.sum_union hdisj, Finset.sum_singleton]All goals completed! 🐙
  linarithAll goals completed! 🐙

/-
**Support membership.** With nonnegative weights summing to `1` and `0 < t ≤ 1`, the
quantile vertex is a support vertex: it lies in the positive-weight subset of `T`.
-/
lemma quantileV_mem_support (T : Finset (Fin k → ℝ)) (w : (Fin k → ℝ) → ℝ) (t : ℝ)
    (ht0 : 0 < t) (ht1 : t ≤ 1) (hw : ∀ v ∈ T, 0 ≤ w v) (hsum : ∑ v ∈ T, w v = 1)
    (hTne : T.Nonempty) :
    quantileV T w t ∈ T.filter (fun v => 0 < w v) := byk:ℕT:Finset (Fin k → ℝ)w:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hTne:T.Nonempty⊢ quantileV T w t ∈ {v ∈ T | 0 < w v}
  exact Finset.mem_filter.mpr ⟨ quantileV_mem T w t ( quantileV_filter_nonempty T w t ht1 hw hsum hTne ), quantileV_weight_pos T w t ht0 ht1 hw hsum hTne ⟩All goals completed! 🐙

Lemma 5.2.2🔗

Lemma 5.2.2 (the quantile depends only on the support). Let \delta \subseteq \sigma, with w as in Lemma 5.2.1 and w(u) = 0 for every u \in \sigma \smallsetminus \delta, \delta \ne \emptyset, 0 < t \le 1. Then \mathrm{qv}_\sigma(w,t) = \mathrm{qv}_\delta(w,t).

Proof. For v \in \delta, \mathrm{cum}_\delta(w,v) = \mathrm{cum}_\sigma(w,v) (the discarded terms vanish). The vertex v_0 := \mathrm{qv}_\sigma(w,t) has positive weight (Lemma 5.2.1), hence lies in \delta; it satisfies the threshold inequality with respect to \delta as well, and it is \preceq-minimal among vertices of \delta satisfying it (being minimal even in the larger \sigma). So it is the quantile vertex of \delta. \blacksquare

/-
**The quantile depends only on the support.** If `S ⊆ T` carries all the weight
(`w` vanishes off `S` within `T`), then the quantile vertex computed over `T` equals the one
computed over `S`.  This is the key to cross-simplex consistency of the labelling.
-/
set_option maxHeartbeats 1600000 in
lemma quantileV_eq_of_support_subset
    {S T : Finset (Fin k → ℝ)} (hST : S ⊆ T)
    (w : (Fin k → ℝ) → ℝ) (t : ℝ)
    (ht0 : 0 < t) (ht1 : t ≤ 1)
    (hw : ∀ v ∈ T, 0 ≤ w v) (hsum : ∑ v ∈ T, w v = 1) (hSne : S.Nonempty)
    (hsupp : ∀ v ∈ T, v ∉ S → w v = 0) :
    quantileV T w t = quantileV S w t := byk:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0⊢ quantileV T w t = quantileV S w t
  -- By definition of `cumWeight`, we know that `cumWeight S w v = cumWeight T w v` for all `v ∈ S`.
  have h_cumWeight_eq : ∀ v ∈ S, cumWeight S w v = cumWeight T w v := byk:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0⊢ quantileV T w t = quantileV S w t
    intro v hvk:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0v:Fin k → ℝhv:v ∈ S⊢ cumWeight S w v = cumWeight T w v; unfold cumWeightk:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0v:Fin k → ℝhv:v ∈ S⊢ ∑ u ∈ S with toLex u ≤ toLex v, w u = ∑ u ∈ T with toLex u ≤ toLex v, w u; rw [ Finset.sum_subset ( Finset.filter_subset_filter _ hST ) ]k:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0v:Fin k → ℝhv:v ∈ S⊢ ∀ x ∈ {u ∈ T | toLex u ≤ toLex v}, x ∉ {u ∈ S | toLex u ≤ toLex v} → w x = 0 ; aesopAll goals completed! 🐙;
  -- Let `v₀ := quantileV T w t`. Then `v₀ ∈ T` (`quantileV_mem`) and `0 < w v₀` (`quantileV_weight_pos`), so `v₀ ∈ S` (else `hsupp` gives `w v₀ = 0`).
  set v₀ := quantileV T w t with hv₀k:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0h_cumWeight_eq:∀ v ∈ S, cumWeight S w v = cumWeight T w vv₀:Fin k → ℝ := quantileV T w thv₀:v₀ = quantileV T w t⊢ v₀ = quantileV S w t
  have hv₀_T : v₀ ∈ T := byk:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0⊢ quantileV T w t = quantileV S w t
    exact quantileV_mem T w t ( quantileV_filter_nonempty T w t ht1 hw hsum ( hSne.mono hST ) )All goals completed! 🐙
  have hv₀_S : v₀ ∈ S := byk:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0⊢ quantileV T w t = quantileV S w t
    exact Classical.not_not.1 fun h => absurd ( quantileV_weight_pos T w t ht0 ht1 hw hsum ( Finset.nonempty_of_ne_empty ( byk:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0h_cumWeight_eq:∀ v ∈ S, cumWeight S w v = cumWeight T w vv₀:Fin k → ℝ := quantileV T w thv₀:v₀ = quantileV T w thv₀_T:v₀ ∈ Th:v₀ ∉ S⊢ T ≠ ∅ aesop_catAll goals completed! 🐙 ) ) ) ( byk:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0h_cumWeight_eq:∀ v ∈ S, cumWeight S w v = cumWeight T w vv₀:Fin k → ℝ := quantileV T w thv₀:v₀ = quantileV T w thv₀_T:v₀ ∈ Th:v₀ ∉ S⊢ ¬0 < w (quantileV T w t) aesopAll goals completed! 🐙 )
  have hv₀_cum : t ≤ cumWeight T w v₀ := byk:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0⊢ quantileV T w t = quantileV S w t
    unfold quantileV at hv₀k:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0h_cumWeight_eq:∀ v ∈ S, cumWeight S w v = cumWeight T w vv₀:Fin k → ℝ := quantileV T w thv₀:v₀ =
  if h : {v ∈ T | t ≤ cumWeight T w v}.Nonempty then
    ofLex ((Finset.image (⇑toLex) ({v ∈ T | t ≤ cumWeight T w v})).min' ⋯)
  else 0hv₀_T:v₀ ∈ Thv₀_S:v₀ ∈ S⊢ t ≤ cumWeight T w v₀;
    split_ifs at hv₀posk:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0h_cumWeight_eq:∀ v ∈ S, cumWeight S w v = cumWeight T w vv₀:Fin k → ℝ := quantileV T w thv₀_T:v₀ ∈ Thv₀_S:v₀ ∈ Sh✝:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv₀:v₀ = ofLex ((Finset.image (⇑toLex) ({v ∈ T | t ≤ cumWeight T w v})).min' ⋯)⊢ t ≤ cumWeight T w v₀negk:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0h_cumWeight_eq:∀ v ∈ S, cumWeight S w v = cumWeight T w vv₀:Fin k → ℝ := quantileV T w thv₀_T:v₀ ∈ Thv₀_S:v₀ ∈ Sh✝:¬{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv₀:v₀ = 0⊢ t ≤ cumWeight T w v₀;
    ·posk:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0h_cumWeight_eq:∀ v ∈ S, cumWeight S w v = cumWeight T w vv₀:Fin k → ℝ := quantileV T w thv₀_T:v₀ ∈ Thv₀_S:v₀ ∈ Sh✝:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv₀:v₀ = ofLex ((Finset.image (⇑toLex) ({v ∈ T | t ≤ cumWeight T w v})).min' ⋯)⊢ t ≤ cumWeight T w v₀ have := Finset.min'_mem ( Finset.image toLex ( Finset.filter ( fun v => t ≤ cumWeight T w v ) T ) )posk:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0h_cumWeight_eq:∀ v ∈ S, cumWeight S w v = cumWeight T w vv₀:Fin k → ℝ := quantileV T w thv₀_T:v₀ ∈ Thv₀_S:v₀ ∈ Sh✝:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv₀:v₀ = ofLex ((Finset.image (⇑toLex) ({v ∈ T | t ≤ cumWeight T w v})).min' ⋯)this:∀ (H : (Finset.image (⇑toLex) ({v ∈ T | t ≤ cumWeight T w v})).Nonempty),
  (Finset.image (⇑toLex) ({v ∈ T | t ≤ cumWeight T w v})).min' H ∈ Finset.image (⇑toLex) ({v ∈ T | t ≤ cumWeight T w v})⊢ t ≤ cumWeight T w v₀ ; aesopAll goals completed! 🐙;
    ·negk:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0h_cumWeight_eq:∀ v ∈ S, cumWeight S w v = cumWeight T w vv₀:Fin k → ℝ := quantileV T w thv₀_T:v₀ ∈ Thv₀_S:v₀ ∈ Sh✝:¬{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv₀:v₀ = 0⊢ t ≤ cumWeight T w v₀ exact False.elim <| ‹¬Finset.Nonempty { v ∈ T | t ≤ cumWeight T w v } › <| quantileV_filter_nonempty T w t ht1 hw hsum <| Finset.nonempty_of_ne_empty <| byk:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0h_cumWeight_eq:∀ v ∈ S, cumWeight S w v = cumWeight T w vv₀:Fin k → ℝ := quantileV T w thv₀_T:v₀ ∈ Thv₀_S:v₀ ∈ Sh✝:¬{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv₀:v₀ = 0⊢ T ≠ ∅ aesop_catAll goals completed! 🐙;
  have hv₀_pos : 0 < w v₀ := byk:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0⊢ quantileV T w t = quantileV S w t
    apply quantileV_weight_pos T w t ht0 ht1 hw hsum (Finset.Nonempty.mono hST hSne)All goals completed! 🐙;
  -- By definition of `quantileV`, we know that `quantileV S w t` is the minimum element in `S` such that `t ≤ cumWeight S w v`.
  have hv₀_min : ∀ v ∈ S, t ≤ cumWeight S w v → toLex v₀ ≤ toLex v := byk:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0⊢ quantileV T w t = quantileV S w t
    unfold quantileV at *k:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0h_cumWeight_eq:∀ v ∈ S, cumWeight S w v = cumWeight T w vv₀:Fin k → ℝ := quantileV T w thv₀:v₀ =
  if h : {v ∈ T | t ≤ cumWeight T w v}.Nonempty then
    ofLex ((Finset.image (⇑toLex) ({v ∈ T | t ≤ cumWeight T w v})).min' ⋯)
  else 0hv₀_T:v₀ ∈ Thv₀_S:v₀ ∈ Shv₀_cum:t ≤ cumWeight T w v₀hv₀_pos:0 < w v₀⊢ ∀ v ∈ S, t ≤ cumWeight S w v → toLex v₀ ≤ toLex v; split_ifs at hv₀posk:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0h_cumWeight_eq:∀ v ∈ S, cumWeight S w v = cumWeight T w vv₀:Fin k → ℝ := quantileV T w thv₀_T:v₀ ∈ Thv₀_S:v₀ ∈ Shv₀_cum:t ≤ cumWeight T w v₀hv₀_pos:0 < w v₀h✝:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv₀:v₀ = ofLex ((Finset.image (⇑toLex) ({v ∈ T | t ≤ cumWeight T w v})).min' ⋯)⊢ ∀ v ∈ S, t ≤ cumWeight S w v → toLex v₀ ≤ toLex vnegk:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0h_cumWeight_eq:∀ v ∈ S, cumWeight S w v = cumWeight T w vv₀:Fin k → ℝ := quantileV T w thv₀_T:v₀ ∈ Thv₀_S:v₀ ∈ Shv₀_cum:t ≤ cumWeight T w v₀hv₀_pos:0 < w v₀h✝:¬{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv₀:v₀ = 0⊢ ∀ v ∈ S, t ≤ cumWeight S w v → toLex v₀ ≤ toLex v ; simp_all +decide [ Finset.min' ]posk:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0h_cumWeight_eq:∀ v ∈ S, cumWeight S w v = cumWeight T w vv₀:Fin k → ℝ := quantileV T w th✝:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv₀_T:ofLex ({v ∈ T | t ≤ cumWeight T w v}.inf' ⋯ fun x => toLex x) ∈ Thv₀_S:ofLex ({v ∈ T | t ≤ cumWeight T w v}.inf' ⋯ fun x => toLex x) ∈ Shv₀_cum:t ≤ cumWeight T w (ofLex ({v ∈ T | t ≤ cumWeight T w v}.inf' ⋯ fun x => toLex x))hv₀_pos:0 < w (ofLex ({v ∈ T | t ≤ cumWeight T w v}.inf' ⋯ fun x => toLex x))hv₀:v₀ = ofLex ({v ∈ T | t ≤ cumWeight T w v}.inf' ⋯ fun x => toLex x)⊢ ∀ v ∈ S, t ≤ cumWeight T w v → ∃ b, (b ∈ T ∧ t ≤ cumWeight T w b) ∧ toLex b ≤ toLex vnegk:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0h_cumWeight_eq:∀ v ∈ S, cumWeight S w v = cumWeight T w vv₀:Fin k → ℝ := quantileV T w thv₀_T:v₀ ∈ Thv₀_S:v₀ ∈ Shv₀_cum:t ≤ cumWeight T w v₀hv₀_pos:0 < w v₀h✝:¬{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv₀:v₀ = 0⊢ ∀ v ∈ S, t ≤ cumWeight S w v → toLex v₀ ≤ toLex v ;
    ·posk:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0h_cumWeight_eq:∀ v ∈ S, cumWeight S w v = cumWeight T w vv₀:Fin k → ℝ := quantileV T w th✝:{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv₀_T:ofLex ({v ∈ T | t ≤ cumWeight T w v}.inf' ⋯ fun x => toLex x) ∈ Thv₀_S:ofLex ({v ∈ T | t ≤ cumWeight T w v}.inf' ⋯ fun x => toLex x) ∈ Shv₀_cum:t ≤ cumWeight T w (ofLex ({v ∈ T | t ≤ cumWeight T w v}.inf' ⋯ fun x => toLex x))hv₀_pos:0 < w (ofLex ({v ∈ T | t ≤ cumWeight T w v}.inf' ⋯ fun x => toLex x))hv₀:v₀ = ofLex ({v ∈ T | t ≤ cumWeight T w v}.inf' ⋯ fun x => toLex x)⊢ ∀ v ∈ S, t ≤ cumWeight T w v → ∃ b, (b ∈ T ∧ t ≤ cumWeight T w b) ∧ toLex b ≤ toLex v exact fun v hv hv' => ⟨ v, ⟨ hST hv, hv' ⟩, le_rfl ⟩All goals completed! 🐙;
    ·negk:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0h_cumWeight_eq:∀ v ∈ S, cumWeight S w v = cumWeight T w vv₀:Fin k → ℝ := quantileV T w thv₀_T:v₀ ∈ Thv₀_S:v₀ ∈ Shv₀_cum:t ≤ cumWeight T w v₀hv₀_pos:0 < w v₀h✝:¬{v ∈ T | t ≤ cumWeight T w v}.Nonemptyhv₀:v₀ = 0⊢ ∀ v ∈ S, t ≤ cumWeight S w v → toLex v₀ ≤ toLex v exact False.elim <| ‹¬ { v ∈ T | t ≤ cumWeight T w v }.Nonempty› ⟨ v₀, Finset.mem_filter.mpr ⟨ hv₀_T, hv₀_cum ⟩ ⟩All goals completed! 🐙;
  unfold quantileVk:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0h_cumWeight_eq:∀ v ∈ S, cumWeight S w v = cumWeight T w vv₀:Fin k → ℝ := quantileV T w thv₀:v₀ = quantileV T w thv₀_T:v₀ ∈ Thv₀_S:v₀ ∈ Shv₀_cum:t ≤ cumWeight T w v₀hv₀_pos:0 < w v₀hv₀_min:∀ v ∈ S, t ≤ cumWeight S w v → toLex v₀ ≤ toLex v⊢ v₀ =
  if h : {v ∈ S | t ≤ cumWeight S w v}.Nonempty then
    ofLex ((Finset.image (⇑toLex) ({v ∈ S | t ≤ cumWeight S w v})).min' ⋯)
  else 0;
  split_ifsposk:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0h_cumWeight_eq:∀ v ∈ S, cumWeight S w v = cumWeight T w vv₀:Fin k → ℝ := quantileV T w thv₀:v₀ = quantileV T w thv₀_T:v₀ ∈ Thv₀_S:v₀ ∈ Shv₀_cum:t ≤ cumWeight T w v₀hv₀_pos:0 < w v₀hv₀_min:∀ v ∈ S, t ≤ cumWeight S w v → toLex v₀ ≤ toLex vh✝:{v ∈ S | t ≤ cumWeight S w v}.Nonempty⊢ v₀ = ofLex ((Finset.image (⇑toLex) ({v ∈ S | t ≤ cumWeight S w v})).min' ⋯)negk:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0h_cumWeight_eq:∀ v ∈ S, cumWeight S w v = cumWeight T w vv₀:Fin k → ℝ := quantileV T w thv₀:v₀ = quantileV T w thv₀_T:v₀ ∈ Thv₀_S:v₀ ∈ Shv₀_cum:t ≤ cumWeight T w v₀hv₀_pos:0 < w v₀hv₀_min:∀ v ∈ S, t ≤ cumWeight S w v → toLex v₀ ≤ toLex vh✝:¬{v ∈ S | t ≤ cumWeight S w v}.Nonempty⊢ v₀ = 0 <;>posk:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0h_cumWeight_eq:∀ v ∈ S, cumWeight S w v = cumWeight T w vv₀:Fin k → ℝ := quantileV T w thv₀:v₀ = quantileV T w thv₀_T:v₀ ∈ Thv₀_S:v₀ ∈ Shv₀_cum:t ≤ cumWeight T w v₀hv₀_pos:0 < w v₀hv₀_min:∀ v ∈ S, t ≤ cumWeight S w v → toLex v₀ ≤ toLex vh✝:{v ∈ S | t ≤ cumWeight S w v}.Nonempty⊢ v₀ = ofLex ((Finset.image (⇑toLex) ({v ∈ S | t ≤ cumWeight S w v})).min' ⋯)negk:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0h_cumWeight_eq:∀ v ∈ S, cumWeight S w v = cumWeight T w vv₀:Fin k → ℝ := quantileV T w thv₀:v₀ = quantileV T w thv₀_T:v₀ ∈ Thv₀_S:v₀ ∈ Shv₀_cum:t ≤ cumWeight T w v₀hv₀_pos:0 < w v₀hv₀_min:∀ v ∈ S, t ≤ cumWeight S w v → toLex v₀ ≤ toLex vh✝:¬{v ∈ S | t ≤ cumWeight S w v}.Nonempty⊢ v₀ = 0 simp_all +decide [ Finset.min' ]negk:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0h_cumWeight_eq:∀ v ∈ S, cumWeight S w v = cumWeight T w vv₀:Fin k → ℝ := quantileV T w thv₀:v₀ = quantileV T w thv₀_T:quantileV T w t ∈ Thv₀_S:quantileV T w t ∈ Shv₀_cum:t ≤ cumWeight T w (quantileV T w t)hv₀_pos:0 < w (quantileV T w t)h✝:∀ ⦃x : Fin k → ℝ⦄, x ∈ S → cumWeight T w x < t⊢ quantileV T w t = 0;
  ·posk:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0h_cumWeight_eq:∀ v ∈ S, cumWeight S w v = cumWeight T w vv₀:Fin k → ℝ := quantileV T w thv₀:v₀ = quantileV T w th✝:{v ∈ S | t ≤ cumWeight S w v}.Nonemptyhv₀_T:quantileV T w t ∈ Thv₀_S:quantileV T w t ∈ Shv₀_cum:t ≤ cumWeight T w (quantileV T w t)hv₀_pos:0 < w (quantileV T w t)hv₀_min:∀ v ∈ S, t ≤ cumWeight T w v → toLex (quantileV T w t) ≤ toLex v⊢ quantileV T w t = ofLex ({x ∈ S | t ≤ cumWeight T w x}.inf' ⋯ fun x => toLex x) convert rflh.e'_3k:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0h_cumWeight_eq:∀ v ∈ S, cumWeight S w v = cumWeight T w vv₀:Fin k → ℝ := quantileV T w thv₀:v₀ = quantileV T w th✝:{v ∈ S | t ≤ cumWeight S w v}.Nonemptyhv₀_T:quantileV T w t ∈ Thv₀_S:quantileV T w t ∈ Shv₀_cum:t ≤ cumWeight T w (quantileV T w t)hv₀_pos:0 < w (quantileV T w t)hv₀_min:∀ v ∈ S, t ≤ cumWeight T w v → toLex (quantileV T w t) ≤ toLex v⊢ ofLex ({x ∈ S | t ≤ cumWeight T w x}.inf' ⋯ fun x => toLex x) = quantileV T w t;
    convert ofLex_toLex v₀h.e'_2.h.e'_6k:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0h_cumWeight_eq:∀ v ∈ S, cumWeight S w v = cumWeight T w vv₀:Fin k → ℝ := quantileV T w thv₀:v₀ = quantileV T w th✝:{v ∈ S | t ≤ cumWeight S w v}.Nonemptyhv₀_T:quantileV T w t ∈ Thv₀_S:quantileV T w t ∈ Shv₀_cum:t ≤ cumWeight T w (quantileV T w t)hv₀_pos:0 < w (quantileV T w t)hv₀_min:∀ v ∈ S, t ≤ cumWeight T w v → toLex (quantileV T w t) ≤ toLex v⊢ ({x ∈ S | t ≤ cumWeight T w x}.inf' ⋯ fun x => toLex x) = toLex v₀;
    refine' le_antisymm _ _h.e'_2.h.e'_6.refine'_1k:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0h_cumWeight_eq:∀ v ∈ S, cumWeight S w v = cumWeight T w vv₀:Fin k → ℝ := quantileV T w thv₀:v₀ = quantileV T w th✝:{v ∈ S | t ≤ cumWeight S w v}.Nonemptyhv₀_T:quantileV T w t ∈ Thv₀_S:quantileV T w t ∈ Shv₀_cum:t ≤ cumWeight T w (quantileV T w t)hv₀_pos:0 < w (quantileV T w t)hv₀_min:∀ v ∈ S, t ≤ cumWeight T w v → toLex (quantileV T w t) ≤ toLex v⊢ ({x ∈ S | t ≤ cumWeight T w x}.inf' ⋯ fun x => toLex x) ≤ toLex v₀h.e'_2.h.e'_6.refine'_2k:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0h_cumWeight_eq:∀ v ∈ S, cumWeight S w v = cumWeight T w vv₀:Fin k → ℝ := quantileV T w thv₀:v₀ = quantileV T w th✝:{v ∈ S | t ≤ cumWeight S w v}.Nonemptyhv₀_T:quantileV T w t ∈ Thv₀_S:quantileV T w t ∈ Shv₀_cum:t ≤ cumWeight T w (quantileV T w t)hv₀_pos:0 < w (quantileV T w t)hv₀_min:∀ v ∈ S, t ≤ cumWeight T w v → toLex (quantileV T w t) ≤ toLex v⊢ toLex v₀ ≤ {x ∈ S | t ≤ cumWeight T w x}.inf' ⋯ fun x => toLex x <;>h.e'_2.h.e'_6.refine'_1k:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0h_cumWeight_eq:∀ v ∈ S, cumWeight S w v = cumWeight T w vv₀:Fin k → ℝ := quantileV T w thv₀:v₀ = quantileV T w th✝:{v ∈ S | t ≤ cumWeight S w v}.Nonemptyhv₀_T:quantileV T w t ∈ Thv₀_S:quantileV T w t ∈ Shv₀_cum:t ≤ cumWeight T w (quantileV T w t)hv₀_pos:0 < w (quantileV T w t)hv₀_min:∀ v ∈ S, t ≤ cumWeight T w v → toLex (quantileV T w t) ≤ toLex v⊢ ({x ∈ S | t ≤ cumWeight T w x}.inf' ⋯ fun x => toLex x) ≤ toLex v₀h.e'_2.h.e'_6.refine'_2k:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0h_cumWeight_eq:∀ v ∈ S, cumWeight S w v = cumWeight T w vv₀:Fin k → ℝ := quantileV T w thv₀:v₀ = quantileV T w th✝:{v ∈ S | t ≤ cumWeight S w v}.Nonemptyhv₀_T:quantileV T w t ∈ Thv₀_S:quantileV T w t ∈ Shv₀_cum:t ≤ cumWeight T w (quantileV T w t)hv₀_pos:0 < w (quantileV T w t)hv₀_min:∀ v ∈ S, t ≤ cumWeight T w v → toLex (quantileV T w t) ≤ toLex v⊢ toLex v₀ ≤ {x ∈ S | t ≤ cumWeight T w x}.inf' ⋯ fun x => toLex x simp_all +decide [ Finset.inf'_le ]All goals completed! 🐙;
    grindAll goals completed! 🐙;
  ·negk:ℕS:Finset (Fin k → ℝ)T:Finset (Fin k → ℝ)hST:S ⊆ Tw:(Fin k → ℝ) → ℝt:ℝht0:0 < tht1:t ≤ 1hw:∀ v ∈ T, 0 ≤ w vhsum:∑ v ∈ T, w v = 1hSne:S.Nonemptyhsupp:∀ v ∈ T, v ∉ S → w v = 0h_cumWeight_eq:∀ v ∈ S, cumWeight S w v = cumWeight T w vv₀:Fin k → ℝ := quantileV T w thv₀:v₀ = quantileV T w thv₀_T:quantileV T w t ∈ Thv₀_S:quantileV T w t ∈ Shv₀_cum:t ≤ cumWeight T w (quantileV T w t)hv₀_pos:0 < w (quantileV T w t)h✝:∀ ⦃x : Fin k → ℝ⦄, x ∈ S → cumWeight T w x < t⊢ quantileV T w t = 0 linarith [ ‹∀ x ∈ S, cumWeight T w x < t› _ hv₀_S ]All goals completed! 🐙

end Quantile
end Submission

Lemma 5.2.3🔗

Lemma 5.2.3 (the quantile depends only on the threshold predicate). If two weight systems w, w' on the same \sigma satisfy \bigl(t \le \mathrm{cum}_\sigma(w,v)\bigr) \Leftrightarrow \bigl(t \le \mathrm{cum}_\sigma(w',v)\bigr) for every vertex v \in \sigma, then they have the same quantile vertex. (Immediate: the quantile is defined from this predicate.)

(In Lean this appears in the next chapter as quantileV_filter_congr, proved directly from the definition.)