OAI/Probability/DilutedSpin/JointRootLaw.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.compoundRootLaw line 12

   Source documentation

   The actual independent Poisson container of iid root labels.

   noncomputable def compoundRootLaw {X : Type} [MeasurableSpace X]
       (μ : Measure X) (r : ℝ≥0) : Measure (Sigma (RootPath X)) :=
   …

   Mentions: OAI.DilutedSpinGlass.RootPath

2. instance OAI.DilutedSpinGlass.compoundRootLaw_prob line 16
3. theorem OAI.DilutedSpinGlass.measurable_prodSigma line 21
4. abbrev OAI.DilutedSpinGlass.FullRootState line 30
5. def OAI.DilutedSpinGlass.fullRootLaw line 33
6. instance OAI.DilutedSpinGlass.fullRootLaw_prob line 37
7. def OAI.DilutedSpinGlass.packRoot line 43
8. theorem OAI.DilutedSpinGlass.measurable_packRoot line 46
9. theorem OAI.DilutedSpinGlass.fullRoot_memLp_linear line 61
10. theorem OAI.DilutedSpinGlass.fullRoot_integrable_quadratic line 77

    Source documentation

    Quadratic envelopes allow both the pressure and its square to be passed through the two independent compound laws, without any count cut-off.

    theorem fullRoot_integrable_quadratic
        {F : RootPath Y M → (k : ℕ) → RootPath X k → (n : ℕ) → RootPath I n → ℝ}
        (hF : ∀ k n, Measurable (fun z : (RootPath Y M × RootPath X k) × RootPath I n => F z.1.1 k z.1.2 n z.2))
        {B C D : ℝ} (hb : ∀ h k x n y, |F h k x n y| ≤ B+C*(k:ℝ)^2+D*(n:ℝ)^2) :
        Integrable (packRoot F) (fullRootLaw ξ μ ν r s) := by
    …

    Mentions: OAI.DilutedSpinGlass.RootPath, OAI.DilutedSpinGlass.packRoot, OAI.DilutedSpinGlass.fullRootLaw

11. theorem OAI.DilutedSpinGlass.twoCompound_integrable_quadratic line 92
12. theorem OAI.DilutedSpinGlass.integral_fullRootLaw_quadratic line 110

    Source documentation

    Exact Fubini identity for the full root law, with all count-dependent root spaces and all physical fields retained.

    theorem integral_fullRootLaw_quadratic
        {F : RootPath Y M → (k : ℕ) → RootPath X k → (n : ℕ) → RootPath I n → ℝ}
        (hF : ∀ k n, Measurable (fun z : (RootPath Y M × RootPath X k) × RootPath I n => F z.1.1 k z.1.2 n z.2))
        {B C D : ℝ} (hb : ∀ h k x n y, |F h k x n y| ≤ B+C*(k:ℝ)^2+D*(n:ℝ)^2) :
        (∫ z, packRoot F z ∂fullRootLaw ξ μ ν r s) =
          ∫ h, ∫ k : ℕ, ∫ x, ∫ n : ℕ, ∫ y, F h k x n y
            ∂rootLaw n (fun _ => ν) ∂poissonMeasure s ∂rootLaw k (fun _ => μ)
              ∂poissonMeasure r ∂rootLaw M ξ := by
    …

    Mentions: OAI.DilutedSpinGlass.RootPath, OAI.DilutedSpinGlass.packRoot, OAI.DilutedSpinGlass.fullRootLaw, OAI.DilutedSpinGlass.rootLaw