OAI/Probability/DilutedSpin/CountedSpinMean.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DilutedSpinGlass.SizeCoupling.measurable_spinMean line 17

   Source documentation

   Measurability for the literal root before quenched averaging. Only the interaction table values are read; auxiliary factorization witnesses are not.

   theorem measurable_spinMean {N p k l r : ℕ} [NeZero N] {A : Fin l → Type}
       [∀ i, Fintype (A i)]
       (Q : (i : Fin l) → Fin (r+1) → FiniteLaw (A i)) (m : Fin (r+1) → ℝ)
       (theta : Z → Fin k → InteractionSample p) (h : Z → Fin N → ℝ)
       (ψ : (i : Fin l) → Spin → FinitePath (A i) (r+1) → ℝ)
       (hθ : ∀ j σ, Measurable (fun z => (theta z j).1 σ))
       (hh : ∀ i, Measurable (fun z => h z i)) :
       Measurable (fun z => spinMean Q m (theta z) (h z) ψ) := by
   …

   Mentions: OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.InteractionSample, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.SizeCoupling.spinMean

2. lemma OAI.DilutedSpinGlass.SizeCoupling.finite_logWeight_bound line 37
3. theorem OAI.DilutedSpinGlass.SizeCoupling.spinMean_bound line 51
4. def OAI.DilutedSpinGlass.SizeCoupling.countedMean line 73

   Source documentation

   Quenched mean at fixed physical and perturbation counts, under one common countable type law. Marks retain their own finite alphabets.

   noncomputable def countedMean (μ : Measure X) (ξ : Measure Y) (ν : Measure I)
       {p r N : ℕ} [NeZero N] (theta : X → InteractionSample p) (field : Y → ℝ)
       (Q : (i : I) → Fin (r+1) → FiniteLaw (A i)) (m : Fin (r+1) → ℝ)
       (ψ : (i : I) → Spin → FinitePath (A i) (r+1) → ℝ) (k l : ℕ) : ℝ :=
   …

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

5. lemma OAI.DilutedSpinGlass.SizeCoupling.abs_integral_le_const line 82
6. theorem OAI.DilutedSpinGlass.SizeCoupling.countedMean_bound line 89
7. theorem OAI.DilutedSpinGlass.SizeCoupling.measurable_countedIntegrand line 107

   Source documentation

   Joint measurability in the genuine independent physical roots.

   theorem measurable_countedIntegrand {p r N : ℕ} [NeZero N]
       (theta : X → InteractionSample p) (field : Y → ℝ)
       (hθ : ∀ σ, Measurable (fun x => (theta x).1 σ)) (hh : Measurable field)
       (Q : (i : I) → Fin (r+1) → FiniteLaw (A i)) (m : Fin (r+1) → ℝ)
       (ψ : (i : I) → Spin → FinitePath (A i) (r+1) → ℝ)
       (k l : ℕ) (a : RootPath I l) :
       Measurable (fun z : RootPath X k × RootPath Y N =>
         spinMean (fun j => Q (rootArray l a j)) m (fun j => theta (rootArray k z.1 j))
           (fun i => field (rootArray N z.2 i)) (fun j => ψ (rootArray l a j))) := by
   …

   Mentions: OAI.DilutedSpinGlass.InteractionSample, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.RootPath, OAI.DilutedSpinGlass.SizeCoupling.spinMean, OAI.DilutedSpinGlass.rootArray

8. theorem OAI.DilutedSpinGlass.FiniteLaw.abs_expect_sub_le line 131
9. theorem OAI.DilutedSpinGlass.SizeCoupling.spinRoot_interaction_step line 141
10. theorem OAI.DilutedSpinGlass.SizeCoupling.spinMean_interaction_step line 155
11. theorem OAI.DilutedSpinGlass.SizeCoupling.spinRoot_mark_step line 176

    Source documentation

    Deleting one realized factor integrates out only its own independent marks. The surviving factors keep their alphabets and level priors exactly.

    theorem spinRoot_mark_step {N p k l r : ℕ} {A : Fin (l+1) → Type}
        [∀ i, Fintype (A i)]
        (Q : (i : Fin (l+1)) → Fin (r+1) → FiniteLaw (A i)) (m : Fin (r+1) → ℝ)
        (hm : ∀ j, 0 < m j) (theta : Fin k → InteractionSample p) (h : Fin N → ℝ)
        (indices : Fin k → Fin p → Fin N) (sites : Fin (l+1) → Fin N)
        (ψ : (i : Fin (l+1)) → Spin → FinitePath (A i) (r+1) → ℝ)
        {D : ℝ} (hψ : ∀ σ a, |Real.log (ψ 0 σ a)| ≤ D) :
        |spinRoot Q m theta h indices sites ψ-
          spinRoot (fun j => Q j.succ) m theta h indices (fun j => sites j.succ) (fun j => ψ j.succ)| ≤ D := by
    …

    Mentions: OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.InteractionSample, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.SizeCoupling.spinRoot

12. theorem OAI.DilutedSpinGlass.SizeCoupling.spinMean_mark_step line 203