GlobalSelectedError.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedError line 16

Source documentation

The literal unnormalised score error from pert:error, with the quenched center under the entire same-law reservoir disorder.

noncomputable def fullSelectedError
    (ξ : Fin M → Measure Y) (μ : Measure X) (ν : Measure I) (r s : ℝ≥0)
    (T : KernelTower Ω L) (Q : (i : I) → Fin L → FiniteLaw (A i)) (m : Fin L → ℝ)
    (base : RootPath Y M → (k : ℕ) → RootPath X k → FinitePath Ω L → ℝ)
    (sel : I → Bool) (fixed D E : (i : I) → FinitePath Ω L → FinitePath (A i) L → ℝ)
    (t u : ℝ) : ℝ :=
…

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

theorem OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedError_nonneg line 35
theorem OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_fullSelectedError line 39

theorem OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedError_split line 46

Source documentation

Conditional/root decomposition proved for the actual tilted score.

theorem fullSelectedError_split
    (hb : ∀ k y, Measurable (fun z : RootPath Y M × RootPath X k => base z.1 k z.2 y))
    (hD : ∀ i x y, |D i x y| ≤ 1) (hE : ∀ i x y, |E i x y| ≤ 1)
    {u : ℝ} (ht : |t| ≤ 1/4) (hu : |u| ≤ 1/4) :
    fullSelectedError ξ μ ν r s T Q m base sel fixed D E t u ≤
      (∫ z, fullSelectedThermal T Q m base sel fixed D E t z u ∂fullRootLaw ξ μ ν r s)+
        rootDeviation (fullRootLaw ξ μ ν r s) (fun z => fullSelectedRawScore T Q m base sel fixed D E t z u) := by
…

Mentions: OAI.DilutedSpinGlass.RootPath, OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedError, OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedThermal, OAI.DilutedSpinGlass.fullRootLaw, OAI.DilutedSpinGlass.rootDeviation, OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedRawScore

theorem OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedError_bound line 88