OAI/Probability/DilutedSpin/FullRootPalm.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.selected_palm_averaged line 15
2. def OAI.DilutedSpinGlass.HeterogeneousMarks.fullInsertedTreeScore line 38
3. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.fullRoot_selected_palm line 55

   Source documentation

   Full-root Palm identity, including the original physical Poisson/sample and field laws. The surviving root law on the right is exactly the left law.

   theorem fullRoot_selected_palm
       (hb : ∀ k y, Measurable (fun z : RootPath Y M × RootPath X k => base z.1 k z.2 y))
       {B : ℝ} (hB : 0 ≤ B) (hf : ∀ x, |f x| ≤ B)
       (hD : ∀ i x y, |D i x y| ≤ 1) (hE : ∀ i x y, |E i x y| ≤ 1)
       (ht : |t| ≤ 1/4) (hu : |u| ≤ 1/4)
       (hA : ∀ i x y, 1/2 ≤ selectedFactor sel fixed D E t u i x y) :
       (∫ z, fullSelectedTreeScore S a T Q m base sel fixed D E t u f z ∂fullRootLaw ξ μ ν r s) =
         (s:ℝ) * ∫ z, fullInsertedTreeScore ν S a T Q m base
           (selectedFactor sel fixed D E t u) (selectedNumerator sel E) f z ∂fullRootLaw ξ μ ν r s := by
   …

   Mentions: OAI.DilutedSpinGlass.RootPath, OAI.DilutedSpinGlass.HeterogeneousMarks.selectedFactor, OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedTreeScore, OAI.DilutedSpinGlass.fullRootLaw, OAI.DilutedSpinGlass.HeterogeneousMarks.fullInsertedTreeScore, OAI.DilutedSpinGlass.HeterogeneousMarks.selectedNumerator