OAI/Probability/DilutedSpin/TreeMeasurable.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DilutedSpinGlass.FiniteLaw.measurable_tilt_weight line 11
2. theorem OAI.DilutedSpinGlass.PrescribedTree.measurable_tilt_sample_weight line 27

   Source documentation

   Measurability of every finite prescribed-tree probability for the actual recursively tilted conditional kernels.

   theorem measurable_tilt_sample_weight {n : ℕ} (S : PrescribedTree n)
       (T : KernelTower Ω n) (m : Fin n → ℝ) {f : X → FinitePath Ω n → ℝ}
       (hf : ∀ y, Measurable (fun x => f x y)) (a : S.Sample Ω) :
       Measurable (fun x => (S.sampleLaw (KernelTower.tilt n T m (f x))).weight a) := by
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.KernelTower.tilt

3. theorem OAI.DilutedSpinGlass.PrescribedTree.measurable_tilt_sample_expect line 46