OAI/Probability/DilutedSpin/MixtureMeasures.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DilutedSpinGlass.measurable_sigmaMk line 15
2. theorem OAI.DilutedSpinGlass.measurable_sigmaUncurry line 20
3. def OAI.DilutedSpinGlass.familyKernel line 31
4. instance OAI.DilutedSpinGlass.familyKernel_markov line 34
5. def OAI.DilutedSpinGlass.familyLaw line 41
6. instance OAI.DilutedSpinGlass.familyLaw_prob line 44
7. theorem OAI.DilutedSpinGlass.familyLaw_integrable_bound line 59

   Source documentation

   Sufficient integrability on the genuine disjoint-union root law.

   theorem familyLaw_integrable_bound (f : (i : I) → X i → ℝ)
       (hf : ∀ i, Measurable (f i)) {B : I → ℝ} (hB : Integrable B μ)
       (hb : ∀ i x, |f i x| ≤ B i) :
       Integrable (fun z : Sigma X => f z.1 z.2) (familyLaw μ ν) := by
   …

   Mentions: OAI.DilutedSpinGlass.familyLaw

8. theorem OAI.DilutedSpinGlass.integral_familyLaw line 85
9. theorem OAI.DilutedSpinGlass.familyLaw_memLp_bound line 106

   Source documentation

   Square-integrability with a random-dimensional envelope; it includes independent physical and perturbation counts.

   theorem familyLaw_memLp_bound {I : Type*} {X : I → Type*}
       [MeasurableSpace I] [DiscreteMeasurableSpace I] [∀ i, MeasurableSpace (X i)]
       (μ : Measure I) (ν : ∀ i, Measure (X i)) [∀ i, IsProbabilityMeasure (ν i)]
       {f : (i : I) → X i → ℝ} (hf : ∀ i, Measurable (f i)) {B : I → ℝ}
       (hB : Integrable (fun i => (B i)^2) μ) (hb : ∀ i x, |f i x| ≤ B i) :
       MemLp (fun z : Sigma X => f z.1 z.2) 2 (familyLaw μ ν) := by
   …

   Mentions: OAI.DilutedSpinGlass.familyLaw

10. theorem OAI.DilutedSpinGlass.familyPoisson_count_integrable line 127
11. theorem OAI.DilutedSpinGlass.familyPoisson_count_mean line 134
12. theorem OAI.DilutedSpinGlass.familyPoisson_memLp_linear line 140