GlobalSelectedAverage.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.PrescribedTree.pairObservableHistory line 19
Source documentation
Actual one-new-path history for an arbitrary two-path observable (in particular the empirical spin overlap). All unused old replicas are retained.
```
noncomputable def pairObservableHistory (T : KernelTower Ω n) (m : Fin (n+1) → ℝ)
    (S : PrescribedTree n) (a : S.Leaf) (d : ℕ)
    (R : FinitePath Ω n → FinitePath Ω n → ℝ) (f : Sample Ω S → ℝ) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample
lemma OAI.DilutedSpinGlass.PrescribedTree.pairObservableHistory_product line 30
lemma OAI.DilutedSpinGlass.PrescribedTree.pair_univ_erase line 35
theorem OAI.DilutedSpinGlass.PrescribedTree.pairObservableHistory_const line 44
Source documentation
Exact, old-tree-independent singleton-anchor coefficient at a fixed split.
```
theorem pairObservableHistory_const (T : KernelTower Ω n) (m : Fin (n+1) → ℝ)
    (hend : m (Fin.last n) = 1) (S : PrescribedTree n) (a : S.Leaf)
    (d : ℕ) (hd : d < n) (R : FinitePath Ω n → FinitePath Ω n → ℝ) :
    pairObservableHistory T m S a d R (fun _ => 1) =
      (m ⟨d,by omega⟩ - m ⟨d+1,by omega⟩) * KernelTower.pairExpect n T d R := by
…
```
Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.pairObservableHistory, OAI.DilutedSpinGlass.KernelTower.pairExpect
lemma OAI.DilutedSpinGlass.PrescribedTree.erase_eq_of_two line 72

theorem OAI.DilutedSpinGlass.HeterogeneousMarks.full_selected_error_split_average line 97

Source documentation

The actual complete score error, split into its thermal and disorder parts. The only bounds used are the perturbation factors and positive exponents.

theorem full_selected_error_split_average
    (ξ : Fin M → Measure Y) [∀ j, IsProbabilityMeasure (ξ j)]
    (μ : Measure X) [IsProbabilityMeasure μ] (ν : Measure I) [IsProbabilityMeasure ν] (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 → ℝ)
    (hb : ∀ 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 → ℝ)
    (hD : ∀ i x y, |D i x y| ≤ 1) (hE : ∀ i x y, |E i x y| ≤ 1)
    {t a b c : ℝ} (ht : |t| ≤ 1/4) (hab : a < b) (hc : 0 < c)
    (hm : ∀ j, c ≤ m j) (hI : Icc a b ⊆ Icc (-(1:ℝ)/4) (1/4)) :
    (∫ u in a..b, fullSelectedError ξ μ ν r s T Q m base sel fixed D E t u) ≤
      Real.sqrt ((b-a)*(4+4*(b-a))/c*(s:ℝ))+
…

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