OAI/Probability/Ising/Interpolation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BufferedIsing.DSS.update line 10

   Source documentation

   The rational single-spin field update.

   noncomputable def update (a c : ℝ) : ℝ := (a + c) / (1 + a * c)

2. lemma OAI.BufferedIsing.DSS.update_den_pos line 12
3. lemma OAI.BufferedIsing.DSS.interpolation_positive_sum line 23
4. lemma OAI.BufferedIsing.DSS.interpolation_pair line 68
5. lemma OAI.BufferedIsing.DSS.one_sub_update line 85
6. lemma OAI.BufferedIsing.DSS.one_add_update line 91
7. theorem OAI.BufferedIsing.DSS.interpolation line 98

   Source documentation

   Finite-field interpolation with a common finite field parameter for both one-sided mixtures.

   theorem interpolation {a b c z : ℝ}
       (ha : -1 < a ∧ a < 1) (hb : -1 < b ∧ b < 1)
       (hab : b ≤ a) (hc : 0 ≤ c ∧ c < 1)
       (hz : 0 ≤ z) (hgap : a - b ≤ 2 * z) :
       ∃ d : ℝ, -1 < d ∧ d < 1 ∧
         update a c ≤ ((1 - c) / (1 + z * c)) * update a d +
           (1 - (1 - c) / (1 + z * c)) ∧
         ((1 - c) / (1 + z * c)) * update b d -
           (1 - (1 - c) / (1 + z * c)) ≤ update b (-c) := by
   …

   Mentions: OAI.BufferedIsing.DSS.update