Model.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.DilutedSpinGlass.Spin line 10
Also declared: ComparatorChallenges/DilutedSpin.lean:12 (same declaration text).
def OAI.DilutedSpinGlass.spin line 12
Also declared: ComparatorChallenges/DilutedSpin.lean:14 (same declaration text).
abbrev OAI.DilutedSpinGlass.Interaction line 14
Also declared: ComparatorChallenges/DilutedSpin.lean:16 (same declaration text).
abbrev OAI.DilutedSpinGlass.InteractionSample line 17
Source documentation
One interaction together with its factorization witness: theta,a,b,f.
Also declared: ComparatorChallenges/DilutedSpin.lean:19 (same declaration text).
```
abbrev InteractionSample (p : ℕ) :=
…
```
structure OAI.DilutedSpinGlass.Model line 20
Also declared: ComparatorChallenges/DilutedSpin.lean:22 (same declaration text).
structure OAI.DilutedSpinGlass.Admissible line 27
Source documentation
Exactly the standing hypotheses (model:integrability through positivity). norm on the finite function space is max_s |theta(s)|.
Also declared: ComparatorChallenges/DilutedSpin.lean:29 (same declaration text).
```
structure Admissible {p : ℕ} (M : Model p) : Prop where
…
```
Mentions: OAI.DilutedSpinGlass.Model
def OAI.DilutedSpinGlass.logWeight line 52
Source documentation
Minus the Hamiltonian, with all index choices including repetitions.
Also declared: ComparatorChallenges/DilutedSpin.lean:54 (same declaration text).
```
noncomputable def logWeight {p N k : ℕ} (theta : Fin k → InteractionSample p)
    (h : Fin N → ℝ) (indices : Fin k → Fin p → Fin N) (σ : Fin N → Spin) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.InteractionSample, OAI.DilutedSpinGlass.Spin
def OAI.DilutedSpinGlass.logPartition line 56
Also declared: ComparatorChallenges/DilutedSpin.lean:58 (same declaration text).
def OAI.DilutedSpinGlass.pressure line 62
Source documentation
F_N, using an explicit uniform average over the independent index labels. The value at N=0 is irrelevant to the limit; valid system sizes are N>=1.
Also declared: ComparatorChallenges/DilutedSpin.lean:64 (same declaration text).
```
noncomputable def pressure {p : ℕ} (M : Model p) (N : ℕ) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.Model
def OAI.DilutedSpinGlass.q line 72
Also declared: ComparatorChallenges/DilutedSpin.lean:74 (same declaration text).
def OAI.DilutedSpinGlass.edge line 75
Also declared: ComparatorChallenges/DilutedSpin.lean:77 (same declaration text).
def OAI.DilutedSpinGlass.appendSpin line 79
Source documentation
Append the distinguished cavity spin in the last position.
Also declared: ComparatorChallenges/DilutedSpin.lean:81 (same declaration text).
```
def appendSpin {p : ℕ} (s : Fin (p - 1) → Spin) (ε : Spin) (l : Fin p) : Spin :=
…
```
Mentions: OAI.DilutedSpinGlass.Spin
def OAI.DilutedSpinGlass.message line 82
Also declared: ComparatorChallenges/DilutedSpin.lean:84 (same declaration text).
def OAI.DilutedSpinGlass.siteLog line 87
Also declared: ComparatorChallenges/DilutedSpin.lean:89 (same declaration text).

def OAI.DilutedSpinGlass.Hierarchy line 98

Source documentation

Nested probability laws: H_0=R and H_{j+1}=P(H_j), with weak topologies.

Also declared: ComparatorChallenges/DilutedSpin.lean:100 (same declaration text).

noncomputable def Hierarchy : ℕ → TopCat
  | 0 => TopCat.of ℝ
  | r + 1 => TopCat.of (ProbabilityMeasure (Hierarchy r))

/-- Logarithmic form of the conditional power means T_0 using independent
message labels. The current eta's are held fixed; only their descendants
are integrated. Physical disorder is a fixed argument of g throughout. -/

Mentions: OAI.DilutedSpinGlass.message

def OAI.DilutedSpinGlass.logMean line 105

Source documentation

Logarithmic form of the conditional power means T_0 using independent message labels. The current eta's are held fixed; only their descendants are integrated. Physical disorder is a fixed argument of g throughout.

Also declared: ComparatorChallenges/DilutedSpin.lean:107 (same declaration text).

noncomputable def logMean {ι : Type} [Fintype ι] :
    (r : ℕ) → ((ι → ℝ) → ℝ) → (Fin r → ℝ) → (ι → Hierarchy r) → ℝ
  | 0, g, _, x => g x
  | r + 1, g, m, eta =>
    Real.log (∫ x : ι → Hierarchy r,
      Real.exp (m 0 * logMean r g (fun i => m i.succ) x)
      ∂Measure.pi (fun i => (eta i).toMeasure)) / m 0

/-- Expectation over the root laws eta_0 of each independent message label.
This also gives the r=0 convention (iid real messages, no power means). -/

Mentions: OAI.DilutedSpinGlass.Hierarchy, OAI.DilutedSpinGlass.message

def OAI.DilutedSpinGlass.trialLog line 115
Source documentation
Expectation over the root laws eta_0 of each independent message label. This also gives the r=0 convention (iid real messages, no power means).
Also declared: ComparatorChallenges/DilutedSpin.lean:117 (same declaration text).
```
noncomputable def trialLog {ι : Type} [Fintype ι] (r : ℕ)
    (ζ : Hierarchy (r + 1)) (m : Fin r → ℝ) (g : (ι → ℝ) → ℝ) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.Hierarchy
def OAI.DilutedSpinGlass.Exponents line 121
Source documentation
Admissible exponents 0<m_1<...<m_r<1; vacuous at r=0.
Also declared: ComparatorChallenges/DilutedSpin.lean:123 (same declaration text).
```
def Exponents {r : ℕ} (m : Fin r → ℝ) : Prop :=
…
```
def OAI.DilutedSpinGlass.functional line 125
Source documentation
The exact finite-depth cavity functional B_r.
Also declared: ComparatorChallenges/DilutedSpin.lean:127 (same declaration text).
```
noncomputable def functional {p : ℕ} (M : Model p) (r : ℕ)
    (ζ : Hierarchy (r + 1)) (m : Fin r → ℝ) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.Hierarchy
def OAI.DilutedSpinGlass.phi line 137
Also declared: ComparatorChallenges/DilutedSpin.lean:139 (same declaration text).
def OAI.DilutedSpinGlass.variationalValue line 141
Also declared: ComparatorChallenges/DilutedSpin.lean:143 (same declaration text).