On this page

GaussianApplicationsapplicationsRandomSATPivotal

Random k-SAT: the variance of the lifetime

GaussianApplications.RandomSAT.Pivotalapplications/RandomSAT/Pivotal.v420 lines34 lemmas and theorems, 10 definitionssource

Imports 3 library modules and 7 external

External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.reals.reals, mathcomp.algebra.arithmetic_tactic, mathcomp.algebra.ring_tactic

Imported by 3

Part of target T7 of phase 12 (see Model.v). A Rocq formalization of the variance step of the credited argument of the proposition 'Polynomial concentration' of 'A limiting satisfiability threshold for every fixed clause size' (family 235 of the OpenAI math collection, revision 1581d4cbd, source/sections/concentration.tex), in the recursive form of the Lean development of the collection, which replaces the lemmas 'Deletion variance bound' and 'Pivotal pairs' of the manuscript and which this file follows (lean/OAI/Probability/RandomSAT):

Lean: clauseAverage (ClauseProcess.lean, line 148)

Lean: survival (ClauseProcess.lean, line 152)

Lean: survival_le_geometric (Variance.lean, line 135)

Lean: insertionSecond_succ (Variance.lean, line 204)

Lean: pivotal_local_bound (Variance.lean, line 243)

Lean: insertionSecond_le_occupation (Variance.lean, line 285)

Lean: lifetimeVariance_succ_le (Variance.lean, line 330)

Lean: lifetimeVariance_le_occupation (Variance.lean, line 361)

S is a set of assignments on n variables, and the clauses of size k are uniform and independent; the means are those of finite_mean.v.

clause_avg k f S is the mean of f (add_clause S c) over one clause c, tuple_avg k m f S the mean of f (restrict S t) over m clauses t, survival k m S the probability that S survives m clauses, and kill k S the probability that one clause empties S. survival_le_geom: survival k d S <= (1 - kill k S)^d, since each of the d clauses must spare S.
life_mean m S and life_var m S are the mean and the variance of the lifetime life S t over m clauses t.
life_var_succ_le: by the law of total variance for the first clause (unif_var_tuple_cons), the variance over m.+1 clauses is at most the mean over the first clause of the variance over the other m, plus the second moment second m S of the change of the lifetime when a clause is inserted in front (delay).
With trunc M S = min(M kill k S, 1) and occ f m S the sum over j < m of the mean of f after j clauses, secondS and pivotal_local give second m S <= 2 occ (trunc M) m.+1 S for m < M (second_le_occ).
life_var_le_occ: if clause n k is not empty (k <= n), then life_var m S <= 2 m occ (trunc M) m S for m <= M.

The manuscript omits the clause i, bounds Var V by the sum over i of E (V^(-i) - V)^2 (the omission form of the Efron-Stein inequality, efron_stein_omission in library/probability/efron_stein_omission.v, which the proof of T7 does not use), and counts the pairs of pivotal times. The recursion here inserts a clause in front instead, as the Lean development does, and gives a bound of the same form: 2 M times the sum over the M prefixes of the mean of min(M q, 1), with q the killing probability.

Main results

Results	Statement
life_var_le_occ	For `k <= n`, a set `S` of assignments on `n` variables and `m <= M`, the variance of the lifetime `life S t` of `m` independent uniform clauses `t` of size `k` is at most `2 m` times the sum over `j < m` of the mean of `min(M q_j, 1)`, where `q_j` is the probability that one more clause empties the solution set of the first `j` clauses.

Declarations44 exported, 1 local

sectionclause_means

Context {R : realType} (n k : nat).
Local Notation asg := {ffun 'I_n -> bool}.
Local Notation C := (clause n k).

definition clause_avg source, line 71

Type

forall {R : realType} {n : nat},
nat -> ({set {ffun 'I_n -> bool}} -> R) -> {set {ffun 'I_n -> bool}} -> R

Definition

Definition clause_avg (f : {set asg} -> R) (S : {set asg}) : R :=
  unif_mean (fun c : C => f (add_clause S c)).

The mean over one uniform clause, and over m independent ones.

Used by 19 declarations in 2 files

this file: tuple_avgS, ler_clause_avg, clause_avg_cst, killE, life_meanS, life_mean_sum, secondS, occS, second_le_occ, life_var_succ_le, life_var_le_occ
GaussianApplications.RandomSAT.Forcing: tuple_avg_add, clause_avg_tuple_avg, del_meanS, era_meanS, del_mean_binom, clause_avg_short_survival, clause_avg_subr, era_mean_replacement

definition tuple_avg source, line 74

Type

forall {R : realType} {n : nat},
nat -> nat -> ({set {ffun 'I_n -> bool}} -> R) -> {set {ffun 'I_n -> bool}} -> R

Definition

Definition tuple_avg m (f : {set asg} -> R) (S : {set asg}) : R :=
  unif_mean (fun t : m.-tuple C => f (restrict S t)).

Used by 11 declarations in 3 files

this file: survival, tuple_avg0, tuple_avgS, ler_tuple_avg, survival0_set, occ
GaussianApplications.RandomSAT.Forcing: tuple_avg_add, clause_avg_tuple_avg, ler_tuple_avg_cst, clause_avg_short_survival
GaussianApplications.RandomSAT.Variance: sat_variance_bound_explicit

definition survival source, line 77

Type

forall {R : realType} {n : nat}, nat -> nat -> {set {ffun 'I_n -> bool}} -> R

Definition

Definition survival m (S : {set asg}) : R := tuple_avg m alive S.

Used by 16 declarations in 3 files

this file: survival_ge0, survival_mono, survival0_set, survival_le1, killE, survival_le_geom, life_mean_sum
GaussianApplications.RandomSAT.Replacement: kill_replacement
GaussianApplications.RandomSAT.Forcing: survival_antitone, del_mean_binom, short_survival, clause_avg_short_survival, era_mean_replacement, survival_le, P, head_forced_mean_le

lemma tuple_avg0 source, line 79

forall {R : realType} [n : nat] (k : nat) (f : {set {ffun 'I_n -> bool}} -> R)
  (S : {set {ffun 'I_n -> bool}}),
tuple_avg k 0 f S = f S

Statement as written in the source

Lemma tuple_avg0 f S : tuple_avg 0 f S = f S.

Used by 7 declarations in 2 files

this file: killE, life_mean_sum, occS
GaussianApplications.RandomSAT.Forcing: tuple_avg_add, del_mean_binom, clause_avg_short_survival, era_mean_replacement

lemma tuple_avgS source, line 82

forall {R : realType} [n : nat] (k m : nat) (f : {set {ffun 'I_n -> bool}} -> R)
  (S0 : {set {ffun 'I_n -> bool}}),
tuple_avg k m.+1 f S0 = clause_avg k (tuple_avg k m f) S0

Statement as written in the source

Lemma tuple_avgS m f S : tuple_avg m.+1 f S = clause_avg (tuple_avg m f) S.

Used by 8 declarations in 2 files

this file: killE, life_mean_sum, occS
GaussianApplications.RandomSAT.Forcing: tuple_avg_add, survival_antitone, del_mean_binom, clause_avg_short_survival, era_mean_replacement

lemma ler_clause_avg source, line 85

forall {R : realType} [n : nat] (k : nat) [f g : {set {ffun 'I_n -> bool}} -> R]
  (S : {set {ffun 'I_n -> bool}}),
(forall T : {set {ffun 'I_n -> bool}}, f T <= g T) -> clause_avg k f S <= clause_avg k g S

Statement as written in the source

Lemma ler_clause_avg (f g : {set asg} -> R) S :
  (forall T, f T <= g T) -> clause_avg f S <= clause_avg g S.

Used by 1 declaration in 1 file

GaussianApplications.RandomSAT.Forcing: era_mean_replacement

lemma ler_tuple_avg source, line 89

forall {R : realType} [n : nat] (k m : nat) [f g : {set {ffun 'I_n -> bool}} -> R]
  (S : {set {ffun 'I_n -> bool}}),
(forall T : {set {ffun 'I_n -> bool}}, f T <= g T) ->
tuple_avg k m f S <= tuple_avg k m g S

Statement as written in the source

Lemma ler_tuple_avg m (f g : {set asg} -> R) S :
  (forall T, f T <= g T) -> tuple_avg m f S <= tuple_avg m g S.

Used by 1 declaration in 1 file

GaussianApplications.RandomSAT.Forcing: clause_avg_short_survival

lemma survival_ge0 source, line 93

forall {R : realType} [n : nat] (k m : nat) (S : {set {ffun 'I_n -> bool}}),
0 <= survival k m S

Statement as written in the source

Lemma survival_ge0 m S : 0 <= survival m S.

Used by 1 declaration in 1 file

GaussianApplications.RandomSAT.Forcing: integrated_head_forcing

lemma survival_mono source, line 96

forall {R : realType} [n : nat] (k m : nat) [S T : {set {ffun 'I_n -> bool}}],
S \subset T -> survival k m S <= survival k m T

Statement as written in the source

Lemma survival_mono m (S T : {set asg}) :
  S \subset T -> survival m S <= survival m T.

Used by 1 declaration in 1 file

GaussianApplications.RandomSAT.Forcing: survival_antitone

lemma survival0_set source, line 103

forall {R : realType} (n k m : nat), survival k m (set0 : {set {ffun 'I_n -> bool}}) = 0

Statement as written in the source

Lemma survival0_set m : survival m (set0 : {set asg}) = 0.

Used by 3 declarations in 3 files

this file: survival_le_geom
GaussianApplications.RandomSAT.Replacement: kill_replacement
GaussianApplications.RandomSAT.Forcing: short_survival

Hypothesis C0 : (0 < #|{: C}|)%N.

lemma clause_avg_cst source, line 113

forall {R : realType} [n k : nat],
(0 < #|{: clause n k}|)%N ->
forall (c : R) (S : {set {ffun 'I_n -> bool}}), clause_avg k (fun=> c) S = c

Statement as written in the source

Lemma clause_avg_cst (c : R) S : clause_avg (fun=> c) S = c.

lemma survival_le1 source, line 116

forall {R : realType} [n k : nat],
(0 < #|{: clause n k}|)%N ->
forall (m : nat) (S : {set {ffun 'I_n -> bool}}), survival k m S <= 1

Statement as written in the source

Lemma survival_le1 m S : survival m S <= 1.

Used by 1 declaration in 1 file

GaussianApplications.RandomSAT.Forcing: integrated_head_forcing

definition kill source, line 123

Type

forall {R : realType} {n : nat}, nat -> {set {ffun 'I_n -> bool}} -> R

Definition

Definition kill (S : {set asg}) : R :=
  unif_mean (fun c : C => alive S - alive (add_clause S c)).

The probability that one uniform clause kills S.

Used by 11 declarations in 2 files

this file: kill_ge0, kill_le1, kill0, killE, survival_le_geom, second0, secondS, trunc, pivotal_local
GaussianApplications.RandomSAT.Replacement: killE_forced, kill_replacement

lemma kill_ge0 source, line 126

forall {R : realType} [n : nat] (k : nat) (S : {set {ffun 'I_n -> bool}}), 0 <= kill k S

Statement as written in the source

Lemma kill_ge0 S : 0 <= kill S.

Used by 2 declarations in 1 file

this file: trunc_ge0, pivotal_local

lemma kill_le1 source, line 131

forall {R : realType} [n k : nat],
(0 < #|{: clause n k}|)%N -> forall S : {set {ffun 'I_n -> bool}}, kill k S <= 1

Statement as written in the source

Lemma kill_le1 S : kill S <= 1.

Used by 1 declaration in 1 file

this file: pivotal_local

lemma kill0 source, line 138

forall {R : realType} [n k : nat], (0 < #|{: clause n k}|)%N -> kill k set0 = 0

Statement as written in the source

Lemma kill0 : kill set0 = 0.

Used by 3 declarations in 3 files

this file: survival_le_geom
GaussianApplications.RandomSAT.Replacement: kill_replacement
GaussianApplications.RandomSAT.Variance: trunc_le_forced

lemma killE source, line 144

forall {R : realType} [n k : nat],
(0 < #|{: clause n k}|)%N ->
forall S0 : {set {ffun 'I_n -> bool}}, kill k S0 = alive S0 - survival k 1 S0

Statement as written in the source

Lemma killE S : kill S = alive S - survival 1 S.

Used by 1 declaration in 1 file

GaussianApplications.RandomSAT.Forcing: short_survival

lemma alive_restrict_le source, line 152

forall {R : realType} [n k : nat] (S : {set {ffun 'I_n -> bool}}) (s : seq (clause n k)),
(alive (restrict S s) : R) <= (\prod_(c <- s) alive (add_clause S c) : R)

A solution of all the clauses of s satisfies each of them.

Statement as written in the source

Lemma alive_restrict_le (S : {set asg}) (s : seq C) :
  alive (restrict S s) <= \prod_(c <- s) alive (add_clause S c) :> R.

Used by 1 declaration in 1 file

this file: survival_le_geom

lemma survival_le_geom source, line 166

forall {R : realType} [n k : nat],
(0 < #|{: clause n k}|)%N ->
forall (d : nat) (S : {set {ffun 'I_n -> bool}}), survival k d S <= (1 - kill k S) ^+ d

Surviving d clauses requires that none of them kills S on its own.

Statement as written in the source

Lemma survival_le_geom d S : survival d S <= (1 - kill S) ^+ d.

Used by 2 declarations in 2 files

this file: pivotal_local
GaussianApplications.RandomSAT.Replacement: kill_replacement

Arguments clause_avg {R n} k f S.
Arguments tuple_avg {R n} k m f S.
Arguments survival {R n} k m S.
Arguments kill {R n} k S.

sectionlifetime

Context {R : realType} (n k : nat).
Local Notation asg := {ffun 'I_n -> bool}.
Local Notation C := (clause n k).
Hypothesis C0 : (0 < #|{: C}|)%N.

let T0 section-local source, line 190

Let T0 m : (0 < #|{: m.-tuple C}|)%N.

definition life_mean source, line 193

Type

forall {R : realType} [n : nat], nat -> nat -> {set {ffun 'I_n -> bool}} -> R

Definition

Definition life_mean m (S : {set asg}) : R :=
  unif_mean (fun t : m.-tuple C => life S t).

Used by 7 declarations in 1 file

this file: life_meanS, life_mean_ge0, life_mean_sum, secondS, pivotal_local, second_le_occ, life_var_succ_le

definition life_var source, line 196

Type

forall {R : realType} [n : nat], nat -> nat -> {set {ffun 'I_n -> bool}} -> R

Definition

Definition life_var m (S : {set asg}) : R :=
  unif_var (fun t : m.-tuple C => life S t).

Used by 4 declarations in 2 files

this file: life_var_succ_le, life_var_le_occ
GaussianApplications.RandomSAT.Variance: sat_capped_varE, sat_variance_bound_explicit

lemma life_meanS source, line 199

forall {R : realType} [n k : nat],
(0 < #|{: clause n k}|)%N ->
forall (m : nat) (S0 : {set {ffun 'I_n -> bool}}),
life_mean k m.+1 S0 =
clause_avg k (fun T : {set {ffun 'I_n -> bool}} => alive T + life_mean k m T) S0

Statement as written in the source

Lemma life_meanS m S :
  life_mean m.+1 S = clause_avg k (fun T => alive T + life_mean m T) S.

Used by 2 declarations in 1 file

this file: life_mean_sum, secondS

lemma life_mean_ge0 source, line 206

forall {R : realType} [n : nat] (k m : nat) (S : {set {ffun 'I_n -> bool}}),
0 <= life_mean k m S

Statement as written in the source

Lemma life_mean_ge0 m S : 0 <= life_mean m S.

Used by 1 declaration in 1 file

this file: pivotal_local

lemma life_mean_sum source, line 209

forall {R : realType} [n k : nat],
(0 < #|{: clause n k}|)%N ->
forall (m : nat) (S0 : {set {ffun 'I_n -> bool}}),
life_mean k m S0 = \sum_(j < m) survival k j.+1 S0

Statement as written in the source

Lemma life_mean_sum m S :
  life_mean m S = \sum_(j < m) survival k j.+1 S.

Used by 1 declaration in 1 file

this file: pivotal_local

definition delay source, line 222

Type

forall {R : realType} [n k m : nat],
{set {ffun 'I_n -> bool}} -> clause n k -> m.-tuple (clause n k) -> R

Definition

Definition delay m (S : {set asg}) (c : C) (t : m.-tuple C) : R :=
  (alive S + life S t) - (alive (add_clause S c) + life (add_clause S c) t).

Inserting the clause c at the front: the change of the lifetime.

Used by 7 declarations in 1 file

this file: second, delay_cons, delay_cross, delay_cons_sqr, second0, secondS, life_var_succ_le

definition second source, line 225

Type

forall {R : realType} [n : nat], nat -> nat -> {set {ffun 'I_n -> bool}} -> R

Definition

Definition second m (S : {set asg}) : R :=
  unif_mean (fun c : C => unif_mean (fun t : m.-tuple C => delay S c t ^+ 2)).

Used by 5 declarations in 1 file

this file: second0, secondS, second_ge0, second_le_occ, life_var_succ_le

lemma delay_cons source, line 228

forall {R : realType} [n k m : nat] (S0 : {set {ffun 'I_n -> bool}}) 
  (c d : clause n k) (t : m.-tuple (clause n k)),
delay S0 c [tuple of d :: t] =
alive S0 - alive (add_clause S0 c) + delay (add_clause S0 d) c t

Statement as written in the source

Lemma delay_cons m S (c d : C) (t : m.-tuple C) :
  delay S c [tuple of d :: t] =
  alive S - alive (add_clause S c) + delay (add_clause S d) c t.

Used by 1 declaration in 1 file

this file: delay_cons_sqr

lemma bool_diff_sqr source, line 233

forall {R : realType} [a b : bool], b ==> a -> (a%:R - b%:R : R) ^+ 2 = a%:R - b%:R

Statement as written in the source

Lemma bool_diff_sqr (a b : bool) :
  (b ==> a) -> (a%:R - b%:R : R) ^+ 2 = a%:R - b%:R.

Used by 1 declaration in 1 file

this file: pivot_sqr

lemma pivot_sqr source, line 237

forall {R : realType} [n k : nat] (S0 : {set {ffun 'I_n -> bool}}) (c : clause n k),
(alive S0 - alive (add_clause S0 c)) ^+ 2 = alive S0 - alive (add_clause S0 c)

Statement as written in the source

Lemma pivot_sqr S (c : C) :
  (alive S - alive (add_clause S c)) ^+ 2 =
    alive S - alive (add_clause S c) :> R.

Used by 2 declarations in 1 file

this file: delay_cons_sqr, second0

lemma delay_cross source, line 245

forall {R : realType} [n k m : nat] [S T : {set {ffun 'I_n -> bool}}] 
  (c : clause n k) (t : m.-tuple (clause n k)),
T \subset S ->
(alive S - alive (add_clause S c)) * delay T c t =
(alive S - alive (add_clause S c)) * (alive T + life T t)

Statement as written in the source

Lemma delay_cross m (S T : {set asg}) (c : C) (t : m.-tuple C) :
  T \subset S ->
  (alive S - alive (add_clause S c)) * delay T c t =
  (alive S - alive (add_clause S c)) * (alive T + life T t).

Used by 1 declaration in 1 file

this file: delay_cons_sqr

lemma delay_cons_sqr source, line 261

forall {R : realType} [n k m : nat] (S0 : {set {ffun 'I_n -> bool}}) 
  (c d : clause n k) (t : m.-tuple (clause n k)),
delay S0 c [tuple of d :: t] ^+ 2 =
delay (add_clause S0 d) c t ^+ 2 + (alive S0 - alive (add_clause S0 c)) +
2 * (alive S0 - alive (add_clause S0 c)) *
(alive (add_clause S0 d) + life (add_clause S0 d) t)

Statement as written in the source

Lemma delay_cons_sqr m S (c d : C) (t : m.-tuple C) :
  delay S c [tuple of d :: t] ^+ 2 =
  delay (add_clause S d) c t ^+ 2 + (alive S - alive (add_clause S c)) +
  2 * (alive S - alive (add_clause S c)) *
    (alive (add_clause S d) + life (add_clause S d) t).

Used by 1 declaration in 1 file

this file: secondS

lemma second0 source, line 271

forall {R : realType} [n : nat] (k : nat) (S : {set {ffun 'I_n -> bool}}),
second k 0 S = kill k S

Statement as written in the source

Lemma second0 S : second 0 S = kill k S.

Used by 1 declaration in 1 file

this file: second_le_occ

lemma secondS source, line 277

forall {R : realType} [n k : nat],
(0 < #|{: clause n k}|)%N ->
forall (m : nat) (S0 : {set {ffun 'I_n -> bool}}),
second k m.+1 S0 = clause_avg k (second k m) S0 + kill k S0 * (1 + 2 * life_mean k m.+1 S0)

Statement as written in the source

Lemma secondS m S :
  second m.+1 S =
  clause_avg k (second m) S + kill k S * (1 + 2 * life_mean m.+1 S).

Used by 1 declaration in 1 file

this file: second_le_occ

lemma second_ge0 source, line 302

forall {R : realType} [n : nat] (k m : nat) (S : {set {ffun 'I_n -> bool}}),
0 <= second k m S

Statement as written in the source

Lemma second_ge0 m S : 0 <= second m S.

lemma geom_sum_le source, line 307

forall {R : realType} [q : R] (t : nat),
0 <= q -> q <= 1 -> q * \sum_(j < t) (1 - q) ^+ j <= Num.min (t%:R * q) 1

Statement as written in the source

Lemma geom_sum_le (q : R) t : 0 <= q -> q <= 1 ->
  q * \sum_(j < t) (1 - q) ^+ j <= Num.min (t%:R * q) 1.

Used by 1 declaration in 1 file

this file: pivotal_local

definition trunc source, line 323

Type

forall {R : realType} [n : nat], nat -> nat -> {set {ffun 'I_n -> bool}} -> R

Definition

Definition trunc M (S : {set asg}) : R := Num.min (M%:R * kill k S) 1.

The killing chance, truncated at 1 / M.

Used by 6 declarations in 2 files

this file: trunc_ge0, pivotal_local, second_le_occ, life_var_le_occ
GaussianApplications.RandomSAT.Variance: trunc_le_forced, sat_variance_bound_explicit

lemma trunc_ge0 source, line 325

forall {R : realType} [n : nat] (k M : nat) (S : {set {ffun 'I_n -> bool}}),
0 <= trunc k M S

Statement as written in the source

Lemma trunc_ge0 M S : 0 <= trunc M S.

Used by 1 declaration in 1 file

this file: life_var_le_occ

lemma pivotal_local source, line 328

forall {R : realType} [n k : nat],
(0 < #|{: clause n k}|)%N ->
forall [m M : nat] (S0 : {set {ffun 'I_n -> bool}}),
(m < M)%N -> kill k S0 * (1 + 2 * life_mean k m S0) <= 2 * trunc k M S0

Statement as written in the source

Lemma pivotal_local m M S : (m.+1 <= M)%N ->
  kill k S * (1 + 2 * life_mean m S) <= 2 * trunc M S.

Used by 1 declaration in 1 file

this file: second_le_occ

definition occ source, line 345

Type

forall {R : realType} [n : nat],
nat -> ({set {ffun 'I_n -> bool}} -> R) -> nat -> {set {ffun 'I_n -> bool}} -> R

Definition

Definition occ (f : {set asg} -> R) m (S : {set asg}) : R :=
  \sum_(j < m) tuple_avg k j f S.

The occupation sum of f along the first m clauses.

Used by 5 declarations in 2 files

this file: occS, occ_ge0, second_le_occ, life_var_le_occ
GaussianApplications.RandomSAT.Variance: sat_variance_bound_explicit

lemma occS source, line 348

forall {R : realType} [n : nat] (k : nat) (f : {set {ffun 'I_n -> bool}} -> R) 
  (m : nat) (S0 : {set {ffun 'I_n -> bool}}),
occ k f m.+1 S0 = f S0 + clause_avg k (occ k f m) S0

Statement as written in the source

Lemma occS f m S : occ f m.+1 S = f S + clause_avg k (occ f m) S.

Used by 2 declarations in 1 file

this file: second_le_occ, life_var_le_occ

lemma occ_ge0 source, line 355

forall {R : realType} [n : nat] (k : nat)
  [f : {set {ffun 'I_n -> bool}} ->
       join_Num_POrderNmodule_between_Algebra_BaseAddUMagma_and_Order_Preorder R]
  (m : nat) (S : {set {ffun 'I_n -> bool}}),
(forall T : {set {ffun 'I_n -> bool}}, 0 <= f T) -> 0 <= occ k f m S

Statement as written in the source

Lemma occ_ge0 f m S : (forall T, 0 <= f T) -> 0 <= occ f m S.

lemma second_le_occ source, line 360

forall {R : realType} [n k : nat],
(0 < #|{: clause n k}|)%N ->
forall [m M : nat] (S0 : {set {ffun 'I_n -> bool}}),
(m < M)%N -> second k m S0 <= 2 * occ k (trunc k M) m.+1 S0

Statement as written in the source

Lemma second_le_occ m M S : (m.+1 <= M)%N ->
  second m S <= 2 * occ (trunc M) m.+1 S.

Used by 1 declaration in 1 file

this file: life_var_le_occ

lemma life_var_succ_le source, line 379

forall {R : realType} [n k : nat],
(0 < #|{: clause n k}|)%N ->
forall (m : nat) (S0 : {set {ffun 'I_n -> bool}}),
life_var k m.+1 S0 <= clause_avg k (life_var k m) S0 + second k m S0

Statement as written in the source

Lemma life_var_succ_le m S :
  life_var m.+1 S <= clause_avg k (life_var m) S + second m S.

Used by 1 declaration in 1 file

this file: life_var_le_occ

lemma life_var_le_occ main result source, line 398

forall {R : realType} [n k : nat],
(0 < #|{: clause n k}|)%N ->
forall [m M : nat] (S0 : {set {ffun 'I_n -> bool}}),
(m <= M)%N -> life_var k m S0 <= 2 * m%:R * occ k (trunc k M) m S0

The variance of the lifetime is at most 2 m times the occupation sum of the truncated killing chance.

Main result, as the README states it

For k <= n, a set S of assignments on n variables and m <= M, the variance of the lifetime life S t of m independent uniform clauses t of size k is at most 2 m times the sum over j < m of the mean of min(M q_j, 1), where q_j is the probability that one more clause empties the solution set of the first j clauses.

Statement as written in the source

Lemma life_var_le_occ m M S : (m <= M)%N ->
  life_var m S <= 2 * m%:R * occ (trunc M) m S.

Used by 1 declaration in 1 file

GaussianApplications.RandomSAT.Variance: sat_variance_bound_explicit

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.