LabeledColorHistory.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.PrescribedTree.anchorAt_one line 13

def OAI.DilutedSpinGlass.PrescribedTree.labeledHistory line 24

Source documentation

The signed ordered history sum, retaining every actual old position and new branch. The terminal observable may inspect all assigned color positions. This is only an explicit finite expansion, not an assumed identity.

noncomputable def labeledHistory {n : ℕ} {C ι : Type} [DecidableEq C] [DecidableEq ι]
    (m : Fin (n+1) → ℝ)
    (V : (S : PrescribedTree n) → (C → S.Leaf) → (Sample Ω S → ℝ) → ℝ) :
    List C → (S : PrescribedTree n) → Finset ι → (ι → S.Leaf) →
      (C → S.Leaf) → (Sample Ω S → ℝ) → ℝ
  | [], S, _, _, pos, f => V S pos f
  | c::cs, S, U, loc, pos, f =>
      (∑ i ∈ U, labeledHistory m V cs S (U.erase i) loc
        (Function.update pos c (loc i)) f) +
      ∑ v : Internal S, gamma S m v * labeledHistory m V cs (grow S v) U
        (fun i => oldLeaf S v (loc i))
        (Function.update (fun c => oldLeaf S v (pos c)) c (newLeaf S v))
…

Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.gamma, OAI.DilutedSpinGlass.PrescribedTree.grow, OAI.DilutedSpinGlass.PrescribedTree.oldLeaf, OAI.DilutedSpinGlass.PrescribedTree.newLeaf

theorem OAI.DilutedSpinGlass.PrescribedTree.coloredAt_labeledHistory line 40

Source documentation

The genuine mixed derivative has precisely the signed labeled-history expansion. No factorial, unsigned normalization, or law is substituted.

theorem coloredAt_labeledHistory {n : ℕ} {C ι : Type} [Fintype C]
    [DecidableEq C] [DecidableEq ι] (T : KernelTower Ω n)
    (m : Fin (n+1) → ℝ) (hm : ∀ j : Fin n, m j.succ ≠ 0)
    (D : C → FinitePath Ω n → ℝ) (cs : List C) (hcs : cs.Nodup)
    (P : Finset C) (hdis : ∀ c ∈ cs, c ∉ P) (hfull : P ∪ cs.toFinset = Finset.univ)
    (S : PrescribedTree n) (U : Finset ι) (loc : ι → S.Leaf)
    (pos : C → S.Leaf) (f : Sample Ω S → ℝ) :
    coloredAt T m (cs.map D) S U (fun i => S.pathAt (loc i))
      (fun x => f x * ∏ c ∈ P, D c (S.pathAt (pos c) x)) (fun _ => 1) =
    labeledHistory m (fun S pos f => (S.sampleLaw T).expect
      (fun x => f x * ∏ c, D c (S.pathAt (pos c) x))) cs S U loc pos f := by
…

Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.coloredAt, OAI.DilutedSpinGlass.PrescribedTree.labeledHistory

lemma OAI.DilutedSpinGlass.FiniteLaw.expect_pi_pair line 121

def OAI.DilutedSpinGlass.KernelTower.pairExpect line 138

Source documentation

Two kernel paths share exactly their first d coordinates; the definition also includes the diagonal endpoint d=n.

noncomputable def pairExpect : (n : ℕ) → KernelTower Ω n → ℕ →
    (FinitePath Ω n → FinitePath Ω n → ℝ) → ℝ
  | 0, _, _, f => f () ()
  | n+1, T, 0, f => (law (n+1) T).expect (fun x => (law (n+1) T).expect (f x))
  | n+1, T, d+1, f => T.1.expect (fun x => pairExpect n (T.2 x) d (fun y z => f (x,y) (x,z)))

Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.KernelTower.law

lemma OAI.DilutedSpinGlass.KernelTower.pairExpect_zero line 144
lemma OAI.DilutedSpinGlass.KernelTower.pairExpect_diagonal line 151
theorem OAI.DilutedSpinGlass.PrescribedTree.pair_marginal line 165
Source documentation
The complete TWO-path joint law is determined by geometric splitting, not by coincidences of configurations. Unused branches are marginalized.
```
theorem pair_marginal {n : ℕ} (S : PrescribedTree n) (T : KernelTower Ω n)
    (a b : S.Leaf) (f : FinitePath Ω n → FinitePath Ω n → ℝ) :
    (S.sampleLaw T).expect (fun x => f (S.pathAt a x) (S.pathAt b x)) =
      KernelTower.pairExpect n T (splitDepth S a b) f := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.KernelTower.pairExpect, OAI.DilutedSpinGlass.PrescribedTree.splitDepth
lemma OAI.DilutedSpinGlass.PrescribedTree.pair_marginal_eq line 209