OAI/Probability/DilutedSpin/GeneralRootArrayLaw.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.rootArrayEquiv line 12
2. lemma OAI.DilutedSpinGlass.rootArrayEquiv_apply line 17
3. theorem OAI.DilutedSpinGlass.measurePreserving_rootArray line 28

   Source documentation

   Exact law identification for arbitrary measurable disorder alphabets, including the continuous physical interaction tables and external fields.

   theorem measurePreserving_rootArray (μ : Measure X) [IsProbabilityMeasure μ] (n : ℕ) :
       MeasurePreserving (rootArrayEquiv (X := X) n) (rootLaw n (fun _ => μ))
   …

   Mentions: OAI.DilutedSpinGlass.rootArrayEquiv, OAI.DilutedSpinGlass.rootLaw

4. theorem OAI.DilutedSpinGlass.integral_rootArray_eq_pi line 40