SingletonAverage.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.UniversalDictionary.regularSingletonAverage line 14
Source documentation
The unnormalized regular-depth average of the actual physical singleton covariance energy; L+1 is the physical height, not the number of RSB steps.
```
noncomputable def regularSingletonAverage (M : Model p) (C H : ℝ) (N : ℕ)
    (u : Spec L×ℕ → ℝ) (η : ℝ) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.UniversalDictionary.Spec
lemma OAI.DilutedSpinGlass.UniversalDictionary.regularSingletonAverage_nonneg line 19
lemma OAI.DilutedSpinGlass.UniversalDictionary.regularSingletonAverage_le line 24

theorem OAI.DilutedSpinGlass.UniversalDictionary.singleton_average_selection line 39

Source documentation

The base case V_(1,L)(eta) ≤ 1/(eta L) is stated as its stronger uniform eventual bound, without assuming existence of a covariance limit.

theorem singleton_average_selection (M : Model p) {C H : ℝ} (hC : 0 ≤ C) (hH : 0 ≤ H)
    (hθ : ∀ᵐ z ∂M.disorder.toMeasure, ∀ σ, |z.1 σ| ≤ C)
    (hh : ∀ᵐ h ∂M.field.toMeasure, |h| ≤ H)
    (hθi : Integrable (fun z : InteractionSample p => ‖z.1‖) M.disorder.toMeasure)
    (hhi : Integrable (fun h : ℝ => |h|) M.field.toMeasure)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ (Ns : ℕ → ℕ) (us : ℕ → Spec L×ℕ → ℝ), StrictMono Ns ∧
      (∀ n i, us n i ∈ Icc (probeLow i.2) (probeHigh i.2)) ∧
      (∀ n, ConcreteReservoir.increment (weights L) prior (gridExponents L) direction anchor M (Ns n) (us n) ≤
        liminf (pressure M) atTop+ε) ∧
      (∀ η : ℝ, 0 < η → ∀ t : ℝ, 0 < t → ∀ᶠ n in atTop,
        regularSingletonAverage M C H (Ns n+1) (us n) η ≤ ((L+1:ℕ):ℝ)⁻¹/η+t) := by
…

Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.InteractionSample, OAI.DilutedSpinGlass.UniversalDictionary.Spec, OAI.DilutedSpinGlass.probeLow, OAI.DilutedSpinGlass.probeHigh, OAI.DilutedSpinGlass.ConcreteReservoir.increment, OAI.DilutedSpinGlass.UniversalDictionary.weights, OAI.DilutedSpinGlass.UniversalDictionary.prior, OAI.DilutedSpinGlass.UniversalDictionary.gridExponents, OAI.DilutedSpinGlass.UniversalDictionary.direction, OAI.DilutedSpinGlass.UniversalDictionary.anchor, OAI.DilutedSpinGlass.pressure, OAI.DilutedSpinGlass.UniversalDictionary.regularSingletonAverage

theorem OAI.DilutedSpinGlass.UniversalDictionary.singleton_iterated_concentration line 60
Source documentation
Full iterated convergence formulation for actual single-leaf covariance: first reservoir size along the chosen physical sequence, then grid height. No interaction positivity or factorization is needed for this base case.
```
theorem singleton_iterated_concentration (M : Model p) {C H : ℝ} (hC : 0 ≤ C) (hH : 0 ≤ H)
    (hθ : ∀ᵐ z ∂M.disorder.toMeasure, ∀ σ, |z.1 σ| ≤ C)
    (hh : ∀ᵐ h ∂M.field.toMeasure, |h| ≤ H)
    (hθi : Integrable (fun z : InteractionSample p => ‖z.1‖) M.disorder.toMeasure)
    (hhi : Integrable (fun h : ℝ => |h|) M.field.toMeasure)
    {ε η ζ : ℝ} (hε : 0 < ε) (hη : 0 < η) (hζ : 0 < ζ) :
    ∃ L₀ : ℕ, ∀ L ≥ L₀,
      ∃ (Ns : ℕ → ℕ) (us : ℕ → Spec L×ℕ → ℝ), StrictMono Ns ∧
        (∀ n i, us n i ∈ Icc (probeLow i.2) (probeHigh i.2)) ∧
        (∀ n, ConcreteReservoir.increment (weights L) prior (gridExponents L) direction anchor M (Ns n) (us n) ≤
          liminf (pressure M) atTop+ε) ∧
        (∀ᶠ n in atTop, 0 ≤ regularSingletonAverage M C H (Ns n+1) (us n) η ∧
…
```
Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.InteractionSample, OAI.DilutedSpinGlass.UniversalDictionary.Spec, OAI.DilutedSpinGlass.probeLow, OAI.DilutedSpinGlass.probeHigh, OAI.DilutedSpinGlass.ConcreteReservoir.increment, OAI.DilutedSpinGlass.UniversalDictionary.weights, OAI.DilutedSpinGlass.UniversalDictionary.prior, OAI.DilutedSpinGlass.UniversalDictionary.gridExponents, OAI.DilutedSpinGlass.UniversalDictionary.direction, OAI.DilutedSpinGlass.UniversalDictionary.anchor, OAI.DilutedSpinGlass.pressure, OAI.DilutedSpinGlass.UniversalDictionary.regularSingletonAverage