OAI/Probability/DilutedSpin/PhysicalAverages.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DilutedSpinGlass.probabilistic_center_bound line 13

    Source documentation

    Integrate a deterministic logarithmic stability estimate without imposing moments beyond the integrable envelope.

    theorem probabilistic_center_bound {X : Type*} [MeasurableSpace X]
    (μ : Measure X) [IsProbabilityMeasure μ] {f g : X → ℝ} {c : ℝ}
    (hf : AEStronglyMeasurable f μ) (hg : Integrable g μ)
    (hb : ∀ᵐ x ∂μ, |f x-c| ≤ g x) :
    Integrable f μ ∧ |(∫ x, f x ∂μ)-c| ≤ ∫ x, g x ∂μ := by
…
  2. def OAI.DilutedSpinGlass.fieldAverage line 29
  3. def OAI.DilutedSpinGlass.disorderAverage line 33
  4. def OAI.DilutedSpinGlass.interactionMoment line 37
  5. def OAI.DilutedSpinGlass.fieldMoment line 40
  6. theorem OAI.DilutedSpinGlass.indexAverage_integrable_and_fieldAverage_bound line 43
  7. theorem OAI.DilutedSpinGlass.stronglyMeasurable_fieldAverage line 67
  8. theorem OAI.DilutedSpinGlass.fieldAverage_integrable_and_disorderAverage_bound line 72
  9. theorem OAI.DilutedSpinGlass.disorderAverage_integrable_and_pressure_bound line 98