CountableReservoir.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.CountableReservoir.average line 17
Source documentation
Conditional iid type/site labels, on the full fixed countable dictionary.
```
noncomputable def average (F : (n : ℕ) → (Fin n → I) → ℝ) (n : ℕ) : ℝ :=
…
```
def OAI.DilutedSpinGlass.CountableReservoir.poissonAverage line 22
Source documentation
Poisson total count and iid countable labels. Marks remain in their finite, label-dependent prior rows and are not part of this quenched root law.
```
noncomputable def poissonAverage (s : ℝ≥0) (F : (n : ℕ) → (Fin n → I) → ℝ) : ℝ :=
…
```
theorem OAI.DilutedSpinGlass.CountableReservoir.integrable_row line 25
theorem OAI.DilutedSpinGlass.CountableReservoir.abs_average_le line 31
theorem OAI.DilutedSpinGlass.CountableReservoir.integrable_average line 38

theorem OAI.DilutedSpinGlass.CountableReservoir.integral_sum_labels line 44

Source documentation

The expected sum over a fixed iid list is exactly count times type mean.

theorem integral_sum_labels (n : ℕ) {D : I → ℝ} (hD : Integrable D ν) :
    (∫ roots : Fin n → I, ∑ q, D (roots q) ∂Measure.pi (fun _ : Fin n => ν)) =
      (n : ℝ) * ∫ i, D i ∂ν := by
…

Mentions: OAI.DilutedSpinGlass.q

theorem OAI.DilutedSpinGlass.CountableReservoir.poissonAverage_sum_stability line 53

Source documentation

A common-law comparison is averaged without replacing the full root law by the low types. The expected number of deleted factors is retained exactly.

theorem poissonAverage_sum_stability (s : ℝ≥0)
    {F G : (n : ℕ) → (Fin n → I) → ℝ} {A B : ℝ} {D : I → ℝ}
    (hF : ∀ n x, |F n x| ≤ A+B*n) (hG : ∀ n x, |G n x| ≤ A+B*n)
    (hD : Integrable D ν)
    (hdiff : ∀ n roots, |F n roots-G n roots| ≤ ∑ q, D (roots q)) :
    |poissonAverage ν s F-poissonAverage ν s G| ≤ (s : ℝ)*(∫ i, D i ∂ν) := by
…

Mentions: OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.CountableReservoir.poissonAverage

def OAI.DilutedSpinGlass.HeterogeneousMarks.pressure line 91

Source documentation

The literal marked-Poisson pressure, with every type in the same law.

noncomputable def pressure (s : ℝ≥0) (T : KernelTower Ω L)
    (Q : (i : I) → Fin L → FiniteLaw (A i)) (m : Fin L → ℝ)
    (base : FinitePath Ω L → ℝ)
    (factor : (i : I) → FinitePath Ω L → FinitePath (A i) L → ℝ) : ℝ :=
…

Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FinitePath

theorem OAI.DilutedSpinGlass.HeterogeneousMarks.pressure_mask_bound line 99

Source documentation

A finite-type truncation is controlled uniformly in all other disorder and parameters. The right side is the expected deleted log-factor mass.

theorem pressure_mask_bound (s : ℝ≥0) (T : KernelTower Ω L)
    (Q : (i : I) → Fin L → FiniteLaw (A i)) (m : Fin L → ℝ) (hm : ∀ j, 0 < m j)
    (base : FinitePath Ω L → ℝ)
    (factor : (i : I) → FinitePath Ω L → FinitePath (A i) L → ℝ)
    (keep : I → Prop) [DecidablePred keep] {C : ℝ} (hC : 0 ≤ C)
    (hfactor : ∀ i x y, |Real.log (factor i x y)| ≤ C) :
    |pressure ν s T Q m base factor -
      pressure ν s T Q m base (fun i x y => if keep i then factor i x y else 1)| ≤
        (s : ℝ) * ∫ i, (if keep i then 0 else C) ∂ν := by
…

Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.HeterogeneousMarks.pressure

theorem OAI.DilutedSpinGlass.HeterogeneousMarks.pressure_base_bound line 123

Source documentation

The entire countable perturbation costs at most its total expected count times the per-factor log bound. No finite-cutoff telescope is used.

theorem pressure_base_bound (s : ℝ≥0) (T : KernelTower Ω L)
    (Q : (i : I) → Fin L → FiniteLaw (A i)) (m : Fin L → ℝ) (hm : ∀ j, 0 < m j)
    (base : FinitePath Ω L → ℝ)
    (factor : (i : I) → FinitePath Ω L → FinitePath (A i) L → ℝ)
    {C : ℝ} (hC : 0 ≤ C) (hfactor : ∀ i x y, |Real.log (factor i x y)| ≤ C) :
    |pressure ν s T Q m base factor - KernelTower.backwardLog L T m base| ≤ (s : ℝ)*C := by
…

Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.HeterogeneousMarks.pressure, OAI.DilutedSpinGlass.KernelTower.backwardLog

theorem OAI.DilutedSpinGlass.CountableReservoir.tail_integral_tendsto line 142
Source documentation
The truncation error tends to zero for every fixed full type law. This uses only total probability one, never a special fast decay of the weights.
```
theorem tail_integral_tendsto (ν : Measure ℕ) [IsProbabilityMeasure ν] {C : ℝ} (hC : 0 ≤ C) :
    Tendsto (fun K : ℕ => ∫ i : ℕ, (if i < K then 0 else C) ∂ν) atTop (𝓝 0) := by
…
```

theorem OAI.DilutedSpinGlass.CountableReservoir.integral_pi_perm line 165

Source documentation

The countable root labels are genuinely iid under finite permutations.

theorem integral_pi_perm {n : ℕ} (σ : Equiv.Perm (Fin n)) (f : (Fin n → I) → ℝ) :
    (∫ roots, f (roots ∘ σ) ∂Measure.pi (fun _ : Fin n => ν)) =
      ∫ roots, f roots ∂Measure.pi (fun _ : Fin n => ν) := by
…

theorem OAI.DilutedSpinGlass.CountableReservoir.integral_pi_cons line 172

Source documentation

A new label has precisely the same independent law as each old label.

theorem integral_pi_cons (n : ℕ) (f : (Fin (n+1) → I) → ℝ) {B : ℝ}
    (hf : ∀ roots, |f roots| ≤ B) :
    (∫ roots, f roots ∂Measure.pi (fun _ : Fin (n+1) => ν)) =
      ∫ i, ∫ roots, f (Fin.cons i roots) ∂Measure.pi (fun _ : Fin n => ν) ∂ν := by
…

theorem OAI.DilutedSpinGlass.CountableReservoir.integral_pi_equivariant line 189

theorem OAI.DilutedSpinGlass.CountableReservoir.poisson_add_label line 203

Source documentation

Palm for the full shared countable reservoir. It does not delete the selected type or truncate the other types in the remaining law.

theorem poisson_add_label (s : ℝ≥0)
    (F : (n : ℕ) → (Fin n → I) → Fin n → ℝ) {B : ℝ}
    (hB : ∀ n roots q, |F n roots q| ≤ B)
    (hF : ∀ n (σ : Equiv.Perm (Fin n)) roots q, F n (roots ∘ σ) q = F n roots (σ q)) :
    (∫ n : ℕ, ∫ roots, ∑ q, F n roots q
      ∂Measure.pi (fun _ : Fin n => ν) ∂poissonMeasure s) =
      (s : ℝ) * ∫ n : ℕ, ∫ i, ∫ roots, F (n+1) (Fin.cons i roots) 0
        ∂Measure.pi (fun _ : Fin n => ν) ∂ν ∂poissonMeasure s := by
…

Mentions: OAI.DilutedSpinGlass.q