PoissonMoments.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DilutedSpinGlass.bounded_memLp line 12

Source documentation

A bounded measurable score belongs to every finite Lp space.

theorem bounded_memLp {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω}
    [IsFiniteMeasure μ] {f : Ω → ℝ} {B : ℝ} (hf : Measurable f)
    (hB : ∀ x, |f x| ≤ B) (p : ℝ≥0∞) : MemLp f p μ := by
…

theorem OAI.DilutedSpinGlass.variance_two_copies line 19

Source documentation

The exact two-independent-copy identity for variance.

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

theorem OAI.DilutedSpinGlass.variance_le_oscillation line 50

Source documentation

Pairwise oscillation controls root variance without choosing a center.

theorem variance_le_oscillation {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω}
    [IsProbabilityMeasure μ] {f : Ω → ℝ} {C : ℝ} (hf : MemLp f 2 μ)
    (hC : ∀ x y, |f x-f y| ≤ C) : variance f μ ≤ C^2/2 := by
…

theorem OAI.DilutedSpinGlass.abs_integral_le_bound line 78
Source documentation
Uniform bounds survive averaging a physical root coordinate.
```
theorem abs_integral_le_bound {f : Ω → ℝ} {B : ℝ} (hB : ∀ x, |f x| ≤ B) :
    |∫ x, f x ∂μ| ≤ B := by
…
```

theorem OAI.DilutedSpinGlass.variance_prod_decomposition line 84

Source documentation

Total variance for a bounded measurable function of two independent root blocks.

theorem variance_prod_decomposition {f : Ω × Λ → ℝ} {B : ℝ}
    (hf : Measurable f) (hB : ∀ x, |f x| ≤ B) :
    variance f (μ.prod ν) =
      (∫ x, variance (fun y => f (x,y)) ν ∂μ) +
        variance (fun x => ∫ y, f (x,y) ∂ν) μ := by
…

theorem OAI.DilutedSpinGlass.integral_oscillation line 105

Source documentation

An independent block average preserves each bounded-difference constant.

theorem integral_oscillation {f : Ω × Λ → ℝ} {B C : ℝ}
    (hf : Measurable f) (hB : ∀ z, |f z| ≤ B)
    (hC : ∀ x x' y, |f (x,y)-f (x',y)| ≤ C) :
    ∀ x x', |(∫ y, f (x,y) ∂ν) - (∫ y, f (x',y) ∂ν)| ≤ C := by
…

abbrev OAI.DilutedSpinGlass.RootPath line 123
Source documentation
A finite independent block sequence, with no finiteness assumption on a block.
```
abbrev RootPath (Ω : Type u) : ℕ → Type u
  | 0 => PUnit
  | n+1 => Ω × RootPath Ω n
```
instance OAI.DilutedSpinGlass.rootPathMeasurable line 127
def OAI.DilutedSpinGlass.rootLaw line 134
instance OAI.DilutedSpinGlass.rootLawProbability line 139
def OAI.DilutedSpinGlass.replaceRoot line 150

theorem OAI.DilutedSpinGlass.root_variance_bound line 156

Source documentation

Bounded coordinate replacements give a variance bound additive in the number of independent root coordinates, not quadratic in that number.

theorem root_variance_bound {Ω : Type*} [MeasurableSpace Ω] (n : ℕ)
    (μ : Fin n → Measure Ω) [hμ : ∀ i, IsProbabilityMeasure (μ i)]
    {F : RootPath Ω n → ℝ} {B : ℝ} (hF : Measurable F) (hB : ∀ x, |F x| ≤ B)
    (C : Fin n → ℝ)
    (hC : ∀ (i : Fin n) x y, |F x-F (replaceRoot n x i y)| ≤ C i) :
    variance F (rootLaw n μ) ≤ ∑ i, (C i)^2/2 := by
…

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