OAI/Probability/DilutedSpin/ClippedModelFacts.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.clippedModel_interaction_bounded line 12
2. lemma OAI.DilutedSpinGlass.clippedModel_field_bounded line 19
3. lemma OAI.DilutedSpinGlass.clippedModel_interaction_integrable line 25
4. lemma OAI.DilutedSpinGlass.clippedModel_field_integrable line 29
5. lemma OAI.DilutedSpinGlass.clippedModel_symmetric line 33
6. lemma OAI.DilutedSpinGlass.clip_interaction_difference_integrable line 48
7. lemma OAI.DilutedSpinGlass.clip_field_difference_integrable line 58
8. def OAI.DilutedSpinGlass.replicaInsertionMoment line 77
9. lemma OAI.DilutedSpinGlass.replicaInsertion_combination line 85

   Source documentation

   The literal order-n replica coefficient of the three independent-label insertions. The old spin-pattern law P and fresh-label spin-pattern law B are arbitrary; their laws are not assumed to agree.

   lemma replicaInsertion_combination {p n : ℕ} (M : Model p) (hM : Admissible M)
       (j : Fin p) (R : ℝ) (P B : FiniteLaw (Fin n → Spin)) :
       replicaInsertionMoment M R (fun _ : Fin p => P) -
         (p:ℝ)*replicaInsertionMoment M R (fun l : Fin p => if l=j then P else B) +
         ((p-1:ℕ):ℝ)*replicaInsertionMoment M R (fun _ : Fin p => B) =
       (∫ z : InteractionSample p,(-z.2.2.1)^n ∂M.disorder.toMeasure)*
         ((∫ z : InteractionSample p,patternFeature R P (z.2.2.2 j) ∂M.disorder.toMeasure)^p -
          (p:ℝ)*(∫ z : InteractionSample p,patternFeature R P (z.2.2.2 j) ∂M.disorder.toMeasure)*
            (∫ z : InteractionSample p,patternFeature R B (z.2.2.2 j) ∂M.disorder.toMeasure)^(p-1) +
          ((p-1:ℕ):ℝ)*(∫ z : InteractionSample p,patternFeature R B (z.2.2.2 j) ∂M.disorder.toMeasure)^p) := by
   …

   Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.Admissible, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.replicaInsertionMoment, OAI.DilutedSpinGlass.InteractionSample, OAI.DilutedSpinGlass.patternFeature

10. lemma OAI.DilutedSpinGlass.replicaInsertion_coefficient_nonpos line 113