MarkerHistoryTransport.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DilutedSpinGlass.PrescribedTree.labeledHistory_reindex line 15

Source documentation

Enlarging the color set by protected old paths does not change any extension choice or its coefficient.

theorem labeledHistory_reindex (m : Fin (n+1) → ℝ) (e : C → D) (he : Function.Injective e)
    (V : (R : PrescribedTree n) → (C → R.Leaf) → (Sample Ω R → ℝ) → ℝ)
    (cs : List C) (S : PrescribedTree n) (U : Finset ι) (loc : ι → S.Leaf)
    (pos : D → S.Leaf) (f : Sample Ω S → ℝ) :
    labeledHistory m (fun R pos g => V R (pos ∘ e) g) (cs.map e) S U loc pos f =
      labeledHistory m V cs S U loc (pos ∘ e) f := by
…

Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.labeledHistory

lemma OAI.DilutedSpinGlass.PrescribedTree.splitDepth_eq_of_lt line 29
Source documentation
In a splitting ultrametric, a path separating from a marker before every old path has the same split from each of those old paths.
```
lemma splitDepth_eq_of_lt (S : PrescribedTree n) (a b c : S.Leaf)
    (h : splitDepth S a b < splitDepth S b c) :
    splitDepth S a c = splitDepth S a b := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.splitDepth

theorem OAI.DilutedSpinGlass.PrescribedTree.marker_matrix_iff line 43

Source documentation

A matrix on the new colors and a single marker determines all their splits from the protected old tree when the old tree has not yet branched at the prescribed separation depth.

theorem marker_matrix_iff (S Q : PrescribedTree n)
    (old : D → S.Leaf) (fresh : C → S.Leaf) (a : D)
    (qold : D → Q.Leaf) (qfresh : C → Q.Leaf)
    (hold : ∀ d e, splitDepth S (old d) (old e)=splitDepth Q (qold d) (qold e))
    (hsep : ∀ c d, splitDepth Q (qfresh c) (qold a)<splitDepth Q (qold a) (qold d)) :
    (∀ x y : Option C,
      splitDepth S (Option.elim' (old a) fresh x) (Option.elim' (old a) fresh y)=
      splitDepth Q (Option.elim' (qold a) qfresh x) (Option.elim' (qold a) qfresh y)) ↔
    (∀ x y : D ⊕ C,
      splitDepth S (Sum.elim old fresh x) (Sum.elim old fresh y)=
      splitDepth Q (Sum.elim qold qfresh x) (Sum.elim qold qfresh y)) := by
…

Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.splitDepth