OAI/Probability/DilutedSpin/PhysicalReservoirIncrement.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.SizeCoupling.energyCavityIncrement line 17
2. lemma OAI.DilutedSpinGlass.SizeCoupling.perturbedMean_reservoir_increment line 35

   Source documentation

   The actual finite-size physical increment at a common score intensity has its reservoir/cavity representation, with only the repeated-new-site and mark-location displacement errors.

   lemma perturbedMean_reservoir_increment
       (μ : Measure X) [IsProbabilityMeasure μ] (ξ : Measure Y) [IsProbabilityMeasure ξ]
       (ν : Measure I) [IsProbabilityMeasure ν] (α s : ℝ≥0)
       (theta : X → InteractionSample (q+1)) (field : Y → ℝ)
       (hθm : ∀ σ,Measurable (fun x => (theta x).1 σ)) (hhm : Measurable field)
       (hsym : ∀ e : Equiv.Perm (Fin (q+1)),IdentDistrib (fun x => (theta x).1)
         (fun x σ => (theta x).1 (fun i => σ (e i))) μ μ)
       (Q : (i : I) → Fin (L+1) → FiniteLaw (A i)) (m : Fin (L+1) → ℝ)
       (hm : ∀ d,0 < m d) (hend : m (Fin.last L)=1)
       (ψ : (i : I) → Spin → FinitePath (A i) (L+1) → ℝ)
       {H C D : ℝ} (hH : 0≤H) (hC : 0≤C) (hD : 0≤D)
       (hθ : ∀ x,‖(theta x).1‖≤C) (hh : ∀ y,|field y|≤H)
   …

   Mentions: OAI.DilutedSpinGlass.InteractionSample, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.FinitePath

3. lemma OAI.DilutedSpinGlass.rootMap_selectRoot line 106
4. lemma OAI.DilutedSpinGlass.PrescribedTree.measurable_activeEnergy line 123
5. lemma OAI.DilutedSpinGlass.PrescribedTree.activeEnergy_bound line 135
6. def OAI.DilutedSpinGlass.PrescribedTree.activeDatumRoot line 150
7. lemma OAI.DilutedSpinGlass.PrescribedTree.measurable_activeDatumRoot line 157
8. lemma OAI.DilutedSpinGlass.PrescribedTree.allocatedMean_selected line 173