OAI/Probability/DilutedSpin/CavityRateLimits.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.oneNewRate_tendsto line 11
2. lemma OAI.DilutedSpinGlass.reservoir_deficit_identity line 17
3. lemma OAI.DilutedSpinGlass.reservoir_deficit_tendsto line 31
4. lemma OAI.DilutedSpinGlass.cavity_bad_count line 39
5. def OAI.DilutedSpinGlass.cavityBadRate line 57
6. lemma OAI.DilutedSpinGlass.cavityBadRate_count line 61
7. lemma OAI.DilutedSpinGlass.cavityBadRate_nonneg line 70
8. lemma OAI.DilutedSpinGlass.cavityBadRate_tendsto line 75
9. def OAI.DilutedSpinGlass.cavityCoordinateEquiv line 95

   Source documentation

   Move the singled-out interaction coordinate to the distinguished last slot, preserving the relative order of all other slots.

   def cavityCoordinateEquiv {q : ℕ} (j : Fin (q+1)) : Equiv.Perm (Fin (q+1)) where
   …

   Mentions: OAI.DilutedSpinGlass.q

10. lemma OAI.DilutedSpinGlass.appendSpin_castSucc line 107
11. lemma OAI.DilutedSpinGlass.appendSpin_last line 112
12. lemma OAI.DilutedSpinGlass.cavityCoordinate_append line 116
13. lemma OAI.DilutedSpinGlass.cavity_coordinate_identDistrib line 125

    Source documentation

    iid coordinate symmetry is sufficient for all one-new-index classes to have the exact same interaction as the last-coordinate cavity convention.

    lemma cavity_coordinate_identDistrib {q : ℕ} {X : Type} [MeasurableSpace X]
        (μ : Measure X) (θ : X → Interaction (q+1))
        (hsym : ∀ e : Equiv.Perm (Fin (q+1)), IdentDistrib θ
          (fun z s => θ z (fun l => s (e l))) μ μ)
        (j : Fin (q+1)) :
        IdentDistrib (fun z (v : (Fin q → Spin) × Spin) => θ z (appendSpin v.1 v.2))
          (fun z (v : (Fin q → Spin) × Spin) => θ z (j.insertNth v.2 v.1)) μ μ := by
    …

    Mentions: OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.Interaction, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.appendSpin