MarkedPoisson.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.poissonWeight line 12
Source documentation
The archival Mathlib Poisson weights, not a replacement count model.
```
noncomputable def poissonWeight (r : ℝ≥0) (n : ℕ) : ℝ :=
…
```
theorem OAI.DilutedSpinGlass.poissonWeight_nonneg line 15
theorem OAI.DilutedSpinGlass.poissonWeight_succ_mul line 19

theorem OAI.DilutedSpinGlass.poisson_add_one line 28

Source documentation

Poisson add-one (the count part of pert:palm), including zero rate.

theorem poisson_add_one (r : ℝ≥0) (f : ℕ → ℝ)
    (hf : Integrable (fun n => f (n+1)) (poissonMeasure r)) :
    (∫ n : ℕ, (n : ℝ) * f n ∂poissonMeasure r) =
      (r : ℝ) * ∫ n : ℕ, f (n+1) ∂poissonMeasure r := by
…

theorem OAI.DilutedSpinGlass.poisson_integrable_count line 44
Source documentation
Integrability of the count is proved from the same add-one recurrence.
```
theorem poisson_integrable_count (r : ℝ≥0) :
    Integrable (fun n : ℕ => (n : ℝ)) (poissonMeasure r) := by
…
```
theorem OAI.DilutedSpinGlass.poisson_mean line 56
theorem OAI.DilutedSpinGlass.poisson_integrable_linear line 60
theorem OAI.DilutedSpinGlass.poisson_integrable_count_sq line 66
theorem OAI.DilutedSpinGlass.poisson_second_moment line 83
theorem OAI.DilutedSpinGlass.poisson_variance line 97

theorem OAI.DilutedSpinGlass.poisson_integrable_quadratic line 117

Source documentation

A quadratic envelope suffices; no exponential moment is used.

theorem poisson_integrable_quadratic (r : ℝ≥0) {f : ℕ → ℝ} {A B : ℝ}
    (h : ∀ n, |f n| ≤ A + B*(n : ℝ)^2) : Integrable f (poissonMeasure r) := by
…

theorem OAI.DilutedSpinGlass.poisson_memLp_lipschitz line 124

Source documentation

Lipschitz sequences have a square-integrable Poisson law.

theorem poisson_memLp_lipschitz (r : ℝ≥0) {f : ℕ → ℝ} {C : ℝ} (hC : 0 ≤ C)
    (hL : ∀ n m, |f n-f m| ≤ C*|(n : ℝ)-(m : ℝ)|) :
    MemLp f 2 (poissonMeasure r) := by
…

theorem OAI.DilutedSpinGlass.poisson_variance_lipschitz line 143

Source documentation

Poisson random-coordinate count variance: a count-Lipschitz logarithm has fluctuations of order sqrt(rate), not order rate.

theorem poisson_variance_lipschitz (r : ℝ≥0) {f : ℕ → ℝ} {C : ℝ} (hC : 0 ≤ C)
    (hL : ∀ n m, |f n-f m| ≤ C*|(n : ℝ)-(m : ℝ)|) :
    variance f (poissonMeasure r) ≤ C^2 * (r : ℝ) := by
…

theorem OAI.DilutedSpinGlass.nat_lipschitz_of_step line 176

Source documentation

Adding one root coordinate gives the full Lipschitz bound in the count.

theorem nat_lipschitz_of_step {f : ℕ → ℝ} {C : ℝ} (_hC : 0 ≤ C)
    (h : ∀ n, |f (n+1)-f n| ≤ C) : ∀ n m, |f n-f m| ≤ C*|(n : ℝ)-(m : ℝ)| := by
…

theorem OAI.DilutedSpinGlass.integral_sq_sub_center line 198

Source documentation

Centering at an arbitrary constant separates conditional variance and squared conditional-mean displacement.

theorem integral_sq_sub_center {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω}
    [IsProbabilityMeasure μ] {f : Ω → ℝ} (hf : MemLp f 2 μ) (a : ℝ) :
    (∫ x, (f x-a)^2 ∂μ) = variance f μ + ((∫ x, f x ∂μ)-a)^2 := by
…

def OAI.DilutedSpinGlass.rootAverage line 212

theorem OAI.DilutedSpinGlass.rootAverage_step line 216

Source documentation

Actual random-count root means inherit the addition/deletion constant.

theorem rootAverage_step {F : (n : ℕ) → RootPath Ω n → ℝ} {B : ℕ → ℝ} {D : ℝ}
    (hF : ∀ n, Measurable (F n)) (hB : ∀ n x, |F n x| ≤ B n)
    (hadd : ∀ n x y, |F (n+1) (x,y) - F n y| ≤ D) (n : ℕ) :
    |rootAverage μ F (n+1)-rootAverage μ F n| ≤ D := by
…

Mentions: OAI.DilutedSpinGlass.RootPath, OAI.DilutedSpinGlass.rootAverage

theorem OAI.DilutedSpinGlass.poisson_random_root_variance line 237