OAI/Probability/DilutedSpin/ReservoirRate.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DilutedSpinGlass.reservoirRate line 12

    Source documentation

    The old-site Poisson intensity, written so that its deficit from αN is manifestly nonnegative. The exponent is p-1.

    noncomputable def reservoirRate (α : ℝ≥0) (q N : ℕ) : ℝ≥0 :=
…

    Mentions: OAI.DilutedSpinGlass.q

  2. lemma OAI.DilutedSpinGlass.reservoirRate_nonzero line 15
  3. lemma OAI.DilutedSpinGlass.reservoirRate_le line 20
  4. lemma OAI.DilutedSpinGlass.reservoirRate_lower line 24
  5. lemma OAI.DilutedSpinGlass.reservoirRate_deficit_le line 42
  6. lemma OAI.DilutedSpinGlass.reservoirRate_source line 48
  7. lemma OAI.DilutedSpinGlass.reservoirRate_tendsto line 57
  8. def OAI.DilutedSpinGlass.reservoirDistance line 64
  9. lemma OAI.DilutedSpinGlass.reservoirDistance_nonneg line 67
  10. lemma OAI.DilutedSpinGlass.reservoirDistance_tendsto line 71
  11. lemma OAI.DilutedSpinGlass.fullRoot_reservoirDistance line 80