OAI/Probability/DilutedSpin/HeterogeneousTwoPoisson.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DilutedSpinGlass.poisson_integrable_root_squared line 15

   Source documentation

   Quadratic integrability for a genuine random-dimensional root block.

   theorem poisson_integrable_root_squared (r : ℝ≥0)
       {F : (n : ℕ) → RootPath I n → ℝ} {A D : ℝ}
       (hF : ∀ n x, |F n x| ≤ A+D*n) (c : ℝ) :
       Integrable (fun n : ℕ => ∫ x, (F n x-c)^2 ∂rootLaw n (fun _ => μ)) (poissonMeasure r) := by
   …

   Mentions: OAI.DilutedSpinGlass.RootPath, OAI.DilutedSpinGlass.rootLaw

2. theorem OAI.DilutedSpinGlass.two_poisson_roots_second_moment line 41

   Source documentation

   Two independent Poisson families, without converting both counts into one process or conditioning away either of the count fluctuations.

   theorem two_poisson_roots_second_moment (r s : ℝ≥0)
       {F : (k : ℕ) → RootPath I k → (n : ℕ) → RootPath J n → ℝ}
       {B C D : ℝ} (hC : 0 ≤ C) (hD : 0 ≤ D)
       (hF : ∀ k n, Measurable (fun z : RootPath I k × RootPath J n => F k z.1 n z.2))
       (hB : ∀ k x n y, |F k x n y| ≤ B+C*k+D*n)
       (hrep1 : ∀ k (i : Fin k) x z n y, |F k x n y-F k (replaceRoot k x i z) n y| ≤ 2*C)
       (hadd1 : ∀ k z x n y, |F (k+1) (z,x) n y-F k x n y| ≤ C)
       (hrep2 : ∀ k x n (i : Fin n) y z, |F k x n y-F k x n (replaceRoot n y i z)| ≤ 2*D)
       (hadd2 : ∀ k x n z y, |F k x (n+1) (z,y)-F k x n y| ≤ D) (c : ℝ) :
       (∫ k : ℕ, ∫ x, ∫ n : ℕ, ∫ y, (F k x n y-c)^2
         ∂rootLaw n (fun _ => ν) ∂poissonMeasure s ∂rootLaw k (fun _ => μ) ∂poissonMeasure r) ≤
         3*C^2*(r : ℝ)+3*D^2*(s : ℝ)+
   …

   Mentions: OAI.DilutedSpinGlass.RootPath, OAI.DilutedSpinGlass.replaceRoot, OAI.DilutedSpinGlass.rootLaw