RetainedHistory.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.PrescribedTree.referenceHistoryExpectation line 15
Source documentation
The actual signed history sum with a retained test. Each fresh branch carries its probability kernels, and every further extension transports ALL retained variables with oldSample. Old-leaf choices introduce no new variable.
```
noncomputable def referenceHistoryExpectation {n : ℕ} (T : PrescribedTree n)
    (m : Fin (n+1) → ℝ) (K : KernelTower Ω n) :
    {p : ℕ} → {s : Fin (p+1) → Leaf T} → ReferencePlan T s →
      (S : PrescribedTree n) → (Fin (p+1) → Leaf S) → (Sample Ω S → ℝ) → ℝ
  | _, _, .nil, S, _, H => (sampleLaw S K).expect H
  | _, s, .cons b _ _ _ next, S, r, H =>
      (∑ x : Leaf S, if labeledOldMatch S T r s b x then
        referenceHistoryExpectation T m K next S (Fin.cons x r) H else 0) +
      (∑ v : Internal S, if labeledFreshMatch S T r s b v then
        gamma S m v * referenceHistoryExpectation T m K next (grow S v)
          (Fin.cons (newLeaf S v) (oldLeaf S v ∘ r))
          (fun x => H (oldSample S v x)) else 0)
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.ReferencePlan, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.sampleLaw, OAI.DilutedSpinGlass.PrescribedTree.labeledOldMatch, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.labeledFreshMatch, OAI.DilutedSpinGlass.PrescribedTree.gamma, OAI.DilutedSpinGlass.PrescribedTree.grow, OAI.DilutedSpinGlass.PrescribedTree.newLeaf, OAI.DilutedSpinGlass.PrescribedTree.oldLeaf, OAI.DilutedSpinGlass.PrescribedTree.oldSample
theorem OAI.DilutedSpinGlass.PrescribedTree.reference_history_expectation line 30
Source documentation
Complete joint-marginal normalization for any retained old test (not just constant tests). The history is combinatorial, never a condition on values.
```
theorem reference_history_expectation {n p : ℕ} (T : PrescribedTree n)
    (m : Fin (n+1) → ℝ) (hend : m (Fin.last n) = 1) (K : KernelTower Ω n)
    {s : Fin (p+1) → Leaf T} (P : ReferencePlan T s) (S : PrescribedTree n)
    (r : Fin (p+1) → Leaf S)
    (hsplit : ∀ i j, splitDepth S (r i) (r j) = splitDepth T (s i) (s j))
    (H : Sample Ω S → ℝ) :
    referenceHistoryExpectation T m K P S r H =
      referencePlanNormalizer T m P * (sampleLaw S K).expect H := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.ReferencePlan, OAI.DilutedSpinGlass.PrescribedTree.splitDepth, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.referenceHistoryExpectation, OAI.DilutedSpinGlass.PrescribedTree.referencePlanNormalizer, OAI.DilutedSpinGlass.PrescribedTree.sampleLaw
def OAI.DilutedSpinGlass.PrescribedTree.firstReferenceExpectation line 67
Source documentation
The first new path is retained along with every old path; all later paths are sampled and summed exactly as in the reference-history expansion.
```
noncomputable def firstReferenceExpectation {n p : ℕ} (T : PrescribedTree n)
    (m : Fin (n+1) → ℝ) (K : KernelTower Ω n) {s : Fin (p+1) → Leaf T}
    (b : Leaf T) (next : ReferencePlan T (Fin.cons b s))
    (S : PrescribedTree n) (r : Fin (p+1) → Leaf S)
    (H : Sample Ω S → FinitePath Ω n → ℝ) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.ReferencePlan, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.FinitePath
theorem OAI.DilutedSpinGlass.PrescribedTree.first_reference_expectation line 82
Source documentation
The genuine old-test/first-path marginal factors from every later signed reference sum. In particular this applies to any first-path prefix observable.
```
theorem first_reference_expectation {n p : ℕ} (T : PrescribedTree n)
    (m : Fin (n+1) → ℝ) (hend : m (Fin.last n) = 1) (K : KernelTower Ω n)
    {s : Fin (p+1) → Leaf T} (b : Leaf T) (next : ReferencePlan T (Fin.cons b s))
    (S : PrescribedTree n) (r : Fin (p+1) → Leaf S)
    (hsplit : ∀ i j, splitDepth S (r i) (r j) = splitDepth T (s i) (s j))
    (H : Sample Ω S → FinitePath Ω n → ℝ) :
    firstReferenceExpectation T m K b next S r H =
      referencePlanNormalizer T m next *
        ((∑ a : Leaf S, if labeledOldMatch S T r s b a then
          (sampleLaw S K).expect (fun x => H x (pathAt S a x)) else 0) +
        (∑ v : Internal S, if labeledFreshMatch S T r s b v then
          gamma S m v * (sampleLaw (grow S v) K).expect
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.ReferencePlan, OAI.DilutedSpinGlass.PrescribedTree.splitDepth, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.firstReferenceExpectation, OAI.DilutedSpinGlass.PrescribedTree.referencePlanNormalizer, OAI.DilutedSpinGlass.PrescribedTree.labeledOldMatch, OAI.DilutedSpinGlass.PrescribedTree.sampleLaw, OAI.DilutedSpinGlass.PrescribedTree.pathAt, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.labeledFreshMatch, OAI.DilutedSpinGlass.PrescribedTree.gamma, OAI.DilutedSpinGlass.PrescribedTree.grow