QuantileReplicaProduct.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The synchronized GG triple product equals the manuscript product path.

theorem OAI.InvariantIsing.gg_quantile_triple_product line 13

theorem OAI.InvariantIsing.gg_replicaProductPath_integral line 101

Source documentation

The off-diagonal replica product has exactly the path used in the rotation identities, including its contributions at overlap atoms.

theorem gg_replicaProductPath_integral {Ω : Type*} [MeasurableSpace Ω]
    (μ : Measure Ω) [IsProbabilityMeasure μ] (R : Ω → RealArray) (hR : Measurable R)
    (hgg : HasEntryGhirlandaGuerra R μ)
    (hsym : ∀ᵐ x ∂μ, ∀ i j, R x i j = R x j i)
    (hu : ∀ᵐ x ∂μ, IsUltrametricArray (R x))
    (p : OverlapPath) (hl : pathMeasure.map p = scalarOverlapLaw μ R)
    (a b Φ : ℝ → ℝ) (ha : Measurable a) (hb : Measurable b) (hΦ : Measurable Φ)
    {A B C : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (hC : 0 ≤ C)
    (haB : ∀ x, |a x| ≤ A) (hbB : ∀ x, |b x| ≤ B) (hΦB : ∀ x, |Φ x| ≤ C)
    (da db : ℝ) :
    (∫ x, Φ (R x 0 1) * (da * b (R x 0 1) + a (R x 0 1) * db -
      2 * (a (R x 0 2) * b (R x 1 2))) ∂μ) =
…

Mentions: OAI.InvariantIsing.OverlapPath, OAI.InvariantIsing.scalarOverlapLaw