OAI/Probability/DilutedSpin/UpperMoments.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.compoundPoisson_superposition_centered line 15

   Source documentation

   Superposition with null marks permitted: equality of the centered mark characteristic exponents is enough, without equality of the raw intensities.

   lemma compoundPoisson_superposition_centered (r s t : ℝ≥0)
       (μ ν τ : Measure E) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] [IsProbabilityMeasure τ]
       (h : ∀ L : StrongDual ℝ E, (r:ℂ)*(charFunDual μ L-1) =
         (s:ℂ)*(charFunDual ν L-1)+(t:ℂ)*(charFunDual τ L-1)) :
       compoundPoisson r μ = compoundPoisson s ν ∗ compoundPoisson t τ := by
   …

   Mentions: OAI.DilutedSpinGlass.compoundPoisson

2. lemma OAI.DilutedSpinGlass.charFunDual_centered_map line 26
3. def OAI.DilutedSpinGlass.factorCut line 45

   Source documentation

   Coordinatewise zero cutoff, retaining iid f and independence from b.

   noncomputable def factorCut (R : ℝ) (f : Spin → ℝ) : Spin → ℝ :=
   …

   Mentions: OAI.DilutedSpinGlass.Spin

4. lemma OAI.DilutedSpinGlass.measurable_factorCut line 48
5. lemma OAI.DilutedSpinGlass.factorCut_bound line 51
6. lemma OAI.DilutedSpinGlass.factorCut_product line 57
7. lemma OAI.DilutedSpinGlass.factorCut_product_lt_one line 67
8. def OAI.DilutedSpinGlass.patternFeature line 76
9. lemma OAI.DilutedSpinGlass.measurable_patternFeature line 79
10. lemma OAI.DilutedSpinGlass.patternFeature_bound line 87
11. lemma OAI.DilutedSpinGlass.integral_b_factors line 98

    Source documentation

    Independence of b and the iid factors, applied to actual measurable coordinate tests rather than assuming a replica coefficient formula.

    lemma integral_b_factors {p : ℕ} (M : Model p) (hM : Admissible M) (n : ℕ)
        (g : Fin p → (Spin → ℝ) → ℝ) (hg : ∀ l,Measurable (g l)) :
        (∫ z : InteractionSample p,(-z.2.2.1)^n*(∏ l,g l (z.2.2.2 l)) ∂M.disorder.toMeasure) =
          (∫ z : InteractionSample p,(-z.2.2.1)^n ∂M.disorder.toMeasure)*
          ∏ l,∫ z : InteractionSample p,g l (z.2.2.2 l) ∂M.disorder.toMeasure := by
    …

    Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.Admissible, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.InteractionSample

12. lemma OAI.DilutedSpinGlass.integral_factor_coordinate line 113
13. lemma OAI.DilutedSpinGlass.upper_pattern_moment line 121

    Source documentation

    All coordinates may use different replica-pattern laws. This includes the old spin replicas and fresh message replicas on every prescribed topology.

    lemma upper_pattern_moment {p n : ℕ} (M : Model p) (hM : Admissible M)
        (j : Fin p) (R : ℝ) (P : Fin p → FiniteLaw (Fin n → Spin)) :
        (∫ z : InteractionSample p,(-z.2.2.1)^n*
          (FiniteLaw.pi P).expect (fun s => ∏ a : Fin n,∏ l : Fin p,factorCut R (z.2.2.2 l) (s l a))
          ∂M.disorder.toMeasure) =
          (∫ z : InteractionSample p,(-z.2.2.1)^n ∂M.disorder.toMeasure)*
          ∏ l,∫ z : InteractionSample p,patternFeature R (P l) (z.2.2.2 j) ∂M.disorder.toMeasure := by
    …

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

14. lemma OAI.DilutedSpinGlass.product_one_distinguished line 140