RegularDepth.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DilutedSpinGlass.fullRoot_variance_eq line 16
def OAI.DilutedSpinGlass.DepthAverage.normalized line 70
def OAI.DilutedSpinGlass.DepthAverage.Regular line 74
Source documentation
Exactly the separated, interior distinct-coordinate domain of decor:average-definition. Ancestry/order restrictions may further restrict it.
```
def Regular (η : ℝ) (q : α → Fin L) : Prop :=
…
```
Mentions: OAI.DilutedSpinGlass.q
def OAI.DilutedSpinGlass.DepthAverage.shiftPerm line 78
lemma OAI.DilutedSpinGlass.DepthAverage.rotate_val_of_room line 81
lemma OAI.DilutedSpinGlass.DepthAverage.regular_room line 92
lemma OAI.DilutedSpinGlass.DepthAverage.normalized_shift_bounds line 99
theorem OAI.DilutedSpinGlass.DepthAverage.regular_shift_restrict line 119
Source documentation
Positive shifts of any subset of retained coordinates are truly +1, not modular wraparound, and send the regular domain into η/2 regularity. The fixed numerical threshold is deliberately generous and uniform.
```
theorem regular_shift_restrict {η : ℝ} (hη : 0<η) (hlarge : 4<η*(L:ℝ))
    (e : β → α) (he : Function.Injective e) (s : β → Bool)
    {q : α → Fin L} (hq : Regular η q) :
    Regular (η/2) (coordinateProjection e (fun i => shiftPerm (s i)) q) := by
…
```
Mentions: OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.DepthAverage.Regular, OAI.DilutedSpinGlass.DepthAverage.coordinateProjection, OAI.DilutedSpinGlass.DepthAverage.shiftPerm

theorem OAI.DilutedSpinGlass.DepthAverage.regular_fiber_fourthRoot_bound line 151

Source documentation

Concrete regular-depth fiber estimate, including arbitrary unused coordinates and independently shifted retained depths.

theorem regular_fiber_fourthRoot_bound {η : ℝ} (hη : 0<η) (hlarge : 4<η*(L:ℝ))
    (e : β → α) (he : Function.Injective e) (s : β → Bool)
    (D : (α → Fin L) → Prop) (hD : ∀ q, D q → Regular η q)
    (F : (β → Fin L) → ℝ) (hF : ∀ q, 0≤F q) :
    average D (fun q => Real.sqrt (Real.sqrt
      (F (coordinateProjection e (fun i => shiftPerm (s i)) q)))) ≤
      Real.sqrt (Real.sqrt (average (Regular (η/2)) F)) := by
…

Mentions: OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.DepthAverage.Regular, OAI.DilutedSpinGlass.DepthAverage.average, OAI.DilutedSpinGlass.DepthAverage.coordinateProjection, OAI.DilutedSpinGlass.DepthAverage.shiftPerm