ConcreteHistory.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.UniversalDictionary.integrable_rootHistory line 34
def OAI.DilutedSpinGlass.UniversalDictionary.physicalHistoryCovariance line 63
Source documentation
The actual charge-weighted, sharing-constrained overlap history in the complete prescribed-tree physical reservoir, centered by its old test.
```
noncomputable def physicalHistoryCovariance (m : Fin (L+1) → ℝ)
    (S : PrescribedTree (L+1)) (anchorLeaf : S.Leaf)
    (M : Model p) (C H : ℝ) (N : ℕ) (u : Spec L×ℕ → ℝ)
    (a b : Fin r → Option (Fin k)) (d : Fin r → Fin L) (spinAnchor : Bool)
    (f : (S.Leaf → FinitePath (Fin N → Spin) (L+1)) → ℝ) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.UniversalDictionary.Spec, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.Spin
lemma OAI.DilutedSpinGlass.UniversalDictionary.physicalHistory_polarization line 75

theorem OAI.DilutedSpinGlass.UniversalDictionary.universal_history_selection line 98

Source documentation

The same selected physical sequence satisfies every finite sharing constraint and both anchor kinds, with no assumed identity producer.

theorem universal_history_selection (m : Fin (L+1) → ℝ)
    (M : Model p) {C H c : ℝ} (hC : 0 ≤ C) (hH : 0 ≤ H) (hc : 0 < c)
    (hθ : ∀ᵐ z ∂M.disorder.toMeasure, ∀ σ, |z.1 σ| ≤ C)
    (hh : ∀ᵐ h ∂M.field.toMeasure, |h| ≤ H)
    (hθi : Integrable (fun z : InteractionSample p => ‖z.1‖) M.disorder.toMeasure)
    (hhi : Integrable (fun h : ℝ => |h|) M.field.toMeasure)
    (hm : ∀ l, c ≤ m l) (hmono : Monotone m) (hend : m (Fin.last L) = 1)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ (Ns : ℕ → ℕ) (us : ℕ → Spec L×ℕ → ℝ), StrictMono Ns ∧
      (∀ n i, us n i ∈ Icc (probeLow i.2) (probeHigh i.2)) ∧
      (∀ n, ConcreteReservoir.increment (weights L) prior m direction anchor M (Ns n) (us n) ≤
        liminf (pressure M) atTop+ε) ∧
…

Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.InteractionSample, OAI.DilutedSpinGlass.UniversalDictionary.Spec, OAI.DilutedSpinGlass.probeLow, OAI.DilutedSpinGlass.probeHigh, OAI.DilutedSpinGlass.ConcreteReservoir.increment, OAI.DilutedSpinGlass.UniversalDictionary.weights, OAI.DilutedSpinGlass.UniversalDictionary.prior, OAI.DilutedSpinGlass.UniversalDictionary.direction, OAI.DilutedSpinGlass.UniversalDictionary.anchor, OAI.DilutedSpinGlass.pressure

lemma OAI.DilutedSpinGlass.HeterogeneousMarks.externalCoefficient_singleton line 139
lemma OAI.DilutedSpinGlass.UniversalDictionary.externalHistory_singleton line 165
lemma OAI.DilutedSpinGlass.UniversalDictionary.historyAverage_singleton line 184