OAI/Probability/DilutedSpin/RegularCovarianceLimit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.DilutedSpinGlass.UniversalDictionary.ScheduledControl line 18

   Source documentation

   The two precise outputs of the shared physical reservoir selection used by the covariance induction. A witness is produced below from the model, with its low-increment and parameter bounds retained alongside it.

   structure ScheduledControl (M : Model p) (θB hB : ℝ) (L : ℕ)
       (Ns : ℕ → ℕ) (us : ℕ → Spec L×ℕ → ℝ) : Prop where
   …

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

2. def OAI.DilutedSpinGlass.UniversalDictionary.physicalShapeLimsup line 33
3. lemma OAI.DilutedSpinGlass.UniversalDictionary.physicalShapeLimsup_nonneg line 37
4. lemma OAI.DilutedSpinGlass.UniversalDictionary.physicalShapeLimsup_le_one line 43
5. lemma OAI.DilutedSpinGlass.UniversalDictionary.physicalShapeLimsup_leaf line 49
6. theorem OAI.DilutedSpinGlass.UniversalDictionary.physicalShapeLimsup_node line 61

   Source documentation

   The full node recursion after the N-limit; the charge is uniform in L, and the only signed-covariance errors have disappeared at fixed grid.

   theorem physicalShapeLimsup_node {M : Model p} {θB hB : ℝ}
       {Ns : ℕ → ℕ} {us : ℕ → Spec L×ℕ → ℝ} (h : ScheduledControl M θB hB L Ns us)
       (k : ℕ+) (hk : 2≤(k:ℕ)) (C : Fin k → ReducedTopology)
       {η : ℝ} (hη : 0<η) (hlarge : 4<η*(L+1:ℕ)) :
       η*physicalShapeLimsup M θB hB L Ns us (.node k hk C) η ≤
         4*((L+1:ℕ):ℝ)⁻¹ +
         2*nodeChargeConstant k hk C η*Real.sqrt (nodeShiftBudget k C/(L+1:ℕ)) +
         (4*nodeChargeConstant k hk C η+4*(nodeHistoryBudget k hk C:ℝ)+16*(k:ℝ))*
           Real.sqrt ((k:ℝ)*∑ j, Real.sqrt (physicalShapeLimsup M θB hB L Ns us (C j) (η/2))) := by
   …

   Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.UniversalDictionary.Spec, OAI.DilutedSpinGlass.UniversalDictionary.ScheduledControl, OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.UniversalDictionary.physicalShapeLimsup, OAI.DilutedSpinGlass.UniversalDictionary.nodeShiftBudget