GaussianAnalysisRocq library documentation
Main resultsGlossary
On this page
GaussianAnalysisprobabilitymeasurable_minimizer

Measurable minimizers

GaussianAnalysis.probability.measurable_minimizerlibrary/probability/measurable_minimizer.v395 lines21 lemmas and theorems, 3 definitionssource
Imports 7 library modules and 26 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.matrix, mathcomp.algebra.vector, mathcomp.algebra.sesquilinear, mathcomp.algebra.rat, mathcomp.algebra.interval, mathcomp.classical.boolp, mathcomp.classical.classical_sets, mathcomp.classical.functions, mathcomp.reals.reals, mathcomp.analysis.ereal, mathcomp.analysis.topology_theory.topology, mathcomp.analysis.normedtype_theory.normedtype, mathcomp.analysis.sequences, mathcomp.analysis.exp, mathcomp.analysis.measure_theory.measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.measurable_realfun, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.probability_theory.probability, mathcomp.algebra.ring_tactic, mathcomp.algebra.field_tactic, mathcomp.algebra.arithmetic_tactic

Required by 1 files of the paper proofs

Let g t, for t in a measurable space T, be functions on a set D of row vectors, minimized at th t with quadratic growth:

g t (th t) + c |theta - th t|^2 <= g t theta  for theta in D, c > 0.

If the values g t (q m) at the points of a fixed sequence q of D are measurable in t and come arbitrarily close to the minimum, then t |-> th t is measurable: th t is the limit of the first minimizers of g t among q 0, ..., q k. This gives a measurable choice of the minimizer of the least squares objective with a barrier of minimizers.v as a function of the features; it does not depend on the features that the objective does not use, as for the leave-one-out objectives of Koehler and Sohn (arXiv 2608.27372, proof of Proposition 2.1, lines 4525-4595).

first_min g q kthe first minimizer of g among q 0, ..., q k, with its value
ls_reduced Z P s lambda beta gamma B thetathe objective with a barrier at (theta, ls_bopt theta), the best b for theta
ls_min DV scB B0 D0 Z P s lambda beta gammathe minimizer over D of ls_reduced

Main results:

Main results

ResultsStatement
measurable_minimizerrel_open_dense_seqls_minls_min_growthmeasurable_ls_minls_min_tuple_set
Measurable selection of minimizers: if g t has a minimizer th t on D with quadratic growth g t (th t) + c |theta - th t|^2 <= g t theta for theta in D (c > 0), and the values g t (q m) at a fixed sequence q of points of D are measurable in t and come arbitrarily close to the minimum, then t |-> th t is measurable (the limit of the first minimizers among q 0, ..., q k). A nonempty relatively open convex set has a dense sequence of points. Hence the minimizer over D x R of the least squares objective with a self-concordant barrier of convex/minimizers.v is a measurable function of the features; the reduced objective grows by at least beta lambda |theta - ls_min Z|^2 away from it, and it does not depend on the features that the objective does not use, as for a leave-one-out objective.

Declarations24 exported

lemma, theoremdefinitioninstancelocal
sectionfirst_minimizer
Context {R : realType} {N : nat}.
fixpoint first_min source, line 62
Type
forall {R : realType} {N : nat}, ('rV_N -> R) -> (nat -> 'rV_N) -> nat -> 'rV_N * R
Definition
Fixpoint first_min (g : 'rV[R]_N -> R) (q : nat -> 'rV[R]_N) (k : nat) :
    'rV[R]_N * R :=
  if k is k'.+1 then
    if g (q k) < (first_min g q k').2 then (q k, g (q k))
    else first_min g q k'
  else (q 0%N, g (q 0%N)).

The first minimizer of g among q 0, ..., q k, with its value.

Used by 5 declarations in 1 file
lemma first_min_val source, line 69 
forall {R : realType} {N : nat} (g : 'rV_N -> R) (q : nat -> 'rV_N) (k : nat),
(first_min g q k).2 = g (first_min g q k).1
Statement as written in the source
Lemma first_min_val g q k : (first_min g q k).2 = g (first_min g q k).1.
Used by 1 declaration in 1 file
lemma first_min_in source, line 72 
forall {R : realType} {N : nat} [D : set 'rV_N] (g : 'rV_N -> R) 
  [q : nat -> 'rV_N] (k : nat),
(forall m : nat, D (q m)) -> D (first_min g q k).1
Statement as written in the source
Lemma first_min_in (D : set 'rV[R]_N) g q k :
  (forall m, D (q m)) -> D (first_min g q k).1.
Used by 1 declaration in 1 file
lemma first_min_le source, line 79 
forall {R : realType} {N : nat} (g : 'rV_N -> R) (q : nat -> 'rV_N) [k m : nat],
(m <= k)%N -> (first_min g q k).2 <= g (q m)
Statement as written in the source
Lemma first_min_le g q k m : (m <= k)%N -> (first_min g q k).2 <= g (q m).
Used by 1 declaration in 1 file
Context d (T : measurableType d).
lemma measurable_first_min source, line 91 
forall {R : realType} {N : nat} [d : measure_display] [T : measurableType d]
  [g : T -> 'rV_N -> R] [q : nat -> 'rV_N] (k : nat),
(forall m : nat, measurable_fun [set: T] (g^~ (q m))) ->
measurable_fun [set: T] (fun t : T => first_min (g t) q k)
Statement as written in the source
Lemma measurable_first_min (g : T -> 'rV[R]_N -> R) (q : nat -> 'rV[R]_N) k :
  (forall m, measurable_fun setT (fun t => g t (q m))) ->
  measurable_fun setT (fun t => first_min (g t) q k).
Used by 1 declaration in 1 file
lemma measurable_minimizer main result source, line 105 
forall {R : realType} {N : nat} [d : measure_display] [T : measurableType d]
  [D : set 'rV_N] [q : nat -> 'rV_N] [g : T -> 'rV_N -> R] [th : T -> 'rV_N] 
  [c : R],
0 < c ->
(forall m : nat, D (q m)) ->
(forall m : nat, measurable_fun [set: T] (g^~ (q m))) ->
(forall (t : T) (theta : 'rV_N),
 D theta -> g t (th t) + c * mxdot (theta - th t) (theta - th t) <= g t theta) ->
(forall (t : T) (e : R), 0 < e -> exists m : nat, g t (q m) < g t (th t) + e) ->
measurable_fun [set: T] th

The selection lemma.

Main result, as the README states it

Measurable selection of minimizers: if g t has a minimizer th t on D with quadratic growth g t (th t) + c |theta - th t|^2 <= g t theta for theta in D (c > 0), and the values g t (q m) at a fixed sequence q of points of D are measurable in t and come arbitrarily close to the minimum, then t |-> th t is measurable (the limit of the first minimizers among q 0, ..., q k). A nonempty relatively open convex set has a dense sequence of points. Hence the minimizer over D x R of the least squares objective with a self-concordant barrier of convex/minimizers.v is a measurable function of the features; the reduced objective grows by at least beta lambda |theta - ls_min Z|^2 away from it, and it does not depend on the features that the objective does not use, as for a leave-one-out objective.

Statement as written in the source
Lemma measurable_minimizer (D : set 'rV[R]_N) (q : nat -> 'rV[R]_N)
    (g : T -> 'rV[R]_N -> R) (th : T -> 'rV[R]_N) (c : R) :
  0 < c -> (forall m, D (q m)) ->
  (forall m, measurable_fun setT (fun t => g t (q m))) ->
  (forall t theta, D theta ->
     g t (th t) + c * mxdot (theta - th t) (theta - th t) <= g t theta) ->
  (forall t (e : R), 0 < e -> exists m, g t (q m) < g t (th t) + e) ->
  measurable_fun setT th.
Used by 1 declaration in 1 file
lemma measurable_mxdot_fun source, line 136 
forall {R : realType} {N : nat} [d : measure_display] [T : measurableType d]
  [f g : T -> 'rV_N],
measurable_fun [set: T] f ->
measurable_fun [set: T] g -> measurable_fun [set: T] (fun t : T => mxdot (f t) (g t))
Statement as written in the source
Lemma measurable_mxdot_fun (f g : T -> 'rV[R]_N) :
  measurable_fun setT f -> measurable_fun setT g ->
  measurable_fun setT (fun t => mxdot (f t) (g t)).
Used by 1 declaration in 1 file
sectiondense_sequence
Context {R : realType} {N : nat}.
lemma rel_open_dense_seq main result source, line 156 
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N],
rel_open_convex V D ->
D !=set0 ->
exists q : nat -> 'rV_N,
  (forall m : nat, D (q m)) /\
  (forall theta : 'rV_N,
   D theta -> forall e : R, 0 < e -> exists m : nat, `|q m - theta| < e)

A nonempty relatively open convex set has a dense sequence of points: the points theta_0 + q E of D, q rational, for an orthonormal basis E of its directions (the construction of measurable_inf_rel_open of barrier_lindeberg.v).

Main result

Stated in the README together with measurable_minimizer.

Statement as written in the source
Lemma rel_open_dense_seq (V : {vspace 'rV[R]_N}) (D : set 'rV[R]_N) :
  rel_open_convex V D -> D !=set0 ->
  exists q : nat -> 'rV[R]_N, (forall m, D (q m)) /\
    forall theta, D theta -> forall e : R, 0 < e ->
      exists m, `|q m - theta| < e.
Used by 1 declaration in 1 file
sectionls_min
Context {R : realType} {N : nat}.
Variables (V : {vspace 'rV[R]_N}) (D : set 'rV[R]_N) (B : 'rV[R]_N -> R).
Hypotheses (DV : rel_open_convex V D) (scB : sc_function V D B).
Hypotheses (B0 : forall z, D z -> 0 <= B z) (D0 : D !=set0).
Variables (n : nat) (P : pred 'I_n) (s lambda beta gamma : R).
Hypotheses (s0 : 0 <= s) (l0 : 0 < lambda) (b0 : 0 < beta) (g0 : 0 < gamma).
definition ls_reduced source, line 222
Type
forall {R : realType} {N : nat},
('rV_N -> R) ->
forall [n : nat], pred 'I_n -> R -> R -> R -> R -> n.-tuple 'rV_N -> 'rV_N -> R
Definition
Definition ls_reduced (Z : n.-tuple 'rV[R]_N) (theta : 'rV[R]_N) : R :=
  ls_ridge Z P s lambda beta theta (ls_bopt Z P s beta theta) +
  gamma * B theta.

The objective with a barrier at the best b for theta.

Used by 8 declarations in 1 file
lemma ls_reduced_le source, line 226 
forall {R : realType} {N : nat} (B : 'rV_N -> R) [n : nat] (P : pred 'I_n) 
  [s : R] (lambda : R) [beta : R] (gamma : R),
0 <= s ->
0 < beta ->
forall (Z : n.-tuple 'rV_N) (theta : 'rV_N) (b : R),
ls_reduced B P s lambda beta gamma Z theta <=
ls_barrier_objective Z P s lambda beta gamma B theta b
Statement as written in the source
Lemma ls_reduced_le (Z : n.-tuple 'rV[R]_N) theta b :
  ls_reduced Z theta <=
  ls_barrier_objective Z P s lambda beta gamma B theta b.
Used by 1 declaration in 1 file
lemma ls_min_exists source, line 235 
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] [B : 'rV_N -> R],
rel_open_convex V D ->
sc_function V D B ->
(forall z : 'rV_N, D z -> 0 <= B z) ->
D !=set0 ->
forall [n : nat] (P : pred 'I_n) [s lambda beta gamma : R],
0 <= s ->
0 < lambda ->
0 < beta ->
0 < gamma ->
forall Z : n.-tuple 'rV_N,
exists2 theta : 'rV_N,
  D theta &
  forall theta' : 'rV_N,
  D theta' ->
  ls_reduced B P s lambda beta gamma Z theta <= ls_reduced B P s lambda beta gamma Z theta'
Statement as written in the source
Lemma ls_min_exists (Z : n.-tuple 'rV[R]_N) :
  exists2 theta, D theta &
    forall theta', D theta' -> ls_reduced Z theta <= ls_reduced Z theta'.
Used by 3 declarations in 1 file
definition ls_min main result source, line 249
Type
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] [B : 'rV_N -> R],
rel_open_convex V D ->
sc_function V D B ->
(forall z : 'rV_N, D z -> 0 <= B z) ->
D !=set0 ->
forall [n : nat],
pred 'I_n ->
forall [s lambda beta gamma : R],
0 <= s -> 0 < lambda -> 0 < beta -> 0 < gamma -> n.-tuple 'rV_N -> 'rV_N
Definition
Definition ls_min (Z : n.-tuple 'rV[R]_N) : 'rV[R]_N :=
  s2val (cid2 (ls_min_exists Z)).
Main result

Stated in the README together with measurable_minimizer.

Used by 9 declarations in 1 file
lemma ls_min_in source, line 252 
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] 
  [B : 'rV_N -> R] (DV : rel_open_convex V D) (scB : sc_function V D B)
  (B0 : forall z : 'rV_N, D z -> 0 <= B z) (D0 : D !=set0) [n : nat] 
  (P : pred 'I_n) [s lambda beta gamma : R] (s0 : 0 <= s) (l0 : 0 < lambda) 
  (b0 : 0 < beta) (g0 : 0 < gamma) (Z : n.-tuple 'rV_N),
D (ls_min DV scB B0 D0 P s0 l0 b0 g0 Z)
Statement as written in the source
Lemma ls_min_in Z : D (ls_min Z).
Used by 4 declarations in 1 file
lemma ls_min_le source, line 255 
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] 
  [B : 'rV_N -> R] (DV : rel_open_convex V D) (scB : sc_function V D B)
  (B0 : forall z : 'rV_N, D z -> 0 <= B z) (D0 : D !=set0) [n : nat] 
  (P : pred 'I_n) [s lambda beta gamma : R] (s0 : 0 <= s) (l0 : 0 < lambda) 
  (b0 : 0 < beta) (g0 : 0 < gamma) (Z : n.-tuple 'rV_N) [theta : 'rV_N],
D theta ->
ls_reduced B P s lambda beta gamma Z (ls_min DV scB B0 D0 P s0 l0 b0 g0 Z) <=
ls_reduced B P s lambda beta gamma Z theta
Statement as written in the source
Lemma ls_min_le Z theta : D theta -> ls_reduced Z (ls_min Z) <= ls_reduced Z theta.
Used by 2 declarations in 1 file
lemma ls_minP source, line 259 
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] 
  [B : 'rV_N -> R] (DV : rel_open_convex V D) (scB : sc_function V D B)
  (B0 : forall z : 'rV_N, D z -> 0 <= B z) (D0 : D !=set0) [n : nat] 
  (P : pred 'I_n) [s lambda beta gamma : R] (s0 : 0 <= s) (l0 : 0 < lambda) 
  (b0 : 0 < beta) (g0 : 0 < gamma) (Z : n.-tuple 'rV_N) [theta : 'rV_N] 
  (b : R),
D theta ->
ls_barrier_objective Z P s lambda beta gamma B (ls_min DV scB B0 D0 P s0 l0 b0 g0 Z)
  (ls_bopt Z P s beta (ls_min DV scB B0 D0 P s0 l0 b0 g0 Z)) <=
ls_barrier_objective Z P s lambda beta gamma B theta b

(ls_min Z, ls_bopt (ls_min Z)) minimizes the objective with a barrier.

Statement as written in the source
Lemma ls_minP Z theta b : D theta ->
  ls_barrier_objective Z P s lambda beta gamma B (ls_min Z)
    (ls_bopt Z P s beta (ls_min Z)) <=
  ls_barrier_objective Z P s lambda beta gamma B theta b.
Used by 1 declaration in 1 file
lemma ls_min_growth main result source, line 268 
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] 
  [B : 'rV_N -> R] (DV : rel_open_convex V D) (scB : sc_function V D B)
  (B0 : forall z : 'rV_N, D z -> 0 <= B z) (D0 : D !=set0) [n : nat] 
  (P : pred 'I_n) [s lambda beta gamma : R] (s0 : 0 <= s) (l0 : 0 < lambda) 
  (b0 : 0 < beta) (g0 : 0 < gamma) (Z : n.-tuple 'rV_N) [theta : 'rV_N],
D theta ->
ls_reduced B P s lambda beta gamma Z (ls_min DV scB B0 D0 P s0 l0 b0 g0 Z) +
beta * lambda *
mxdot (theta - ls_min DV scB B0 D0 P s0 l0 b0 g0 Z)
  (theta - ls_min DV scB B0 D0 P s0 l0 b0 g0 Z) <=
ls_reduced B P s lambda beta gamma Z theta

Quadratic growth of the reduced objective away from ls_min Z.

Main result

Stated in the README together with measurable_minimizer.

Statement as written in the source
Lemma ls_min_growth Z theta : D theta ->
  ls_reduced Z (ls_min Z) +
    beta * lambda * mxdot (theta - ls_min Z) (theta - ls_min Z) <=
  ls_reduced Z theta.
Used by 2 declarations in 1 file
lemma ls_min_unique source, line 300 
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] 
  [B : 'rV_N -> R] (DV : rel_open_convex V D) (scB : sc_function V D B)
  (B0 : forall z : 'rV_N, D z -> 0 <= B z) (D0 : D !=set0) [n : nat] 
  [P : pred 'I_n] [s lambda beta gamma : R] (s0 : 0 <= s) (l0 : 0 < lambda) 
  (b0 : 0 < beta) (g0 : 0 < gamma) [Z : n.-tuple 'rV_N] [theta : 'rV_N],
D theta ->
(forall theta' : 'rV_N,
 D theta' ->
 ls_reduced B P s lambda beta gamma Z theta <= ls_reduced B P s lambda beta gamma Z theta') ->
theta = ls_min DV scB B0 D0 P s0 l0 b0 g0 Z
Statement as written in the source
Lemma ls_min_unique Z theta : D theta ->
  (forall theta', D theta' -> ls_reduced Z theta <= ls_reduced Z theta') ->
  theta = ls_min Z.
Used by 1 declaration in 1 file
lemma measurable_ls_reduced_at source, line 314 
forall {R : realType} {N : nat} (B : 'rV_N -> R) [n : nat] (P : pred 'I_n)
  (s lambda beta gamma : R) (theta : 'rV_N),
measurable_fun [set: n.-tuple _]
  ((ls_reduced B P s lambda beta gamma)^~ theta)

The minimizer is a measurable function of the features.

Statement as written in the source
Lemma measurable_ls_reduced_at theta :
  measurable_fun setT (fun Z : n.-tuple 'rV[R]_N => ls_reduced Z theta).
Used by 1 declaration in 1 file
lemma measurable_ls_min main result source, line 321 
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] 
  [B : 'rV_N -> R] (DV : rel_open_convex V D) (scB : sc_function V D B)
  (B0 : forall z : 'rV_N, D z -> 0 <= B z) (D0 : D !=set0) [n : nat] 
  (P : pred 'I_n) [s lambda beta gamma : R] (s0 : 0 <= s) (l0 : 0 < lambda) 
  (b0 : 0 < beta) (g0 : 0 < gamma),
measurable_fun [set: n.-tuple _]
  (ls_min DV scB B0 D0 P s0 l0 b0 g0)
Main result

Stated in the README together with measurable_minimizer.

Statement as written in the source
Lemma measurable_ls_min : measurable_fun setT ls_min.
Used by 1 declaration in 1 file
lemma measurable_mxdot_ls_min source, line 354 
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] 
  [B : 'rV_N -> R] (DV : rel_open_convex V D) (scB : sc_function V D B)
  (B0 : forall z : 'rV_N, D z -> 0 <= B z) (D0 : D !=set0) [n : nat] 
  (P : pred 'I_n) [s lambda beta gamma : R] (s0 : 0 <= s) (l0 : 0 < lambda) 
  (b0 : 0 < beta) (g0 : 0 < gamma) (i : 'I_n),
measurable_fun [set: n.-tuple _]
  (fun Z : n.-tuple 'rV_N => mxdot (tnth Z i) (ls_min DV scB B0 D0 P s0 l0 b0 g0 Z))

The best b at the minimizer, and the values of the linear forms of the features there, are measurable functions of the features.

Statement as written in the source
Lemma measurable_mxdot_ls_min (i : 'I_n) :
  measurable_fun setT (fun Z : n.-tuple 'rV[R]_N => mxdot (tnth Z i) (ls_min Z)).
Used by 1 declaration in 1 file
lemma measurable_ls_bopt_min source, line 361 
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] 
  [B : 'rV_N -> R] (DV : rel_open_convex V D) (scB : sc_function V D B)
  (B0 : forall z : 'rV_N, D z -> 0 <= B z) (D0 : D !=set0) [n : nat] 
  (P : pred 'I_n) [s lambda beta gamma : R] (s0 : 0 <= s) (l0 : 0 < lambda) 
  (b0 : 0 < beta) (g0 : 0 < gamma),
measurable_fun [set: n.-tuple _]
  (fun Z : n.-tuple 'rV_N => ls_bopt Z P s beta (ls_min DV scB B0 D0 P s0 l0 b0 g0 Z))
Statement as written in the source
Lemma measurable_ls_bopt_min :
  measurable_fun setT (fun Z : n.-tuple 'rV[R]_N => ls_bopt Z P s beta (ls_min Z)).
lemma ls_bopt_tuple_set source, line 370 
forall {R : realType} {N : nat} [n : nat] [P : pred 'I_n] (s beta : R) 
  (Z : n.-tuple 'rV_N) [i : 'I_n] (t theta : 'rV_N),
~~ P i -> ls_bopt (tuple_set Z i t) P s beta theta = ls_bopt Z P s beta theta

The minimizer does not depend on the features outside P.

Statement as written in the source
Lemma ls_bopt_tuple_set (Z : n.-tuple 'rV[R]_N) i t theta :
  ~~ P i -> ls_bopt (tuple_set Z i t) P s beta theta = ls_bopt Z P s beta theta.
Used by 1 declaration in 1 file
lemma ls_reduced_tuple_set source, line 377 
forall {R : realType} {N : nat} (B : 'rV_N -> R) [n : nat] [P : pred 'I_n]
  (s lambda beta gamma : R) (Z : n.-tuple 'rV_N) [i : 'I_n] (t theta : 'rV_N),
~~ P i ->
ls_reduced B P s lambda beta gamma (tuple_set Z i t) theta =
ls_reduced B P s lambda beta gamma Z theta
Statement as written in the source
Lemma ls_reduced_tuple_set (Z : n.-tuple 'rV[R]_N) i t theta :
  ~~ P i -> ls_reduced (tuple_set Z i t) theta = ls_reduced Z theta.
Used by 1 declaration in 1 file
lemma ls_min_tuple_set main result source, line 387 
forall {R : realType} {N : nat} [V : {vspace 'rV_N}] [D : set 'rV_N] 
  [B : 'rV_N -> R] (DV : rel_open_convex V D) (scB : sc_function V D B)
  (B0 : forall z : 'rV_N, D z -> 0 <= B z) (D0 : D !=set0) [n : nat] 
  [P : pred 'I_n] [s lambda beta gamma : R] (s0 : 0 <= s) (l0 : 0 < lambda) 
  (b0 : 0 < beta) (g0 : 0 < gamma) (Z : n.-tuple 'rV_N) [i : 'I_n] 
  (t : 'rV_N),
~~ P i ->
ls_min DV scB B0 D0 P s0 l0 b0 g0 (tuple_set Z i t) = ls_min DV scB B0 D0 P s0 l0 b0 g0 Z
Main result

Stated in the README together with measurable_minimizer.

Statement as written in the source
Lemma ls_min_tuple_set (Z : n.-tuple 'rV[R]_N) i t :
  ~~ P i -> ls_min (tuple_set Z i t) = ls_min Z.
Generated from commit 9046883 (tag phase12) of the ellipsoid fitting repository. Signatures are printed by Rocq 9.1.1; links in the source statements come from the compiled .glob files. The source links open the files on GitHub at this commit, in the now-public repository.