OAI/Probability/DilutedSpin/PalmError.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedTreeScore_one line 24
2. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.fullRoot_palm_error line 33

   Source documentation

   The Palm covariance bound under the same complete original reservoir. Normalization by a type mass c can be done after this identity; no root Poisson families have been deleted or resampled.

   theorem fullRoot_palm_error
       (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) (hs : 0 < s) :
       |(∫ z, fullInsertedTreeScore ν S a T Q m base
           (selectedFactor sel fixed D E t u) (selectedNumerator sel E) f z ∂fullRootLaw ξ μ ν r s) -
         (∫ z, fullSelectedTreeMean S T Q m base sel fixed D E t u f z ∂fullRootLaw ξ μ ν r s) *
         (∫ z, fullInsertedTreeScore ν S a T Q m base
           (selectedFactor sel fixed D E t u) (selectedNumerator sel E) (fun _ => 1) z ∂fullRootLaw ξ μ ν r s)| ≤
         B * fullSelectedError ξ μ ν r s T Q m base sel fixed D E t u / (s:ℝ) := by
   …

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