OAI/Probability/DilutedSpin/ParameterPalm.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.parameter_dictionary_palm line 26

   Source documentation

   Actual parameter-score Palm inequality: all old factors are the literal full dictionary factors at u, including the selected type.

   theorem parameter_dictionary_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)
       (hab : ∀ j, a j ≤ b j) (hI : ∀ j, Icc (a j) (b j) ⊆ Icc (-(1:ℝ)/4) (1/4))
       (ht : ∀ j, |t j| ≤ 1/4)
       (hD : ∀ i x y, |D i x y| ≤ 1) (hE : ∀ i x y, |E i x y| ≤ 1)
       (hc : 0 < ν.real {j}) (hs : 0 < s) :
       |externalCovariance ξ μ (ν.prod τ) (τ.map (fun q => (j,q))) r s S anchor T Q m base
         (parameterFactor Prod.fst a b t D E u) D E f (t j) (boundParameter (a j) (b j) (u j))| ≤
         B * (parameterError ξ μ (ν.prod τ) r s T Q (fun l => m l.succ) base
           Prod.fst a b t D E j u / (ν.real {j}*(s:ℝ))) := by
   …

   Mentions: OAI.DilutedSpinGlass.RootPath, OAI.DilutedSpinGlass.HeterogeneousMarks.externalCovariance, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.HeterogeneousMarks.parameterFactor, OAI.DilutedSpinGlass.boundParameter, OAI.DilutedSpinGlass.HeterogeneousMarks.parameterError