OAI/Probability/DilutedSpin/PoissonReplacement.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.successCount_le line 13
2. lemma OAI.DilutedSpinGlass.successCount_cons line 19
3. lemma OAI.DilutedSpinGlass.uniform_indicator_expect line 23
4. lemma OAI.DilutedSpinGlass.finite_count_replacement line 39

   Source documentation

   Finite independent replacement of real-or-null interactions by cavity interactions. The error has its exact extensive coefficient.

   lemma finite_count_replacement (p : ℕ) [NeZero p] (f : ℕ → ℕ → ℝ) (c : ℝ)
       (h : ∀ n l,f (n+1) l+((p-1:ℕ):ℝ)*f n l ≤ (p:ℝ)*(f n (l+1)-c))
       (k n l : ℕ) :
       (FiniteLaw.pi (fun _ : Fin k => (FiniteLaw.uniform : FiniteLaw (Fin p)))).expect
         (fun a => f (n+successCount a) l) ≤ f n (l+k)-(k:ℝ)*c := by
   …

   Mentions: OAI.DilutedSpinGlass.FiniteLaw.pi, OAI.DilutedSpinGlass.FiniteLaw.uniform, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.successCount

5. lemma OAI.DilutedSpinGlass.integral_poisson_thinning line 66
6. lemma OAI.DilutedSpinGlass.poisson_count_replacement line 99

   Source documentation

   Uniformized Poisson interpolation endpoint. The sole local input is the conditional cavity replacement inequality, at ALL old real/cavity counts.

   lemma poisson_count_replacement (r : ℝ≥0) (p : ℕ) [NeZero p]
       (f : ℕ → ℕ → ℝ) (c : ℝ) {B D : ℝ} (hD : 0≤D)
       (hf : ∀ n l,|f n l|≤B+D*(n+l))
       (h : ∀ n l,f (n+1) l+((p-1:ℕ):ℝ)*f n l ≤ (p:ℝ)*(f n (l+1)-c)) :
       (∫ n,f n 0 ∂poissonMeasure (r/p))+(r:ℝ)*c ≤ ∫ l,f 0 l ∂poissonMeasure r := by
   …