SpectralQuantilePaths.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous pair quantile laws of the actual spectral GG limits.

def OAI.InvariantIsing.spectralLinearLaw line 16
instance OAI.InvariantIsing.spectralLinearLaw_probability line 19
lemma OAI.InvariantIsing.spectralLinearLaw_unit line 25
def OAI.InvariantIsing.spectralQuantilePath line 32
lemma OAI.InvariantIsing.spectralQuantilePath_law line 40

theorem OAI.InvariantIsing.spectralQuantilePath_pair_law line 48

Source documentation

All pairs of required nonnegative linear overlap combinations have simultaneous quantile laws. The total spin combination is included once its unit bound is derived from the genuine spectral partition.

theorem spectralQuantilePath_pair_law {m : ℕ} {Q : ProbabilityMeasure (SpectralArray m)}
    (hgg : HasEntryGhirlandaGuerra (fun x i j => x (i,j)) (Q : Measure (SpectralArray m)))
    (hG : ∀ᵐ x ∂(Q : Measure (SpectralArray m)), SpectralGram x)
    (q : Fin m → ℝ) (hq : ∀ a, 0 ≤ q a)
    (hd : ∀ᵐ x ∂(Q : Measure (SpectralArray m)), ∀ i a, (x (i,i) a : ℝ) = q a)
    (hE : ∀ e : Equiv.Perm ℕ,
      (Q : Measure (SpectralArray m)).map (permuteSpectralArray e) = Q)
    (w z : Fin m → ℝ) (hw : ∀ a, 0 ≤ w a) (hz : ∀ a, 0 ≤ z a)
    (hws : ∀ᵐ x ∂(Q : Measure (SpectralArray m)), spectralLinearArray w x 0 1 ∈ Icc (0 : ℝ) 1)
    (hzs : ∀ᵐ x ∂(Q : Measure (SpectralArray m)), spectralLinearArray z x 0 1 ∈ Icc (0 : ℝ) 1) :
    InvariantIsing.pathMeasure.map
      (fun s => (spectralQuantilePath Q w hws s, spectralQuantilePath Q z hzs s)) =
…

Mentions: OAI.InvariantIsing.SpectralArray, OAI.InvariantIsing.SpectralGram, OAI.InvariantIsing.permuteSpectralArray, OAI.InvariantIsing.spectralLinearArray, OAI.InvariantIsing.spectralQuantilePath

lemma OAI.InvariantIsing.integral_of_pair_law line 82