FirstSplitSchedule.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.ReducedTopology.realize_unary_of_later line 12
lemma OAI.DilutedSpinGlass.ReducedTopology.conditionalScheduledMean_rootProduct line 21
Source documentation
At the assigned first split, the whole scheduled mean is EXACTLY the product of its proper-child means, including the transition at that split.
```
lemma conditionalScheduledMean_rootProduct (H p : ℕ) (k : ℕ+) (hk : 2≤(k:ℕ))
    (C : Fin k → ReducedTopology) (q : (j : Fin k) → (C j).Vertex → ℕ)
    (hq : ∀ j v, p<q j v) (T : KernelTower Ω (H+1+p))
    (f : FinitePath Ω (H+1+p) → Fin N → ℝ) (x : FinitePath Ω (H+1+p)) (i : Fin N) :
    conditionalScheduledMean (H+1+p) 0 p (.node k hk C) (rootSchedule p q) T (fun y => f y i) x=
      conditionalScheduledProduct (H+1+p) 0 p C q T f x i := by
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.ReducedTopology.conditionalScheduledMean, OAI.DilutedSpinGlass.ReducedTopology.rootSchedule, OAI.DilutedSpinGlass.ReducedTopology.conditionalScheduledProduct
lemma OAI.DilutedSpinGlass.ReducedTopology.conditionalScheduledMean_eq_splitProjector line 37
Source documentation
Literal identification with the old/target projector in the matrix identity, at arbitrary initial evaluation prefix and later first split.
```
lemma conditionalScheduledMean_eq_splitProjector (H r d a : ℕ) (S : ReducedTopology)
    (q : S.Vertex → ℕ) (T : KernelTower Ω (H+r+1+d))
    (f : FinitePath Ω (H+r+1+d) → ℝ) (x : FinitePath Ω (H+r+1+d)) :
    conditionalScheduledMean (H+r+1+d) a (r+1+d) S q T f x=
      PrescribedTree.splitProjector (realize H (a+(r+1+d)) S q) r d T f x := by
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.ReducedTopology.conditionalScheduledMean, OAI.DilutedSpinGlass.PrescribedTree.splitProjector, OAI.DilutedSpinGlass.ReducedTopology.realize
theorem OAI.DilutedSpinGlass.ReducedTopology.scheduled_splitProjector_product line 53
Source documentation
The actual first-split projector in the matrix observable is precisely the scheduled conditional child product. This applies to the old or delayed target schedule separately, without altering any branching assignment.
```
theorem scheduled_splitProjector_product (H r d : ℕ) (k : ℕ+) (hk : 2≤(k:ℕ))
    (C : Fin k → ReducedTopology) (q : (j : Fin k) → (C j).Vertex → ℕ)
    (hq : ∀ j v, r+1+d<q j v) (T : KernelTower Ω (H+1+r+1+d))
    (f : FinitePath Ω (H+1+r+1+d) → Fin N → ℝ) :
    (fun x i => PrescribedTree.splitProjector
      (realize (H+1) (r+1+d) (.node k hk C) (rootSchedule (r+1+d) q)) r d T (fun y => f y i) x)=
      conditionalScheduledProduct (H+1+r+1+d) 0 (r+1+d) C q T f := by
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.splitProjector, OAI.DilutedSpinGlass.ReducedTopology.realize, OAI.DilutedSpinGlass.ReducedTopology.rootSchedule, OAI.DilutedSpinGlass.ReducedTopology.conditionalScheduledProduct