OAI/Probability/DilutedSpin/SelectedRegularity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.selectedFactor_log_bound line 13
2. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_selected_correctedScore line 40

   Source documentation

   Joint parameter regularity of the fully tilted selected score at fixed labels. The countable random labels are reintroduced below.

   theorem measurable_selected_correctedScore {X : Type} [MeasurableSpace X]
       (T : KernelTower Ω L) (Q : (i : I) → Fin L → FiniteLaw (A i))
       (m : Fin L → ℝ) (base : X → FinitePath Ω L → ℝ) (roots : Fin n → I)
       (sel : I → Bool) (fixed D E : (i : I) → FinitePath Ω L → FinitePath (A i) L → ℝ)
       (hb : ∀ y, Measurable (fun x => base x y)) (t : ℝ) :
       Measurable (fun z : X × ℝ => selectedScore T Q m (base z.1) roots sel fixed D E t z.2+4*n*z.2) := by
   …

   Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.HeterogeneousMarks.selectedScore