OAI/Probability/DilutedSpin/DictionaryAnalytic.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.HeterogeneousMarks.dictionaryFactor line 24
2. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.dictionary_covariance_probe_bound line 32

   Source documentation

   A single old-reservoir analytic function is small at every prescribed probe. The trace j occurs only in the independently inserted mark; it is not erased from or changed inside the old ambient Poisson dictionary.

   theorem dictionary_covariance_probe_bound
       (u : K×ℕ → ℝ) (f : (S.Leaf → FinitePath Ω L) → ℝ) (q : K) (j : ℕ)
       (hb : ∀ k y, Measurable (fun z : RootPath Y M × RootPath X k => base z.1 k z.2 y))
       (hm : ∀ j : Fin L, m j.succ ≠ 0) (hmono : Monotone m) (hpos : ∀ j, 0 ≤ m j)
       (hroot : m 0 = 0) (hend : m (Fin.last L) = 1)
       {B : ℝ} (hB : 0 ≤ B) (hf : ∀ x, |f x| ≤ B)
       (hD : ∀ i v x y, |D i v x y| ≤ 1) (hE : ∀ i v x y, |E i v x y| ≤ 1)
       (hc : 0 < ν.real {(q,j)}) (hs : 0 < s) :
       |externalCovariance ξ μ (ν.prod τ) (τ.map (fun v => ((q,0),v))) r s S anchor T
         (fun i => Q i.1.1) m base (dictionaryFactor D E u)
         (fun i => D i.1.1 i.2) (fun i => E i.1.1 i.2) f (extractionProbe j) 0| ≤
         4*(4+8*(S.leaves:ℝ))*B*extractionProbe j^(j+4) +
   …

   Mentions: OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.RootPath, OAI.DilutedSpinGlass.HeterogeneousMarks.externalCovariance, OAI.DilutedSpinGlass.HeterogeneousMarks.dictionaryFactor, OAI.DilutedSpinGlass.extractionProbe