TripleMarginal.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.PrescribedTree.labeledHistory_add line 16
lemma OAI.DilutedSpinGlass.PrescribedTree.labeledHistory_mul_left line 29
lemma OAI.DilutedSpinGlass.PrescribedTree.labeledHistory_zero line 45
lemma OAI.DilutedSpinGlass.PrescribedTree.labeledHistory_sum line 54

theorem OAI.DilutedSpinGlass.PrescribedTree.constrainedHistory_site_average line 67

Source documentation

Averaging the independent insertion site gives exactly the multioverlap inside each signed history, with no distinct-site restriction.

theorem constrainedHistory_site_average {k : ℕ} {R J : Type} [Fintype R] [DecidableEq R]
    [Fintype J] (weights : J → ℝ) (T : KernelTower Ω n) (m : Fin (n+1) → ℝ)
    (a b : R → Option (Fin k)) (d : R → Fin n)
    (spinColor : J → Option (Fin k) → FinitePath Ω n → ℝ)
    (S : PrescribedTree n) (anchor : S.Leaf) (f : Sample Ω S → ℝ) :
    (∑ i, weights i * constrainedHistory T m a b d (spinColor i) S anchor f) =
    labeledHistory m (fun S pos f =>
      (S.sampleLaw T).expect
        (fun x => f x * ∑ i, weights i * ∏ c, spinColor i c (S.pathAt (pos c) x)) *
      ∏ r, if (d r).val+1 ≤ splitDepth S (pos (a r)) (pos (b r)) then (1:ℝ) else 0)
      (List.ofFn (fun j : Fin k => (some j : Option (Fin k)))).reverse S
      (Finset.univ.erase anchor) id (fun _ => anchor) f := by
…

Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.constrainedHistory, OAI.DilutedSpinGlass.PrescribedTree.labeledHistory, OAI.DilutedSpinGlass.PrescribedTree.splitDepth

lemma OAI.DilutedSpinGlass.PrescribedTree.labeledHistory_sub line 106

theorem OAI.DilutedSpinGlass.PrescribedTree.projection_history_cost line 121

Source documentation

The genuine signed history of an L2 projection error has the exact small-L charging cost. The target error need only be small under its own single-copy law; it may be correlated with every old path and old test.

theorem projection_history_cost (hL : 0 < L) (Q : Finset ℕ)
    (T S : PrescribedTree L) (q : C → T.Leaf) (hq : Function.Surjective q)
    (hS : branchingCount S (· ∈ Q) = 0) (K : KernelTower Ω L)
    (D : (C → FinitePath Ω L) → ℝ) (cs : List C) (U : Finset ι)
    (loc : ι → S.Leaf) (pos : C → S.Leaf) (f : Sample Ω S → ℝ)
    (hf : ∀ x, |f x| ≤ 1) (hU : U.card ≤ leaves S) :
    |labeledHistory (grid L 0 L)
      (fun R pos g => if ∀ a b, splitDepth R (pos a) (pos b) = splitDepth T (q a) (q b)
        then (R.sampleLaw K).expect (fun x => g x*D (fun c => R.pathAt (pos c) x)) else 0)
      cs S U loc pos f| ≤
      (T.sampleLaw K).l2 (fun x => D (fun c => T.pathAt (q c) x)) *
        (chargeBound (2*(leaves S+cs.length:ℕ)) ((Q.card:ℝ)*(leaves S+cs.length:ℕ))
…

Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.PrescribedTree.branchingCount, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.leaves, OAI.DilutedSpinGlass.PrescribedTree.labeledHistory, OAI.DilutedSpinGlass.PrescribedTree.grid, OAI.DilutedSpinGlass.PrescribedTree.splitDepth, OAI.DilutedSpinGlass.PrescribedTree.chargeBound

theorem OAI.DilutedSpinGlass.PrescribedTree.projection_history_difference line 141

Source documentation

Direct comparison of an actual target overlap with its projected observable inside the full signed ordered extension sum.

theorem projection_history_difference (hL : 0 < L) (Q : Finset ℕ)
    (T S : PrescribedTree L) (q : C → T.Leaf) (hq : Function.Surjective q)
    (hS : branchingCount S (· ∈ Q) = 0) (K : KernelTower Ω L)
    (A B : (C → FinitePath Ω L) → ℝ) (cs : List C) (U : Finset ι)
    (loc : ι → S.Leaf) (pos : C → S.Leaf) (f : Sample Ω S → ℝ)
    (hf : ∀ x, |f x| ≤ 1) (hU : U.card ≤ leaves S) :
    |labeledHistory (grid L 0 L)
      (fun R pos g => if ∀ a b, splitDepth R (pos a) (pos b) = splitDepth T (q a) (q b)
        then (R.sampleLaw K).expect (fun x => g x*A (fun c => R.pathAt (pos c) x)) else 0)
      cs S U loc pos f -
     labeledHistory (grid L 0 L)
      (fun R pos g => if ∀ a b, splitDepth R (pos a) (pos b) = splitDepth T (q a) (q b)
…

lemma OAI.DilutedSpinGlass.FiniteLaw.expect_pi_three line 181
def OAI.DilutedSpinGlass.KernelTower.tripleExpectAt line 195
lemma OAI.DilutedSpinGlass.KernelTower.tripleExpectAt_eq line 203
lemma OAI.DilutedSpinGlass.PrescribedTree.branch_leaf_marginal line 213
theorem OAI.DilutedSpinGlass.PrescribedTree.triple_marginal line 223
Source documentation
Every uncontracted tree with three positional pairwise split depths equal to d has the genuine three-copy conditional marginal. All other branches are integrated out, irrespective of their number or depths.
```
theorem triple_marginal {n : ℕ} (S : PrescribedTree n) (T : KernelTower Ω n)
    (a b c : S.Leaf) (d : ℕ) (hd : d < n)
    (hab : splitDepth S a b = d) (hac : splitDepth S a c = d)
    (hbc : splitDepth S b c = d)
    (F : FinitePath Ω n → FinitePath Ω n → FinitePath Ω n → ℝ) :
    (S.sampleLaw T).expect (fun x => F (S.pathAt a x) (S.pathAt b x) (S.pathAt c x)) =
      KernelTower.tripleExpectAt n T d F := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree.splitDepth, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.KernelTower.tripleExpectAt