OAI/Probability/DilutedSpin/HistoryDistinct.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.DilutedSpinGlass.PrescribedTree.HistoryValid line 11
2. lemma OAI.DilutedSpinGlass.PrescribedTree.HistoryValid.pick_old line 17
3. lemma OAI.DilutedSpinGlass.PrescribedTree.HistoryValid.pick_fresh line 46
4. lemma OAI.DilutedSpinGlass.PrescribedTree.labeledHistory_congr_distinct line 80

   Source documentation

   A colored history never reuses a position. Thus identities only need to be proved on terminal tuples of distinct geometric leaves, not sample values.

   lemma labeledHistory_congr_distinct (m : Fin (n+1) → ℝ)
       (V W : (S : PrescribedTree n) → (C → S.Leaf) → (Sample Ω S → ℝ) → ℝ)
       (hVW : ∀ S pos f, Function.Injective pos → V S pos f = W S pos f)
       (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)
       (h : HistoryValid S U loc P pos) (f : Sample Ω S → ℝ) :
       labeledHistory m V cs S U loc pos f = labeledHistory m W cs S U loc pos f := by
   …

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

5. lemma OAI.DilutedSpinGlass.PrescribedTree.anchorHistory_valid line 114