OAI/Probability/InvariantIsing/Arrays/UltrametricProduct.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InvariantIsing.replicaProductFirst line 14
2. def OAI.InvariantIsing.replicaProductSecond line 17
3. lemma OAI.InvariantIsing.ultrametric_product_decomposition line 20
4. lemma OAI.InvariantIsing.measurable_replicaProductFirst line 48
5. lemma OAI.InvariantIsing.measurable_replicaProductSecond line 54
6. lemma OAI.InvariantIsing.replicaProductFirst_abs_le line 60
7. lemma OAI.InvariantIsing.replicaProductSecond_abs_le line 66
8. theorem OAI.InvariantIsing.gg_ultrametric_product_integral line 79

   Source documentation

   The full synchronized triple product is reduced to its two-link GG marginals. Strict comparisons retain the diagonal contribution at atoms.

   theorem gg_ultrametric_product_integral {Ω : Type*} [MeasurableSpace Ω]
       (μ : Measure Ω) [IsProbabilityMeasure μ] (R : Ω → RealArray) (hR : Measurable R)
       (hgg : HasEntryGhirlandaGuerra R μ)
       (hs : ∀ᵐ x ∂μ, ∀ i j, R x i j = R x j i)
       (hu : ∀ᵐ x ∂μ, IsUltrametricArray (R x))
       (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) :
       2 * (∫ x, Φ (R x 0 1) * (a (R x 0 2) * b (R x 1 2)) ∂μ) =
         (∫ x, ∫ y, Φ x * replicaProductFirst a b x y ∂scalarOverlapLaw μ R ∂scalarOverlapLaw μ R) +
         (∫ x, ∫ y, Φ x * replicaProductSecond a b x y ∂scalarOverlapLaw μ R ∂scalarOverlapLaw μ R) +
         ∫ x, Φ x * (a x * b x) ∂scalarOverlapLaw μ R := by
   …

   Mentions: OAI.InvariantIsing.replicaProductFirst, OAI.InvariantIsing.scalarOverlapLaw, OAI.InvariantIsing.replicaProductSecond