OAI/Probability/InvariantIsing/Spectral/SpectralReplicaLaw.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Actual spectral overlap array laws retain the common rotation disorder.

  1. def OAI.InvariantIsing.spectralJointEntry line 15
  2. lemma OAI.InvariantIsing.spectralJointEntry_spectral line 22
  3. lemma OAI.InvariantIsing.spectralJointEntry_tree line 27
  4. lemma OAI.InvariantIsing.measurable_spectralJointEntry line 32
  5. def OAI.InvariantIsing.spectralReplicaArray line 46
  6. lemma OAI.InvariantIsing.measurable_spectralReplicaArray line 51
  7. def OAI.InvariantIsing.disorderReplicaLaw line 75

    Source documentation

    Keeping the external disorder in the sampled space is essential: projected overlaps depend on the same rotation as the Gibbs measure.

    def disorderReplicaLaw {Ω X : Type*} [MeasurableSpace Ω] [MeasurableSpace X]
    [Countable X] [MeasurableSingletonClass X] (P : Measure Ω) (ν : Ω → Measure X)
    (hν : Measurable ν) [∀ ω, IsProbabilityMeasure (ν ω)] : Measure (Ω × (ℕ → X)) :=
…
  8. instance OAI.InvariantIsing.disorderReplicaLaw_probability line 80
  9. def OAI.InvariantIsing.spectralArrayLaw line 87
  10. theorem OAI.InvariantIsing.spectralArrayLaw_integral line 96