OAI/Probability/DilutedSpin/FinitePoissonSplit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.finiteUniform line 11
2. instance OAI.DilutedSpinGlass.finiteUniform_prob line 13
3. lemma OAI.DilutedSpinGlass.integral_finiteUniform line 16
4. lemma OAI.DilutedSpinGlass.centeredExp_integrable line 29
5. lemma OAI.DilutedSpinGlass.centered_finite_mark line 37
6. lemma OAI.DilutedSpinGlass.finite_poisson_split line 48

   Source documentation

   Exact splitting of a finite marked process, allowing marks outside two disjoint families to be replaced by zero. The rates retain their exact finite-size values.

   lemma finite_poisson_split {A B C : Type*} [Fintype A] [Fintype B] [Fintype C]
       [Nonempty A] [Nonempty B] [Nonempty C]
       [MeasurableSpace A] [MeasurableSpace B] [MeasurableSpace C]
       [MeasurableSingletonClass A] [MeasurableSingletonClass B] [MeasurableSingletonClass C]
       (eA : A → C) (eB : B → C) (good : C → Prop) [DecidablePred good]
       (hs : ∀ f : C → ℂ, (∑ c,if good c then f c else 0) = (∑ a,f (eA a))+(∑ b,f (eB b)))
       (V : X×C → E) (hV : Measurable V) (r : ℝ≥0) :
       compoundPoisson r (Measure.map (fun z : X×C => if good z.2 then V z else 0)
         (μ.prod (finiteUniform C))) =
         compoundPoisson (r*(Fintype.card A)/(Fintype.card C))
           (Measure.map (fun z : X×A => V (z.1,eA z.2)) (μ.prod (finiteUniform A))) ∗
         compoundPoisson (r*(Fintype.card B)/(Fintype.card C))
   …

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