diff --git a/analysis/markov/src/Linleios/Probability.lean b/analysis/markov/src/Linleios/Probability.lean index df0dc5b37..ba5c24320 100644 --- a/analysis/markov/src/Linleios/Probability.lean +++ b/analysis/markov/src/Linleios/Probability.lean @@ -19,17 +19,19 @@ deriving Repr Fait Accompli sortition. -/ def faSortition (nPools n : Nat) : List Sortition := - let S (i : Nat) := ((nPools - i + 1).toFloat / nPools.toFloat)^10 - ((nPools - i).toFloat / nPools.toFloat)^10 - let ρ (i : Nat) := 1 - ((nPools - i).toFloat / nPools.toFloat)^10 - let test (n i : Nat) : Bool := (1 - S i / ρ i)^2 < (n - i).toFloat / (n - i + 1).toFloat + let ρ (i : Nat) := ((nPools - i + 1).toFloat / nPools.toFloat)^10 + let S (i : Nat) := ρ i - ((nPools - i).toFloat / nPools.toFloat)^10 + let test (i : Nat) : Bool := (1 - S i / ρ i)^2 < (n - i).toFloat / (n - i + 1).toFloat let i := (List.range nPools).map $ Add.add 1 - let ⟨ persistent , nonpersistent ⟩ := i.partition $ test n - let ρStar := ρ $ persistent.length + 1 + let ⟨ persistent , nonpersistent ⟩ := i.partition test + let n₁ := persistent.length + let n₂ := n - n₁ + let ρStar := ρ $ n₁ + 1 let persistent' := persistent.map $ fun i ↦ {stake := S i, probability := 1} let nonpersistent' := nonpersistent.map $ fun i ↦ let Si := S i - {stake := Si, probability := Si / ρStar} + {stake := Si, probability := 1 - Float.exp (- n₂.toFloat * Si / ρStar)} persistent' ++ nonpersistent' /-- diff --git a/analysis/markov/src/LinleiosTest.lean b/analysis/markov/src/LinleiosTest.lean index a651492d7..669e70226 100644 --- a/analysis/markov/src/LinleiosTest.lean +++ b/analysis/markov/src/LinleiosTest.lean @@ -131,8 +131,8 @@ private def outcomeNearUnity (os : Outcomes) : Bool := ) $ group "Quorum" ( check "All voters vote and all votes are received" ( - ∀ τ : RangedFloat 0.51 0.76, - ∀ committeeSize : RangedNat 700 1000, + ∀ τ : RangedFloat 0.50 0.90, + ∀ committeeSize : RangedNat 600 1000, nearUnity $ pQuorum 1 committeeSize.value.toFloat τ.value ) )