OAI/Probability/DilutedSpin/RegularNodeAverage.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.UniversalDictionary.physicalShapeAverage line 15

   Source documentation

   Regular depth-cube average of the literal physical covariance energy.

   noncomputable def physicalShapeAverage (M : Model p) (θB hB : ℝ) (N L : ℕ)
       (u : Spec L × ℕ → ℝ) (S : ReducedTopology) (η : ℝ) : ℝ :=
   …

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

2. lemma OAI.DilutedSpinGlass.UniversalDictionary.physicalShapeAverage_nonneg line 20
3. lemma OAI.DilutedSpinGlass.UniversalDictionary.physicalShapeAverage_le_one line 25
4. def OAI.DilutedSpinGlass.UniversalDictionary.physicalChildrenAverage line 31
5. lemma OAI.DilutedSpinGlass.UniversalDictionary.averaged_multileaf_scalar_bound line 35
6. lemma OAI.DilutedSpinGlass.UniversalDictionary.physicalChildMass_average line 52
7. lemma OAI.DilutedSpinGlass.UniversalDictionary.regular_node_average_inequality line 60
8. theorem OAI.DilutedSpinGlass.UniversalDictionary.regular_node_average line 106

   Source documentation

   Uniform averaged producer. All old/target experiments are chosen before N and u. The two old/delayed child contributions are controlled using full-cube fibers, never by restricting independently averaged copies to a diagonal.

   theorem regular_node_average (M : Model p) (θB hB : ℝ) (L : ℕ)
       (k : ℕ+) (hk : 2≤(k:ℕ)) (C : Fin k → ReducedTopology)
       {η : ℝ} (hη : 0<η) (hlarge : 4<η*(L+1:ℕ)) :
       let α := Option (ReducedTopology.node k hk C).Vertex
   …

   Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.ReducedTopology