OAI/Probability/InvariantIsing/Pressure/RandomOrbitLaw.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The joint conditional-Haar hypothesis for random spectra and fields. Only the one-dimensional marginal orbit law is prescribed at each dimension.

  1. abbrev OAI.InvariantIsing.FieldSpectralData line 13

    Also declared: ComparatorChallenges/InvariantIsing.lean:217 (same declaration text).

  2. def OAI.InvariantIsing.dataPhysicalPressure line 15

    Also declared: ComparatorChallenges/InvariantIsing.lean:219 (same declaration text).

  3. lemma OAI.InvariantIsing.measurable_random_specialPressure line 18
  4. lemma OAI.InvariantIsing.measurable_dataPhysicalPressure line 33
  5. lemma OAI.InvariantIsing.measurable_dataPressureMean line 45
  6. def OAI.InvariantIsing.ConditionalFieldOrbitLaw line 52

    Source documentation

    Conditional jointly on the spectrum and field, the pressure has its Haar orbit law. This formulation allows arbitrary dependence across dimensions and between the two data sets.

    Distinct definitions of this name: ComparatorChallenges/InvariantIsing.lean:222 (same statement text; different proof or body). Qualify references as OAI.InvariantIsing.ConditionalFieldOrbitLaw@path.

    def ConditionalFieldOrbitLaw {Ω : Type*} [MeasurableSpace Ω] {N : ℕ}
    (P : Measure Ω) (d : Ω → FieldSpectralData N) (pressure : Ω → ℝ)
    (H : Measure (Orthogonal N)) : Prop :=
…

    Mentions: OAI.InvariantIsing.FieldSpectralData, OAI.InvariantIsing.pressure, OAI.InvariantIsing.Orthogonal