StemCoupling.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.PrescribedTree.stemLeaf_bijective line 13
lemma OAI.DilutedSpinGlass.PrescribedTree.tailMean_path_stem line 30
Source documentation
The actual projector uses only the sampled stem. It does not depend on which old descendant leaf represents that stem.
```
lemma tailMean_path_stem (S : PrescribedTree n) (r : ℕ) (a b : S.Leaf)
    (T : KernelTower Ω (n+r)) (f : FinitePath Ω (n+r) → ℝ)
    (z : Sample Ω (stem S r)) :
    tailMean S r T f ((stem S r).pathAt (stemLeaf S r a) z) =
      tailMean S r T f ((stem S r).pathAt (stemLeaf S r b) z) := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.stem, OAI.DilutedSpinGlass.PrescribedTree.tailMean, OAI.DilutedSpinGlass.PrescribedTree.pathAt, OAI.DilutedSpinGlass.PrescribedTree.stemLeaf
lemma OAI.DilutedSpinGlass.PrescribedTree.tailMean_any_path_stem line 39
theorem OAI.DilutedSpinGlass.PrescribedTree.doubled_stem_projector_old_side line 51
Source documentation
In the literal two-copy old tree, every leaf opposite the anchor has exactly the same projected vector as the designated old-II leaf. This is the geometric hOld premise of the full signed-matrix estimate.
```
theorem doubled_stem_projector_old_side (S : PrescribedTree n) (r : ℕ)
    (a b : (stem S r).Leaf) (T : KernelTower Ω (n+r+1))
    (f : FinitePath Ω (n+r+1) → Fin N → ℝ)
    (c : (doubled (stem S r)).Leaf)
    (hc : splitDepth (doubled (stem S r)) ⟨0,a⟩ c=0)
    (z : Sample Ω (doubled (stem S r))) :
    (fun i => tailMean S (r+1) T (fun x => f x i)
      ((doubled (stem S r)).pathAt c z)) =
    (fun i => tailMean S (r+1) T (fun x => f x i)
      ((doubled (stem S r)).pathAt ⟨1,b⟩ z)) := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.stem, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.doubled, OAI.DilutedSpinGlass.PrescribedTree.splitDepth, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.tailMean, OAI.DilutedSpinGlass.PrescribedTree.pathAt
lemma OAI.DilutedSpinGlass.ReducedTopology.leaf_card_pos line 89
lemma OAI.DilutedSpinGlass.ReducedTopology.child_leaf_card_lt line 100
Source documentation
Every proper child consumes strictly fewer leaves, without suppressing or identifying distinct child occurrences with the same topology.
```
lemma child_leaf_card_lt (k : ℕ+) (hk : 2≤(k:ℕ)) (C : Fin k → ReducedTopology)
    (j : Fin k) : Fintype.card (C j).Leaf <
      Fintype.card (ReducedTopology.node k hk C).Leaf := by
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.ReducedTopology.Leaf