OAI/Probability/DilutedSpin/FullSelectedRawConcentration.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedRawScore line 15
2. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedRawScore_eq line 23
3. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.full_selected_root_concentration line 34

   Source documentation

   The actual selected score, with the auxiliary convex correction removed.

   theorem full_selected_root_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