ConcentrationRate.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.scoreScale line 13
Source documentation
The scale prescribed by the manuscript; no enlarged moment hypothesis is used in the bounded-model concentration step.
```
noncomputable def scoreScale (N : ℕ) : ℝ := (N:ℝ)^((3:ℝ)/4)
```
def OAI.DilutedSpinGlass.scoreMargin line 14
lemma OAI.DilutedSpinGlass.sqrt_scoreScale_div line 16
lemma OAI.DilutedSpinGlass.sqrt_div_scoreMargin_scale line 22

theorem OAI.DilutedSpinGlass.score_envelope_normalize line 29

Source documentation

Exact normalization of the four-term concentration envelope.

theorem score_envelope_normalize {x K T ell w : ℝ} (hx : 0 < x) (hK : 0 ≤ K)
    (hT : 0 ≤ T) (hell : 0 < ell) (hw : 0 < w) :
    (Real.sqrt (T*x^((3:ℝ)/4))/ell+
      4*Real.sqrt (K*x)/(x^(-(1:ℝ)/8))+
      12*(x^(-(1:ℝ)/8))*(x^((3:ℝ)/4))/ell+
      Real.sqrt (x^((3:ℝ)/4)))/(w*x^((3:ℝ)/4)) =
    ((Real.sqrt T/ell+1)/w)*x^(-(3:ℝ)/8)+
      ((4*Real.sqrt K+12/ell)/w)*x^(-(1:ℝ)/8) := by
…

theorem OAI.DilutedSpinGlass.score_envelope_bound line 47

Source documentation

Monotonicity version used with the physical variance envelope.

theorem score_envelope_bound {x K T ell w v R : ℝ} (hx : 0 < x) (hK : 0 ≤ K)
    (hT : 0 ≤ T) (hell : 0 < ell) (hw : 0 < w) (hR : R ≤ K*x)
    (hv : v ≤ Real.sqrt (T*x^((3:ℝ)/4))/ell+
      4*Real.sqrt R/(x^(-(1:ℝ)/8))+
      12*(x^(-(1:ℝ)/8))*(x^((3:ℝ)/4))/ell+Real.sqrt (x^((3:ℝ)/4))) :
    v/(w*x^((3:ℝ)/4)) ≤
      ((Real.sqrt T/ell+1)/w)*x^(-(3:ℝ)/8)+
      ((4*Real.sqrt K+12/ell)/w)*x^(-(1:ℝ)/8) := by
…

lemma OAI.DilutedSpinGlass.scoreScale_le line 59
lemma OAI.DilutedSpinGlass.physical_score_variance_linear line 65
Source documentation
The variance bound required in normalization holds for any reservoir with interaction rate at most linear in N, and for s_N=N^(3/4).
```
lemma physical_score_variance_linear {N : ℕ} (hN : 1 ≤ N) {r C H R : ℝ}
    (hr : r ≤ R*N) :
    3*C^2*r+4*scoreScale N+2*H^2*N ≤ (3*C^2*R+4+2*H^2)*N := by
…
```
Mentions: OAI.DilutedSpinGlass.scoreScale
theorem OAI.DilutedSpinGlass.tendsto_score_rate line 74
Source documentation
Both prescribed normalized score rates vanish, including the thermal term; the constants may depend on the fixed type and depth.
```
theorem tendsto_score_rate (A B : ℝ) :
    Tendsto (fun N : ℕ => A*(N:ℝ)^(-(3:ℝ)/8)+B*(N:ℝ)^(-(1:ℝ)/8))
      atTop (𝓝 0) := by
…
```
lemma OAI.DilutedSpinGlass.unit_limsup_nonneg line 91
lemma OAI.DilutedSpinGlass.unit_limsup_le_one line 99

lemma OAI.DilutedSpinGlass.limsup_finite_sqrt_bound line 106

Source documentation

A finite-family limsup estimate, proved by taking the size limit before removing the positive scalar slack. No uniform size rate is used.

lemma limsup_finite_sqrt_bound {ι : Type*} [Fintype ι]
    (a e : ℕ → ℝ) (f : ι → ℕ → ℝ) {η b c k : ℝ}
    (hη : 0<η) (hc : 0≤c) (hk : 0≤k)
    (ha0 : ∀ n, 0≤a n) (ha1 : ∀ n, a n≤1)
    (hf1 : ∀ j n, f j n≤1) (he : Tendsto e atTop (𝓝 0))
    (hbound : ∀ n, η*a n≤b+2*e n+c*Real.sqrt (k*∑ j, Real.sqrt (f j n))) :
    η*limsup a atTop≤b+c*Real.sqrt (k*∑ j, Real.sqrt (limsup (f j) atTop)) := by
…

lemma OAI.MeasureTheory.integrable_triple_rotate line 160
lemma OAI.MeasureTheory.integrable_triple_middle_swap line 167
lemma OAI.MeasureTheory.integral_triple_rotate line 175
lemma OAI.MeasureTheory.integral_triple_middle_swap line 188