OAI/Probability/DilutedSpin/PoissonCountThinning.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.finite_poisson_deletion line 16
2. def OAI.DilutedSpinGlass.rawReplicaMoment line 88
3. lemma OAI.DilutedSpinGlass.replicaInsertionMoment_eq line 93
4. lemma OAI.DilutedSpinGlass.factorCut_eventually line 107
5. lemma OAI.DilutedSpinGlass.rawReplicaMoment_limit line 112
6. lemma OAI.DilutedSpinGlass.rawReplica_combination_nonneg line 149

   Source documentation

   Removing the coordinate cutoff uses only the original uniform product bound. No additional moments of individual factors are assumed.

   lemma rawReplica_combination_nonneg {p n : ℕ} (M : Model p) (hM : Admissible M)
       (hn : 1≤n) (j : Fin p) (P B : FiniteLaw (Fin n → Spin)) :
       0 ≤ rawReplicaMoment M (fun _ : Fin p => P) -
         (p:ℝ)*rawReplicaMoment M (fun l : Fin p => if l=j then P else B) +
         ((p-1:ℕ):ℝ)*rawReplicaMoment M (fun _ : Fin p => B) := by
   …

   Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.Admissible, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.rawReplicaMoment

7. lemma OAI.DilutedSpinGlass.compoundPoisson_dirac_one line 171
8. lemma OAI.DilutedSpinGlass.compoundPoisson_uniform_indicator line 186

   Source documentation

   Poisson thinning for independent uniform categorical choices.

   lemma compoundPoisson_uniform_indicator (r : ℝ≥0) (p : ℕ) [NeZero p] :
       compoundPoisson r (Measure.map (fun a : Fin p => if a=0 then (1:ℝ) else 0)
         (finiteUniform (Fin p))) = compoundPoisson (r/p) (Measure.dirac (1:ℝ)) := by
   …

   Mentions: OAI.DilutedSpinGlass.compoundPoisson, OAI.DilutedSpinGlass.finiteUniform

9. def OAI.DilutedSpinGlass.successCount line 216
10. lemma OAI.DilutedSpinGlass.map_poisson_successCount line 219