OAI/Probability/DilutedSpin/TreeSampling.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.DilutedSpinGlass.PrescribedTree line 13

   Source documentation

   Prescribed trees include a vertex at every depth, including unary vertices. Every internal vertex has at least one child; every leaf has the given height.

   inductive PrescribedTree : ℕ → Type
     | leaf : PrescribedTree 0
     | node {n : ℕ} (k : ℕ+) (children : Fin k → PrescribedTree n) : PrescribedTree (n+1)
   
   namespace PrescribedTree

2. def OAI.DilutedSpinGlass.PrescribedTree.leaves line 19
3. def OAI.DilutedSpinGlass.PrescribedTree.freshTotal line 24

   Source documentation

   Sum of the fresh-extension coefficients gamma_beta.

   noncomputable def freshTotal (m : ℕ → ℝ) (d : ℕ) : {n : ℕ} → PrescribedTree n → ℝ
     | 0, .leaf => 0
     | _+1, .node k T => m d - (k : ℝ) * m (d+1) + ∑ i, freshTotal m (d+1) (T i)
   
   /-- Sum of their absolute values. -/

   Mentions: OAI.DilutedSpinGlass.PrescribedTree

4. def OAI.DilutedSpinGlass.PrescribedTree.freshAbsolute line 29

   Source documentation

   Sum of their absolute values.

   noncomputable def freshAbsolute (m : ℕ → ℝ) (d : ℕ) : {n : ℕ} → PrescribedTree n → ℝ
     | 0, .leaf => 0
     | _+1, .node k T => |m d - (k : ℝ) * m (d+1)| +
         ∑ i, freshAbsolute m (d+1) (T i)
   
   /-- The exact telescoping normalization before specializing m_L=1. -/

   Mentions: OAI.DilutedSpinGlass.PrescribedTree

5. theorem OAI.DilutedSpinGlass.PrescribedTree.fresh_total line 35

   Source documentation

   The exact telescoping normalization before specializing m_L=1.

   theorem fresh_total {n : ℕ} (T : PrescribedTree n) (m : ℕ → ℝ) (d : ℕ) :
       freshTotal m d T = m d - leaves T * m (d+n) := by
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.freshTotal, OAI.DilutedSpinGlass.PrescribedTree.leaves

6. theorem OAI.DilutedSpinGlass.PrescribedTree.fresh_absolute_eq_neg line 47
7. theorem OAI.DilutedSpinGlass.PrescribedTree.fresh_absolute_root line 62

   Source documentation

   tree:telescoping. At root depth zero the absolute fresh-choice budget is exactly the number of old leaves, uniformly over the number of levels.

   theorem fresh_absolute_root {n : ℕ} (T : PrescribedTree n) (m : ℕ → ℝ)
       (hm : Monotone m) (hpos : ∀ d, 0 ≤ m d) (hzero : m 0 = 0) (hend : m n = 1) :
       freshAbsolute m 0 T = leaves T := by
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.freshAbsolute, OAI.DilutedSpinGlass.PrescribedTree.leaves

8. theorem OAI.DilutedSpinGlass.PrescribedTree.unused_subtree_total line 71

   Source documentation

   The sum of old-leaf and fresh choices in a reference-free subtree is m at its incoming depth. This is the nontrivial cancellation used to sum reference-constrained extensions, not their absolute values.

   theorem unused_subtree_total {n : ℕ} (T : PrescribedTree n) (m : ℕ → ℝ)
       (d : ℕ) (hend : m (d+n) = 1) :
       (leaves T : ℝ) + freshTotal m d T = m d := by
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.leaves, OAI.DilutedSpinGlass.PrescribedTree.freshTotal

9. theorem OAI.DilutedSpinGlass.PrescribedTree.reference_total line 79

   Source documentation

   The next color must avoid precisely the reference-containing children. All unused subtrees cancel to m_(d+1), giving the required local coefficient.

   theorem reference_total {n : ℕ} (k : ℕ+) (T : Fin k → PrescribedTree n)
       (m : ℕ → ℝ) (d : ℕ) (J : Finset (Fin k)) (hend : m (d+1+n) = 1) :
       m d - (k : ℝ) * m (d+1) +
         (∑ i ∈ Finset.univ \ J, ((leaves (T i) : ℝ) + freshTotal m (d+1) (T i))) =
           m d - (J.card : ℝ) * m (d+1) := by
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.leaves, OAI.DilutedSpinGlass.PrescribedTree.freshTotal

10. def OAI.DilutedSpinGlass.PrescribedTree.Sample line 98

    Source documentation

    Samples at separate sibling vertices are independent; repeated values are allowed. The full unary parts of each prescribed tree are retained.

    def Sample (Ω : Type) : {n : ℕ} → PrescribedTree n → Type
      | 0, .leaf => Unit
      | _+1, .node k C => (i : Fin k) → Ω × Sample Ω (C i)

    Mentions: OAI.DilutedSpinGlass.PrescribedTree

11. instance OAI.DilutedSpinGlass.PrescribedTree.sampleFintype line 102
12. def OAI.DilutedSpinGlass.PrescribedTree.sampleLaw line 111
13. def OAI.DilutedSpinGlass.PrescribedTree.vertexPotential line 119

    Source documentation

    The logarithm of the vertex product in tree:density. The first entry of m is the incoming edge exponent (zero at the root); the final entry equals one in the manuscript applications.

    noncomputable def vertexPotential : {n : ℕ} → (S : PrescribedTree n) →
        KernelTower Ω n → (Fin (n+1) → ℝ) → (FinitePath Ω n → ℝ) → Sample Ω S → ℝ
      | 0, .leaf, _, m, f, _ => m 0 * f ()
      | n+1, .node k C, T, m, f, x =>
          (m 0 - (k : ℝ) * m 1) * KernelTower.backwardLog (n+1) T (fun j => m j.succ) f +
          ∑ i, vertexPotential (C i) (T.2 (x i).1) (fun j => m j.succ)
            (fun y => f ((x i).1,y)) (x i).2
    
    /-- Exact joint law after insertion, expressed without division by the old
    weight. This handles zero-probability paths and every prescribed tree. -/

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.KernelTower.backwardLog

14. theorem OAI.DilutedSpinGlass.PrescribedTree.sampleLaw_tilt_weight line 129

    Source documentation

    Exact joint law after insertion, expressed without division by the old weight. This handles zero-probability paths and every prescribed tree.

    theorem sampleLaw_tilt_weight {n : ℕ} (S : PrescribedTree n)
        (T : KernelTower Ω n) (m : Fin (n+1) → ℝ)
        (hm : ∀ j : Fin n, m j.succ ≠ 0) (f : FinitePath Ω n → ℝ)
        (x : Sample Ω S) :
        (sampleLaw S (KernelTower.tilt n T (fun j => m j.succ) f)).weight x =
          (sampleLaw S T).weight x * Real.exp
            (vertexPotential S T m f x - m 0 * KernelTower.backwardLog n T (fun j => m j.succ) f) := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.sampleLaw, OAI.DilutedSpinGlass.KernelTower.tilt, OAI.DilutedSpinGlass.PrescribedTree.vertexPotential, OAI.DilutedSpinGlass.KernelTower.backwardLog

15. theorem OAI.DilutedSpinGlass.PrescribedTree.sampleLaw_tilt_density line 170

    Source documentation

    At the tree root there is no incoming edge. This is the self-contained, finite-kernel version of tree:density, with exactly its vertex exponents.

    theorem sampleLaw_tilt_density {n : ℕ} (S : PrescribedTree n)
        (T : KernelTower Ω n) (m : Fin (n+1) → ℝ)
        (hm : ∀ j : Fin n, m j.succ ≠ 0) (hroot : m 0 = 0)
        (f : FinitePath Ω n → ℝ) (x : Sample Ω S) :
        (sampleLaw S (KernelTower.tilt n T (fun j => m j.succ) f)).weight x =
          (sampleLaw S T).weight x * Real.exp (vertexPotential S T m f x) := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.sampleLaw, OAI.DilutedSpinGlass.KernelTower.tilt, OAI.DilutedSpinGlass.PrescribedTree.vertexPotential

16. def OAI.DilutedSpinGlass.PrescribedTree.vertexScore line 180

    Source documentation

    First variation of the vertex product: one score for every uncontracted leaf, and gamma_beta times the score of a fresh path at every internal vertex.

    noncomputable def vertexScore : {n : ℕ} → (S : PrescribedTree n) →
        KernelTower Ω n → (Fin (n+1) → ℝ) → (FinitePath Ω n → ℝ) →
          (FinitePath Ω n → ℝ) → Sample Ω S → ℝ
      | 0, .leaf, _, m, _, f', _ => m 0 * f' ()
      | n+1, .node k C, T, m, f, f', x =>
          (m 0 - (k : ℝ) * m 1) *
            (KernelTower.law (n+1) (KernelTower.tilt (n+1) T (fun j => m j.succ) f)).expect f' +
            ∑ i, vertexScore (C i) (T.2 (x i).1) (fun j => m j.succ)
              (fun y => f ((x i).1,y)) (fun y => f' ((x i).1,y)) (x i).2
    
    /-- Differentiate the entire prescribed tree density, without assuming all
    sampled prefixes are distinct or all original kernel weights positive. -/

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.KernelTower.law, OAI.DilutedSpinGlass.KernelTower.tilt

17. theorem OAI.DilutedSpinGlass.PrescribedTree.hasDerivAt_vertexPotential line 192

    Source documentation

    Differentiate the entire prescribed tree density, without assuming all sampled prefixes are distinct or all original kernel weights positive.

    theorem hasDerivAt_vertexPotential {n : ℕ} (S : PrescribedTree n)
        (T : KernelTower Ω n) (m : Fin (n+1) → ℝ)
        (hm : ∀ j : Fin n, m j.succ ≠ 0)
        {f : ℝ → FinitePath Ω n → ℝ} {f' : FinitePath Ω n → ℝ} {u : ℝ}
        (hf : ∀ y, HasDerivAt (fun t => f t y) (f' y) u) (x : Sample Ω S) :
        HasDerivAt (fun t => vertexPotential S T m (f t) x)
          (vertexScore S T m (f u) f' x) u := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.vertexPotential, OAI.DilutedSpinGlass.PrescribedTree.vertexScore

18. theorem OAI.DilutedSpinGlass.PrescribedTree.sampleLaw_tilt_expect line 216

    Source documentation

    Joint-law density in expectation form; physical root remains fixed.

    theorem sampleLaw_tilt_expect {n : ℕ} (S : PrescribedTree n)
        (T : KernelTower Ω n) (m : Fin (n+1) → ℝ)
        (hm : ∀ j : Fin n, m j.succ ≠ 0) (hroot : m 0 = 0)
        (f : FinitePath Ω n → ℝ) (G : Sample Ω S → ℝ) :
        (sampleLaw S (KernelTower.tilt n T (fun j => m j.succ) f)).expect G =
          (sampleLaw S T).expect (fun x => G x * Real.exp (vertexPotential S T m f x)) := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.sampleLaw, OAI.DilutedSpinGlass.KernelTower.tilt, OAI.DilutedSpinGlass.PrescribedTree.vertexPotential

19. theorem OAI.DilutedSpinGlass.PrescribedTree.hasDerivAt_sampleLaw_tilt_expect line 230

    Source documentation

    Tree differentiation rule, including a parameter-dependent test. Choosing G as a product of canceled replica factors yields the protected-leaf rule.

    theorem hasDerivAt_sampleLaw_tilt_expect {n : ℕ} (S : PrescribedTree n)
        (T : KernelTower Ω n) (m : Fin (n+1) → ℝ)
        (hm : ∀ j : Fin n, m j.succ ≠ 0) (hroot : m 0 = 0)
        {f : ℝ → FinitePath Ω n → ℝ} {f' : FinitePath Ω n → ℝ}
        {G : ℝ → Sample Ω S → ℝ} {G' : Sample Ω S → ℝ} {u : ℝ}
        (hf : ∀ y, HasDerivAt (fun t => f t y) (f' y) u)
        (hG : ∀ x, HasDerivAt (fun t => G t x) (G' x) u) :
        HasDerivAt (fun t => (sampleLaw S (KernelTower.tilt n T (fun j => m j.succ) (f t))).expect (G t))
          ((sampleLaw S (KernelTower.tilt n T (fun j => m j.succ) (f u))).expect
            (fun x => G' x + G u x * vertexScore S T m (f u) f' x)) u := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.sampleLaw, OAI.DilutedSpinGlass.KernelTower.tilt, OAI.DilutedSpinGlass.PrescribedTree.vertexScore

20. def OAI.DilutedSpinGlass.PrescribedTree.Leaf line 249

    Source documentation

    A leaf label is a vertex, not its sampled spin value.

    def Leaf : {n : ℕ} → PrescribedTree n → Type
      | 0, .leaf => Unit
      | _+1, .node k C => (i : Fin k) × Leaf (C i)

    Mentions: OAI.DilutedSpinGlass.PrescribedTree

21. instance OAI.DilutedSpinGlass.PrescribedTree.leafFintype line 253
22. def OAI.DilutedSpinGlass.PrescribedTree.pathAt line 260

    Source documentation

    Recover a whole path from a labeled leaf in a sampled tree.

    def pathAt : {n : ℕ} → (S : PrescribedTree n) → Leaf S → Sample Ω S → FinitePath Ω n
      | 0, .leaf, _, _ => ()
      | _+1, .node _ C, a, x => ((x a.1).1, pathAt (C a.1) a.2 (x a.1).2)
    
    /-- Exactly the denominator cancellation at the selected protected leaves,
    written in logarithmic form. -/

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.leaves

23. def OAI.DilutedSpinGlass.PrescribedTree.protectedLog line 266

    Source documentation

    Exactly the denominator cancellation at the selected protected leaves, written in logarithmic form.

    noncomputable def protectedLog {n : ℕ} (S : PrescribedTree n) (C : Finset (Leaf S))
        (f : FinitePath Ω n → ℝ) (x : Sample Ω S) : ℝ :=
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample

24. theorem OAI.DilutedSpinGlass.PrescribedTree.hasDerivAt_protectedLog line 271
25. theorem OAI.DilutedSpinGlass.PrescribedTree.hasDerivAt_protected_expect line 284
26. theorem OAI.DilutedSpinGlass.PrescribedTree.hasDerivAt_log_affine line 306

    Source documentation

    For positive affine insertions, the logarithmic score is D/A, with the actual (not a formal or assumed) analytic derivative.

    theorem hasDerivAt_log_affine {D u : ℝ} (hu : 1 + u*D ≠ 0) :
        HasDerivAt (fun t : ℝ => Real.log (1+t*D)) (D/(1+u*D)) u := by
    …

27. def OAI.DilutedSpinGlass.PrescribedTree.Internal line 315

    Source documentation

    Internal vertices refer to labeled genealogy, not coincident sampled values.

    def Internal : {n : ℕ} → PrescribedTree n → Type
      | 0, .leaf => Empty
      | _+1, .node _ C => Option ((i : _) × Internal (C i))

    Mentions: OAI.DilutedSpinGlass.PrescribedTree

28. instance OAI.DilutedSpinGlass.PrescribedTree.internalFintype line 319
29. def OAI.DilutedSpinGlass.PrescribedTree.gamma line 326

    Source documentation

    The signed coefficient at the exact uncontracted divergence vertex.

    noncomputable def gamma : {n : ℕ} → (S : PrescribedTree n) →
        (Fin (n+1) → ℝ) → Internal S → ℝ
      | 0, .leaf, _, v => nomatch v
      | _+1, .node k C, m, v =>
          match (v : Option ((i : Fin k) × Internal (C i))) with
          | none => m 0 - (k : ℝ) * m 1
          | some ⟨i,v⟩ => gamma (C i) (fun j => m j.succ) v
    
    variable {Ω : Type} [Fintype Ω]
    
    /-- Conditional expectation on a completely new path below the chosen vertex.
    Old sampled descendants are NOT reused, even if their values happen to agree. -/

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Internal

30. def OAI.DilutedSpinGlass.PrescribedTree.freshEval line 338

    Source documentation

    Conditional expectation on a completely new path below the chosen vertex. Old sampled descendants are NOT reused, even if their values happen to agree.

    noncomputable def freshEval : {n : ℕ} → (S : PrescribedTree n) →
        KernelTower Ω n → Internal S → (FinitePath Ω n → ℝ) → Sample Ω S → ℝ
      | 0, .leaf, _, v, _, _ => nomatch v
      | n+1, .node k C, T, v, D, x =>
          match (v : Option ((i : Fin k) × Internal (C i))) with
          | none => (KernelTower.law (n+1) T).expect D
          | some ⟨i,v⟩ => freshEval (C i) (T.2 (x i).1) v (fun y => D ((x i).1,y)) (x i).2
    
    /-- Resolves the differentiated density into terminal contributions and actual
    fresh conditional path expectations. No diagonal identification is made. -/

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.KernelTower.law

31. theorem OAI.DilutedSpinGlass.PrescribedTree.vertexScore_decomposition line 348

    Source documentation

    Resolves the differentiated density into terminal contributions and actual fresh conditional path expectations. No diagonal identification is made.

    theorem vertexScore_decomposition {n : ℕ} (S : PrescribedTree n)
        (T : KernelTower Ω n) (m : Fin (n+1) → ℝ)
        (f D : FinitePath Ω n → ℝ) (x : Sample Ω S) :
        vertexScore S T m f D x =
          m (Fin.last n) * (∑ a : Leaf S, D (pathAt S a x)) +
          ∑ v : Internal S, gamma S m v *
            freshEval S (KernelTower.tilt n T (fun j => m j.succ) f) v D x := by
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.vertexScore, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.pathAt, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.gamma, OAI.DilutedSpinGlass.PrescribedTree.freshEval, OAI.DilutedSpinGlass.KernelTower.tilt

32. theorem OAI.DilutedSpinGlass.PrescribedTree.protected_leaf_extension_rule line 385

    Source documentation

    Exact finite-kernel form of the protected-leaf differentiation rule. The second line is the expectation on a fresh extended path, conditional on its shared prefix. The canceled leaves are removed, not merely bounded.

    theorem protected_leaf_extension_rule {n : ℕ} (S : PrescribedTree n)
        (T : KernelTower Ω n) (m : Fin (n+1) → ℝ)
        (hm : ∀ j : Fin n, m j.succ ≠ 0) (hroot : m 0 = 0) (hend : m (Fin.last n) = 1)
        [DecidableEq (Leaf S)] (C : Finset (Leaf S)) (G : Sample Ω S → ℝ)
        {f : ℝ → FinitePath Ω n → ℝ} {D : FinitePath Ω n → ℝ} {u : ℝ}
        (hf : ∀ y, HasDerivAt (fun t => f t y) (D y) u) :
        HasDerivAt (fun t => (sampleLaw S (KernelTower.tilt n T (fun j => m j.succ) (f t))).expect
          (fun x => G x * Real.exp (-protectedLog S C (f t) x)))
          ((sampleLaw S (KernelTower.tilt n T (fun j => m j.succ) (f u))).expect
            (fun x => (G x * Real.exp (-protectedLog S C (f u) x)) *
              ((∑ a ∈ Finset.univ \ C, D (pathAt S a x)) +
                ∑ v : Internal S, gamma S m v *
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.sampleLaw, OAI.DilutedSpinGlass.KernelTower.tilt, OAI.DilutedSpinGlass.PrescribedTree.protectedLog, OAI.DilutedSpinGlass.PrescribedTree.pathAt, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.gamma

33. def OAI.DilutedSpinGlass.PrescribedTree.single line 414
34. def OAI.DilutedSpinGlass.PrescribedTree.grow line 420

    Source documentation

    Attach a genuinely new child at the divergence vertex; keep every old child and every unary level. Child 0 is the new child for root attachment.

    def grow : {n : ℕ} → (S : PrescribedTree n) → Internal S → PrescribedTree n
      | 0, .leaf, v => nomatch v
      | n+1, .node k C, v =>
        match (v : Option ((i : Fin k) × Internal (C i))) with
        | none => .node (k+1) (Fin.cases (single n) C)
        | some ⟨i,v⟩ => .node k (Function.update C i (grow (C i) v))
    
    variable {Ω : Type}

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.single

35. def OAI.DilutedSpinGlass.PrescribedTree.singlePath line 429
36. def OAI.DilutedSpinGlass.PrescribedTree.oldSample line 434

    Source documentation

    The projection forgets the new branch but preserves every old value.

    def oldSample : {n : ℕ} → (S : PrescribedTree n) → (v : Internal S) →
        Sample Ω (grow S v) → Sample Ω S
      | 0, .leaf, v => nomatch v
      | n+1, .node k C, v => by
        change Option ((i : Fin k) × Internal (C i)) at v
        cases v with
        | none =>
          intro x i
          exact x i.succ
        | some v =>
          obtain ⟨i,v⟩ := v
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.grow

37. def OAI.DilutedSpinGlass.PrescribedTree.newPath line 456

    Source documentation

    The new path shares just its prescribed prefix, even for repeated values.

    def newPath : {n : ℕ} → (S : PrescribedTree n) → (v : Internal S) →
        Sample Ω (grow S v) → FinitePath Ω n
      | 0, .leaf, v => nomatch v
      | n+1, .node k C, v => by
        change Option ((i : Fin k) × Internal (C i)) at v
        cases v with
        | none =>
          intro x
          exact ((x 0).1, singlePath n (x 0).2)
        | some v =>
          obtain ⟨i,v⟩ := v
    …

    Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.grow, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.singlePath