CavityBounds.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DilutedSpinGlass.q_pos line 10
theorem OAI.DilutedSpinGlass.q_sum line 14
theorem OAI.DilutedSpinGlass.product_q_sum line 22
Source documentation
Product message probabilities have total mass exactly one.
```
theorem product_q_sum {p : ℕ} (x : Fin p → ℝ) :
    (∑ s : Fin p → Spin, ∏ l, q (x l) (s l)) = 1 := by
…
```
Mentions: OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.q

theorem OAI.DilutedSpinGlass.weighted_exp_bounds line 29

Source documentation

Uniform bounds on a finite probability-weighted exponential sum.

theorem weighted_exp_bounds {ι : Type*} [Fintype ι] (w f : ι → ℝ)
    (hw : ∀ i, 0 ≤ w i) (hs : ∑ i, w i = 1) {B : ℝ}
    (hf : ∀ i, |f i| ≤ B) :
    Real.exp (-B) ≤ ∑ i, w i * Real.exp (f i) ∧
      (∑ i, w i * Real.exp (f i)) ≤ Real.exp B := by
…

theorem OAI.DilutedSpinGlass.weighted_log_exp_bound line 47
theorem OAI.DilutedSpinGlass.edge_pos line 56
theorem OAI.DilutedSpinGlass.log_edge_bound line 64
Source documentation
The message-free uniform edge bound, with only the physical interaction norm.
```
theorem log_edge_bound {p : ℕ} (theta : Interaction p) (x : Fin p → ℝ) :
    |Real.log (edge theta x)| ≤ ‖theta‖ := by
…
```
Mentions: OAI.DilutedSpinGlass.Interaction, OAI.DilutedSpinGlass.edge
theorem OAI.DilutedSpinGlass.message_bound line 72
Source documentation
The uniform cavity-message bound; no message moments occur.
```
theorem message_bound {p : ℕ} (theta : Interaction p)
    (x : Fin (p - 1) → ℝ) (ε : Spin) : |message theta x ε| ≤ ‖theta‖ := by
…
```
Mentions: OAI.DilutedSpinGlass.Interaction, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.message
theorem OAI.DilutedSpinGlass.siteLog_bound line 81