OAI/Probability/DilutedSpin/JointRootParam.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DilutedSpinGlass.measurable_packRoot_param line 13

   Source documentation

   Joint measurability through both random counts, with an external parameter.

   theorem measurable_packRoot_param
       {F : RootPath Y M → (k : ℕ) → RootPath X k → (n : ℕ) → RootPath I n → U → ℝ}
       (hF : ∀ k n, Measurable (fun z : ((RootPath Y M × RootPath X k) × RootPath I n) × U => F z.1.1.1 k z.1.1.2 n z.1.2 z.2)) :
       Measurable (fun z : FullRootState Y X I M × U => packRoot (fun h k x n y => F h k x n y z.2) z.1) := by
   …

   Mentions: OAI.DilutedSpinGlass.RootPath, OAI.DilutedSpinGlass.FullRootState, OAI.DilutedSpinGlass.packRoot

2. theorem OAI.DilutedSpinGlass.fullRoot_count_memLp line 32
3. theorem OAI.DilutedSpinGlass.fullRoot_count_mean line 38