OAI/Probability/DilutedSpin/GlobalSelectedConcentration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.full_selected_error_concentration line 17

   Source documentation

   An unconditional quantitative bound for the global-centered selected score on the actual two-Poisson-plus-field law. Selection changes no prior and does not discard any of the other perturbations.

   theorem full_selected_error_concentration
       (μ : Measure X) [IsProbabilityMeasure μ] (ν : Measure I) [IsProbabilityMeasure ν]
       (ξ : Fin M → Measure Y) [∀ j, IsProbabilityMeasure (ξ j)] (r s : ℝ≥0)
       (T : KernelTower Ω L) (Q : (i : I) → Fin L → FiniteLaw (A i))
       (m : Fin L → ℝ) {c : ℝ} (hc : 0 < c) (hm : ∀ j, c ≤ m j)
       (base : RootPath Y M → (k : ℕ) → RootPath X k → FinitePath Ω L → ℝ)
       (hbmeas : ∀ k y, Measurable (fun z : RootPath Y M × RootPath X k => base z.1 k z.2 y))
       (sel : I → Bool) (fixed D E : (i : I) → FinitePath Ω L → FinitePath (A i) L → ℝ)
       {B C : ℝ} (hC : 0 ≤ C)
       (hb : ∀ h k x y, |base h k x y| ≤ B+C*k)
       (hf : ∀ i x y, |Real.log (fixed i x y)| ≤ 1)
       (hD : ∀ i x y, |D i x y| ≤ 1) (hE : ∀ i x y, |E i x y| ≤ 1)
   …

   Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.RootPath, OAI.DilutedSpinGlass.FinitePath