OAI/Probability/DilutedSpin/FullSelectedConcentration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.full_selected_corrected_concentration line 18

   Source documentation

   Concentration of the actual selected corrected score under the full common reservoir law. The variance estimate is produced from replacement controls, not a premise. All unselected types keep their original factors and priors.

   theorem full_selected_corrected_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 → ℝ) (hm : ∀ j, 0 < 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