OAI/Probability/DilutedSpin/InsertionPoint.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.integral_conv_increment line 15
2. lemma OAI.DilutedSpinGlass.compoundPoisson_increment line 33

   Source documentation

   Exact old-system addition formula at the level of physical energy laws.

   lemma compoundPoisson_increment (r s : ℝ≥0) (μ : Measure E) [IsProbabilityMeasure μ]
       (hμ : Integrable id μ) {C : ℝ≥0} {f : E → ℝ} (hf : LipschitzWith C f) :
       (∫ x,f x ∂compoundPoisson (r+s) μ)-(∫ x,f x ∂compoundPoisson r μ)=
         ∫ x,∫ y,f (x+y)-f x ∂compoundPoisson s μ ∂compoundPoisson r μ := by
   …

   Mentions: OAI.DilutedSpinGlass.compoundPoisson

3. lemma OAI.DilutedSpinGlass.compoundPoisson_increment_rate_bound line 41
4. lemma OAI.DilutedSpinGlass.reservoir_increment_limit line 54

   Source documentation

   The reservoir deficit can be replaced by its exact limiting insertion rate, uniformly over the old energy and every finite auxiliary hierarchy.

   lemma reservoir_increment_limit (α : ℝ≥0) (q : ℕ) (μ : Measure E)
       [IsProbabilityMeasure μ] (hμ : Integrable id μ)
       (f : ℕ → E → ℝ) (hf : ∀ N,LipschitzWith 1 (f N)) :
       Tendsto (fun N : ℕ =>
         (∫ x,f N x ∂compoundPoisson (α*N) μ)-
         (∫ x,f N x ∂compoundPoisson (reservoirRate α q N) μ)-
         (∫ x,∫ y,f N (x+y)-f N x ∂compoundPoisson (α*q) μ
           ∂compoundPoisson (reservoirRate α q N) μ)) atTop (𝓝 0) := by
   …

   Mentions: OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.compoundPoisson, OAI.DilutedSpinGlass.reservoirRate

5. lemma OAI.DilutedSpinGlass.FiniteLaw.expect_double_integral line 82
6. lemma OAI.DilutedSpinGlass.FiniteLaw.expect_pi_bind line 115
7. def OAI.DilutedSpinGlass.mixedFactor line 139
8. lemma OAI.DilutedSpinGlass.mixedFactor_bound line 143
9. lemma OAI.DilutedSpinGlass.measurable_mixedFactor line 155
10. def OAI.DilutedSpinGlass.insertionPoint line 167
11. lemma OAI.DilutedSpinGlass.measurable_insertionPoint line 173
12. lemma OAI.DilutedSpinGlass.insertionPoint_bound line 183
13. lemma OAI.DilutedSpinGlass.integrable_insertionPoint line 196
14. lemma OAI.DilutedSpinGlass.insertionCoefficient_eq_integral_point line 204
15. lemma OAI.DilutedSpinGlass.integral_expected_insertionPoint line 209