MatrixPair.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.PrescribedTree.singleton_history_cover line 18

theorem OAI.DilutedSpinGlass.PrescribedTree.matrixHistory_first_pair line 36

Source documentation

The actual full prescribed split-matrix history, retaining just the anchor and the first newly assigned path, is its exact kappa ratio times the literal one-color pair history. All unused old replicas and their joint test remain. This is not a reference-history assumption.

theorem matrixHistory_first_pair (T : PrescribedTree n) (q : C → T.Leaf)
    (hq : Function.Injective q) (K : KernelTower Ω n) (m : Fin (n+1) → ℝ)
    (hm : StrictMono m) (hp : ∀ j, 0 ≤ m j) (hend : m (Fin.last n) = 1)
    (a c : C) (hac : a ≠ c) (cs : List C) (hcs : cs.Nodup)
    (hdis : ∀ d ∈ cs, d ∉ insert c ({a} : Finset C))
    (hfull : insert c ({a} : Finset C) ∪ cs.toFinset = Finset.univ)
    (S : PrescribedTree n) (x : S.Leaf)
    (R : FinitePath Ω n → FinitePath Ω n → ℝ) (f : Sample Ω S → ℝ) :
    weightedMatrixHistory T q
      (fun D pos g => (D.sampleLaw K).expect
        (fun z => g z * R (D.pathAt (pos a) z) (D.pathAt (pos c) z)))
      m (c::cs) S (Finset.univ.erase x) id (fun _ => x) f =
…

Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.weightedMatrixHistory

lemma OAI.DilutedSpinGlass.PrescribedTree.measurable_pairObservableHistory_tilt line 156
def OAI.DilutedSpinGlass.PrescribedTree.pairHistoryMass line 178
Source documentation
Total absolute mass controlling one added color, with the entire old tree left present. The bound is independent of the realized reservoir size.
```
noncomputable def pairHistoryMass (S : PrescribedTree n) (m : Fin (n+1) → ℝ) (a : S.Leaf) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree
lemma OAI.DilutedSpinGlass.PrescribedTree.pairObservableHistory_bound line 181