OAI/Probability/DilutedSpin/PhysicalShapeError.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.UniversalDictionary.physicalTreeDeviation line 14
2. lemma OAI.DilutedSpinGlass.UniversalDictionary.physicalTreeDeviation_le_variance line 25
3. def OAI.DilutedSpinGlass.UniversalDictionary.physicalShapeDeviation line 32
4. lemma OAI.DilutedSpinGlass.UniversalDictionary.physicalShapeDeviation_nonneg line 43
5. lemma OAI.DilutedSpinGlass.UniversalDictionary.physicalShapeDeviation_qExpect_le line 47
6. theorem OAI.DilutedSpinGlass.UniversalDictionary.physicalShapeError_tendsto line 57

   Source documentation

   The complete finite-shape MAD error for the actual selected reservoir tends to zero. This is the error required by the empirical pattern comparison.

   theorem physicalShapeError_tendsto (M : Model p) (C H : ℝ)
       (Ns : ℕ → ℕ → ℕ) (us : (L : ℕ) → ℕ → Spec L×ℕ → ℝ)
       (hcontrol : ∀ L, FullShapeControl M C H L (Ns L) (us L)) (k : ℕ) :
       Tendsto (fun L => limsup (fun n => qExpect (grid (L+1) 0 (L+1))
         (physicalShapeDeviation M C H (Ns L n+1) L (us L n)) k (single (L+1))) atTop)
         atTop (𝓝 0) := by
   …

   Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.UniversalDictionary.Spec, OAI.DilutedSpinGlass.UniversalDictionary.FullShapeControl, OAI.DilutedSpinGlass.UniversalDictionary.physicalShapeDeviation

7. lemma OAI.DilutedSpinGlass.FiniteLaw.mixedDeviation_le_two line 87
8. lemma OAI.DilutedSpinGlass.PrescribedTree.shapeDeviation_bound line 100
9. lemma OAI.DilutedSpinGlass.PrescribedTree.qExpect_shape_bound line 117
10. lemma OAI.DilutedSpinGlass.limsup_le_of_vanishing_error line 126