OAI/Probability/DilutedSpin/FiniteLaw.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.DilutedSpinGlass.FiniteLaw line 12

   Source documentation

   A finite conditional path law. Used only for the finite-kernel proof steps.

   structure FiniteLaw (Ω : Type*) [Fintype Ω] where
   …

2. def OAI.DilutedSpinGlass.FiniteLaw.expect line 21
3. theorem OAI.DilutedSpinGlass.FiniteLaw.expect_const line 23
4. theorem OAI.DilutedSpinGlass.FiniteLaw.expect_add line 26
5. theorem OAI.DilutedSpinGlass.FiniteLaw.expect_sub line 30
6. theorem OAI.DilutedSpinGlass.FiniteLaw.expect_mul_left line 34
7. theorem OAI.DilutedSpinGlass.FiniteLaw.expect_mul_right line 38
8. theorem OAI.DilutedSpinGlass.FiniteLaw.expect_div line 42
9. theorem OAI.DilutedSpinGlass.FiniteLaw.expect_neg line 46
10. theorem OAI.DilutedSpinGlass.FiniteLaw.expect_sum line 50
11. theorem OAI.DilutedSpinGlass.FiniteLaw.expect_finset_sum line 56

    Source comment

    Finset.sum one-binder version, deliberately avoiding simp's double-binder notation.

    theorem expect_finset_sum {ι : Type*} (s : Finset ι) (f : ι → Ω → ℝ) :
        P.expect (fun x => ∑ i ∈ s, f i x) = ∑ i ∈ s, P.expect (f i) :=
    …

12. theorem OAI.DilutedSpinGlass.FiniteLaw.expect_fintype_sum line 60
13. theorem OAI.DilutedSpinGlass.FiniteLaw.expect_congr line 65
14. theorem OAI.DilutedSpinGlass.FiniteLaw.expect_nonneg line 68
15. theorem OAI.DilutedSpinGlass.FiniteLaw.expect_mono line 71
16. def OAI.DilutedSpinGlass.FiniteLaw.covariance line 74
17. theorem OAI.DilutedSpinGlass.FiniteLaw.covariance_centered line 77
18. theorem OAI.DilutedSpinGlass.FiniteLaw.difference_product line 86

    Source documentation

    Two independent centered copies have second moment twice the covariance.

    theorem difference_product (f g : Ω → ℝ) :
        P.expect (fun y => P.expect (fun z => (f y - f z) * (g y - g z))) =
          2 * P.covariance f g := by
    …

19. def OAI.DilutedSpinGlass.FiniteLaw.dot line 98

    Source documentation

    The normalized site contraction used in sections/decorrelation.tex.

    noncomputable def dot {n : ℕ} (x y : Fin n → ℝ) : ℝ :=
    …

20. theorem OAI.DilutedSpinGlass.FiniteLaw.dot_sub_right line 103
21. theorem OAI.DilutedSpinGlass.FiniteLaw.dot_sq line 107
22. theorem OAI.DilutedSpinGlass.FiniteLaw.three_copy_identity line 120

    Source documentation

    Exact finite-conditional-law three-copy identity, with a square remainder. No boundedness assumption is needed for this algebraic ingredient.

    theorem three_copy_identity (X : Ω → Fin n → ℝ) :
        P.expect (fun x => P.expect (fun y => P.expect (fun z =>
          (dot (X x) (X y) - dot (X x) (X z))^2))) =
        (2 / (n : ℝ)^2) *
          ((∑ i, ∑ j, P.covariance (fun x => X x i) (fun x => X x j)^2) +
            P.expect (fun x => (∑ i, P.expect (fun y => X y i) *
              (X x i - P.expect (fun y => X y i)))^2)) := by
    …

    Mentions: OAI.DilutedSpinGlass.FiniteLaw.dot

23. theorem OAI.DilutedSpinGlass.FiniteLaw.three_copy_bound line 174

    Source documentation

    decor:three-copy-bound for each finite conditional path law.

    theorem three_copy_bound (X : Ω → Fin n → ℝ) :
        (2 / (n : ℝ)^2) *
          (∑ i, ∑ j, P.covariance (fun x => X x i) (fun x => X x j)^2) ≤
        P.expect (fun x => P.expect (fun y => P.expect (fun z =>
          (dot (X x) (X y) - dot (X x) (X z))^2))) := by
    …

    Mentions: OAI.DilutedSpinGlass.FiniteLaw.dot

24. def OAI.DilutedSpinGlass.FiniteLaw.covarianceEnergy line 185

    Source documentation

    Squared conditional covariance density.

    noncomputable def covarianceEnergy (X : Ω → Fin n → ℝ) : ℝ :=
    …

25. theorem OAI.DilutedSpinGlass.FiniteLaw.normalized_abs_sum_le line 189

    Source documentation

    Matrix Cauchy-Schwarz with exactly the manuscript's normalization.

    theorem normalized_abs_sum_le (C : Fin n → Fin n → ℝ) :
        (∑ i, ∑ j, |C i j|) / (n : ℝ)^2 ≤
          Real.sqrt ((∑ i, ∑ j, C i j ^ 2) / (n : ℝ)^2) := by
    …

26. theorem OAI.DilutedSpinGlass.FiniteLaw.centered_contraction_identity line 206

    Source documentation

    The exact second moment if the other vector is held fixed.

    theorem centered_contraction_identity (X : Ω → Fin n → ℝ) (b : Fin n → ℝ) :
        P.expect (fun x => (dot (fun i => X x i - P.expect (fun y => X y i)) b)^2) =
          (∑ i, ∑ j, P.covariance (fun x => X x i) (fun x => X x j) * (b i * b j)) /
            (n : ℝ)^2 := by
    …

    Mentions: OAI.DilutedSpinGlass.FiniteLaw.dot

27. theorem OAI.DilutedSpinGlass.FiniteLaw.centered_contraction_bound line 219

    Source documentation

    decor:contraction-bound, before the last square root, for a fixed multiplier.

    theorem centered_contraction_bound (X : Ω → Fin n → ℝ) (b : Fin n → ℝ)
        (hb : ∀ i, |b i| ≤ 1) :
        P.expect (fun x => (dot (fun i => X x i - P.expect (fun y => X y i)) b)^2) ≤
          Real.sqrt (P.covarianceEnergy X) := by
    …

    Mentions: OAI.DilutedSpinGlass.FiniteLaw.dot

28. theorem OAI.DilutedSpinGlass.FiniteLaw.independent_contraction_bound line 240

    Source documentation

    The other multiplier may itself be random, independently sampled under Q.

    theorem independent_contraction_bound {Λ : Type*} [Fintype Λ]
        (Q : FiniteLaw Λ) (X : Ω → Fin n → ℝ) (B : Λ → Fin n → ℝ)
        (hB : ∀ z i, |B z i| ≤ 1) :
        Q.expect (fun z => P.expect (fun x =>
          (dot (fun i => X x i - P.expect (fun y => X y i)) (B z))^2)) ≤
          Real.sqrt (P.covarianceEnergy X) := by
    …

    Mentions: OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FiniteLaw.dot

29. theorem OAI.DilutedSpinGlass.FiniteLaw.expect_sq_sub_expect line 252

    Source documentation

    Elementary Jensen for the square, proved from its nonnegative variance.

    theorem expect_sq_sub_expect (f : Ω → ℝ) :
        P.expect (fun x => (f x - P.expect f)^2) =
          P.expect (fun x => f x ^ 2) - P.expect f ^ 2 := by
    …

30. theorem OAI.DilutedSpinGlass.FiniteLaw.sq_expect_le_expect_sq line 260
31. theorem OAI.DilutedSpinGlass.FiniteLaw.expect_sqrt_le line 267

    Source documentation

    Jensen for the square root, including possible zero coordinates.

    theorem expect_sqrt_le (f : Ω → ℝ) (hf : ∀ x, 0 ≤ f x) :
        P.expect (fun x => Real.sqrt (f x)) ≤ Real.sqrt (P.expect f) := by
    …

32. theorem OAI.DilutedSpinGlass.FiniteLaw.conditional_contraction_bound line 276

    Source documentation

    Root/prefix averaged form of decor:contraction-bound. In the finite model conditional independence is expressed constructively by the independent laws P and Q at each prefix, not by an assumed covariance conclusion.

    theorem conditional_contraction_bound {Γ Λ : Type*} [Fintype Γ] [Fintype Λ]
        (R : FiniteLaw Γ) (P : Γ → FiniteLaw Ω) (Q : Γ → FiniteLaw Λ)
        (X : Γ → Ω → Fin n → ℝ) (B : Γ → Λ → Fin n → ℝ)
        (hB : ∀ γ z i, |B γ z i| ≤ 1) :
        Real.sqrt (R.expect (fun γ => (Q γ).expect (fun z => (P γ).expect (fun x =>
          (dot (fun i => X γ x i - (P γ).expect (fun y => X γ y i)) (B γ z))^2)))) ≤
          Real.sqrt (Real.sqrt (R.expect (fun γ => (P γ).covarianceEnergy (X γ)))) := by
    …

    Mentions: OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FiniteLaw.expect, OAI.DilutedSpinGlass.FiniteLaw.dot, OAI.DilutedSpinGlass.FiniteLaw.covarianceEnergy

33. theorem OAI.DilutedSpinGlass.FiniteLaw.conditional_three_copy_bound line 293

    Source documentation

    Prefix-averaged three-copy lower bound, the other half of decor:contractions.

    theorem conditional_three_copy_bound {Γ : Type*} [Fintype Γ]
        (R : FiniteLaw Γ) (P : Γ → FiniteLaw Ω) (X : Γ → Ω → Fin n → ℝ) :
        2 * R.expect (fun γ => (P γ).covarianceEnergy (X γ)) ≤
          R.expect (fun γ => (P γ).expect (fun x => (P γ).expect (fun y =>
            (P γ).expect (fun z => (dot (X γ x) (X γ y) - dot (X γ x) (X γ z))^2)))) := by
    …

    Mentions: OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FiniteLaw.covarianceEnergy, OAI.DilutedSpinGlass.FiniteLaw.expect, OAI.DilutedSpinGlass.FiniteLaw.dot

34. theorem OAI.DilutedSpinGlass.FiniteLaw.expect_mul_sq_le line 306

    Source documentation

    Finite-law Cauchy-Schwarz.

    theorem expect_mul_sq_le (f g : Ω → ℝ) :
        P.expect (fun x => f x * g x)^2 ≤
          P.expect (fun x => f x^2) * P.expect (fun x => g x^2) := by
    …

35. def OAI.DilutedSpinGlass.FiniteLaw.l2 line 319
36. theorem OAI.DilutedSpinGlass.FiniteLaw.l2_nonneg line 321
37. theorem OAI.DilutedSpinGlass.FiniteLaw.l2_sq line 323
38. theorem OAI.DilutedSpinGlass.FiniteLaw.l2_zero line 326
39. theorem OAI.DilutedSpinGlass.FiniteLaw.expect_mul_le_l2 line 328
40. theorem OAI.DilutedSpinGlass.FiniteLaw.l2_add_le line 338

    Source documentation

    Minkowski is used for successive projection of independent child shapes.

    theorem l2_add_le (f g : Ω → ℝ) :
        P.l2 (fun x => f x + g x) ≤ P.l2 f + P.l2 g := by
    …

41. theorem OAI.DilutedSpinGlass.FiniteLaw.l2_mono line 352
42. theorem OAI.DilutedSpinGlass.FiniteLaw.l2_mul_le line 358
43. def OAI.DilutedSpinGlass.FiniteLaw.bind line 366

    Source documentation

    A finite mixture, to represent the root and the independent kernels exactly.

    noncomputable def bind {Λ : Type*} [Fintype Λ] (Q : Ω → FiniteLaw Λ) : FiniteLaw (Ω × Λ) where
    …

    Mentions: OAI.DilutedSpinGlass.FiniteLaw

44. theorem OAI.DilutedSpinGlass.FiniteLaw.expect_bind line 372
45. theorem OAI.DilutedSpinGlass.FiniteLaw.l2_condition_le line 378

    Source documentation

    Conditional expectation contracts the L2 norm for a finite kernel.

    theorem l2_condition_le {Λ : Type*} [Fintype Λ] (Q : Ω → FiniteLaw Λ)
        (f : Ω × Λ → ℝ) :
        P.l2 (fun x => (Q x).expect (fun y => f (x, y))) ≤ (P.bind Q).l2 f := by
    …

    Mentions: OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FiniteLaw.expect, OAI.DilutedSpinGlass.FiniteLaw.l2

46. theorem OAI.DilutedSpinGlass.FiniteLaw.expect_pos line 388

    Source documentation

    Positive functions have positive finite expectation, without a full-support assumption on the kernel.

    theorem expect_pos {f : Ω → ℝ} (hf : ∀ x, 0 < f x) : 0 < P.expect f := by
    …

47. def OAI.DilutedSpinGlass.FiniteLaw.expMoment line 399
48. theorem OAI.DilutedSpinGlass.FiniteLaw.expMoment_pos line 402
49. def OAI.DilutedSpinGlass.FiniteLaw.tilt line 406

    Source documentation

    One tilted path kernel (trees.tex, original-tilt).

    noncomputable def tilt (m : ℝ) (f : Ω → ℝ) : FiniteLaw Ω where
    …

    Mentions: OAI.DilutedSpinGlass.FiniteLaw

50. def OAI.DilutedSpinGlass.FiniteLaw.logMean line 414
51. theorem OAI.DilutedSpinGlass.FiniteLaw.tilt_expect line 417
52. theorem OAI.DilutedSpinGlass.FiniteLaw.expMoment_add line 422
53. theorem OAI.DilutedSpinGlass.FiniteLaw.logMean_add line 426
54. theorem OAI.DilutedSpinGlass.FiniteLaw.logMean_mono line 433
55. theorem OAI.DilutedSpinGlass.FiniteLaw.logMean_stability line 440

    Source documentation

    Root-measurable uniform bounds pass unchanged through each power mean.

    theorem logMean_stability {m c : ℝ} (hm : 0 < m) {f g : Ω → ℝ}
        (h : ∀ x, |f x - g x| ≤ c) : |P.logMean m f - P.logMean m g| ≤ c := by
    …

56. theorem OAI.DilutedSpinGlass.FiniteLaw.logMean_insertion line 451

    Source documentation

    Exact insertion identity for a single finite backward step.

    theorem logMean_insertion {m : ℝ} (f a : Ω → ℝ) :
        P.logMean m (fun x => f x + a x) - P.logMean m f =
          (P.tilt m f).logMean m a := by
    …

    Mentions: OAI.DilutedSpinGlass.FiniteLaw.logMean

57. theorem OAI.DilutedSpinGlass.FiniteLaw.hasDerivAt_expect line 464

    Source documentation

    Differentiation commutes with a finite path kernel.

    theorem hasDerivAt_expect {f : ℝ → Ω → ℝ} {f' : Ω → ℝ} {u : ℝ}
        (h : ∀ x, HasDerivAt (fun t => f t x) (f' x) u) :
        HasDerivAt (fun t => P.expect (f t)) (P.expect f') u := by
    …

58. theorem OAI.DilutedSpinGlass.FiniteLaw.hasDerivAt_logMean line 476

    Source documentation

    First variation of a power-mean step: the derivative is the tilted score.

    theorem hasDerivAt_logMean {m : ℝ} (hm : m ≠ 0)
        {f : ℝ → Ω → ℝ} {f' : Ω → ℝ} {u : ℝ}
        (h : ∀ x, HasDerivAt (fun t => f t x) (f' x) u) :
        HasDerivAt (fun t => P.logMean m (f t)) ((P.tilt m (f u)).expect f') u := by
    …

    Mentions: OAI.DilutedSpinGlass.FiniteLaw.expect

59. theorem OAI.DilutedSpinGlass.FiniteLaw.hasDerivAt_tilt_expect line 497

    Source documentation

    Differentiating an observable under a finite exponentially tilted kernel.

    theorem hasDerivAt_tilt_expect {m : ℝ}
        {f g : ℝ → Ω → ℝ} {f' g' : Ω → ℝ} {u : ℝ}
        (hf : ∀ x, HasDerivAt (fun t => f t x) (f' x) u)
        (hg : ∀ x, HasDerivAt (fun t => g t x) (g' x) u) :
        HasDerivAt (fun t => (P.tilt m (f t)).expect (g t))
          ((P.tilt m (f u)).expect g' +
            m * (P.tilt m (f u)).covariance (g u) f') u := by
    …

    Mentions: OAI.DilutedSpinGlass.FiniteLaw.expect, OAI.DilutedSpinGlass.FiniteLaw.covariance

60. theorem OAI.DilutedSpinGlass.FiniteLaw.hasDerivAt_tilt_score line 529

    Source documentation

    The second variation identity used in bounded score concentration.

    theorem hasDerivAt_tilt_score {m : ℝ}
        {f f' : ℝ → Ω → ℝ} {f'' : Ω → ℝ} {u : ℝ}
        (hf : ∀ x, HasDerivAt (fun t => f t x) (f' u x) u)
        (hf' : ∀ x, HasDerivAt (fun t => f' t x) (f'' x) u) :
        HasDerivAt (fun t => (P.tilt m (f t)).expect (f' t))
          ((P.tilt m (f u)).expect f'' +
            m * (P.tilt m (f u)).covariance (f' u) (f' u)) u :=
    …

    Mentions: OAI.DilutedSpinGlass.FiniteLaw.expect, OAI.DilutedSpinGlass.FiniteLaw.covariance

61. theorem OAI.DilutedSpinGlass.FiniteLaw.variance_bind line 539

    Source documentation

    Total variance at one edge of a finite probability tree.

    theorem variance_bind {Λ : Type*} [Fintype Λ] (Q : Ω → FiniteLaw Λ)
        (f : Ω × Λ → ℝ) :
        (P.bind Q).covariance f f =
          P.expect (fun x => (Q x).covariance (fun y => f (x,y)) (fun y => f (x,y))) +
            P.covariance (fun x => (Q x).expect (fun y => f (x,y)))
              (fun x => (Q x).expect (fun y => f (x,y))) := by
    …

    Mentions: OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FiniteLaw.covariance, OAI.DilutedSpinGlass.FiniteLaw.expect

62. theorem OAI.DilutedSpinGlass.FiniteLaw.covariance_self_nonneg line 548
63. theorem OAI.DilutedSpinGlass.FiniteLaw.covariance_self_le_one line 553

    Source documentation

    A bounded spin product has total conditional variance at most one.

    theorem covariance_self_le_one {f : Ω → ℝ} (hf : ∀ x, |f x| ≤ 1) :
        P.covariance f f ≤ 1 := by
    …

64. theorem OAI.DilutedSpinGlass.FiniteLaw.weights_ext line 564
65. theorem OAI.DilutedSpinGlass.FiniteLaw.logMean_const line 570
66. theorem OAI.DilutedSpinGlass.FiniteLaw.tilt_weight line 576

    Source documentation

    The edge-density form of the normalized tilted finite kernel.

    theorem tilt_weight {m : ℝ} (hm : m ≠ 0) (f : Ω → ℝ) (x : Ω) :
        (P.tilt m f).weight x = P.weight x * Real.exp (m * (f x - P.logMean m f)) := by
    …

67. theorem OAI.DilutedSpinGlass.FiniteLaw.tilt_insertion line 585

    Source documentation

    Exact composition of two one-step insertions, with no support assumption.

    theorem tilt_insertion (m : ℝ) (f a : Ω → ℝ) :
        (P.tilt m f).tilt m a = P.tilt m (fun x => f x + a x) := by
    …

    Mentions: OAI.DilutedSpinGlass.FiniteLaw.tilt

68. def OAI.DilutedSpinGlass.FiniteLaw.pi line 601

    Source documentation

    Independent product of finitely many finite conditional laws.

    noncomputable def pi {ι : Type*} [Fintype ι] [DecidableEq ι] {α : ι → Type*} [∀ i, Fintype (α i)]
        (Q : (i : ι) → FiniteLaw (α i)) : FiniteLaw ((i : ι) → α i) where
    …

    Mentions: OAI.DilutedSpinGlass.FiniteLaw

69. theorem OAI.DilutedSpinGlass.FiniteLaw.expect_pi_product line 608

    Source documentation

    Finite independence identity, valid for arbitrary and distinct kernels.

    theorem expect_pi_product {ι : Type*} [Fintype ι] [DecidableEq ι] {α : ι → Type*} [∀ i, Fintype (α i)]
        (Q : (i : ι) → FiniteLaw (α i)) (f : (i : ι) → α i → ℝ) :
        (pi Q).expect (fun x => ∏ i, f i (x i)) = ∏ i, (Q i).expect (f i) := by
    …

    Mentions: OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FiniteLaw.pi, OAI.DilutedSpinGlass.FiniteLaw.expect

70. theorem OAI.DilutedSpinGlass.FiniteLaw.abs_expect_le line 613
71. theorem OAI.DilutedSpinGlass.FiniteLaw.continuousOn_expect line 622
72. theorem OAI.DilutedSpinGlass.FiniteLaw.continuousOn_logMean line 630
73. theorem OAI.DilutedSpinGlass.FiniteLaw.continuousOn_tilt_expect line 639
74. theorem OAI.DilutedSpinGlass.FiniteLaw.continuousOn_tilt_covariance line 650