OAI/Probability/DilutedSpin/RegularPhysicalShift.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.ReducedTopology.childBranchCoordinates line 12
2. lemma OAI.DilutedSpinGlass.ReducedTopology.childBranchCoordinates_injective line 17
3. lemma OAI.DilutedSpinGlass.ReducedTopology.regular_child_branches line 23
4. theorem OAI.DilutedSpinGlass.UniversalDictionary.regular_physical_shift_average line 46

   Source documentation

   The uniform h_N bound on the FULL actual regular/admissible parent domain, with the literal physical root and exactly its proper-child embeddings. This has no geometry or ordinary-integrability hypothesis left to discharge.

   theorem regular_physical_shift_average (M : Model p) (θB hB : ℝ) (N L : ℕ)
       (u : Spec L × ℕ → ℝ) (k : ℕ+) (hk : 2≤(k:ℕ)) (C : Fin k → ReducedTopology)
       (η : ℝ) (hlarge : 1<η*(L+1:ℕ)) :
       let μ := fullRootLaw (fun _ : Fin N => M.field.toMeasure) (bondLaw M N)
   …

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