AveragedMatrixSelection.lean`

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DilutedSpinGlass.DepthAverage.tendsto_average_zero line 15
Source documentation
At each fixed grid, there are only finitely many depth assignments. Thus the signed physical identity error can be averaged BEFORE the size limit.
```
theorem tendsto_average_zero (D : (α → Fin L) → Prop)
    (F : ℕ → (α → Fin L) → ℝ)
    (hF : ∀ q, Tendsto (fun n => F n q) atTop (𝓝 0)) :
    Tendsto (fun n => average D (F n)) atTop (𝓝 0) := by
…
```
Mentions: OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.DepthAverage.average
theorem OAI.DilutedSpinGlass.UniversalDictionary.joint_grid_averaged_selection line 36
Source documentation
The low-increment grid sequence simultaneously has its regular singleton base case and a vanishing normalized regular-cube matrix error. The old tree, target shape, labeling and charging denominator may all vary with the complete depth assignment. This is the actual shared-root signed covariance, not an absolute coefficient majorant or a diagonal restriction of two averages.
```
theorem joint_grid_averaged_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,
        ∀ d ∈ regularSingletonDepths L η,
…
```
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.regularSingletonDepths