DoubledStemProjection.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.PrescribedTree.doubledOverlap line 13
Source documentation
The overlap of every old leaf, with two complete independent descendant sides retained. This is also the normalized full leaf product.
```
noncomputable def doubledOverlap (S : PrescribedTree n) (f : FinitePath Ω (n+1) → Fin N → ℝ)
    (z : Sample Ω (doubled S)) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.doubled
lemma OAI.DilutedSpinGlass.PrescribedTree.doubledOverlap_eq line 19
theorem OAI.DilutedSpinGlass.PrescribedTree.oldProjectionError_doubled_stem_le line 33
Source documentation
The old-tree projection error in the signed matrix bound, on the literal doubled old tree, is controlled by the actual proper-child energies at its later first split. No conditional concentration assumption is imposed.
```
theorem oldProjectionError_doubled_stem_le (k : ℕ+) (C : Fin k → PrescribedTree n)
    (a : (PrescribedTree.node k C).Leaf) (r : ℕ)
    (T : KernelTower Ω (n+1+r+1)) (f : FinitePath Ω (n+1+r+1) → Fin N → ℝ)
    (hf : ∀ x i, |f x i|≤1) :
    let S := PrescribedTree.node k C
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath
def OAI.DilutedSpinGlass.PrescribedTree.stemInternal line 100
lemma OAI.DilutedSpinGlass.PrescribedTree.splitDepth_stem line 104
lemma OAI.DilutedSpinGlass.PrescribedTree.freshSplitDepth_stem line 113
def OAI.DilutedSpinGlass.PrescribedTree.splitProjector line 124
Source documentation
A later-split projector lifted through an arbitrary actual ancestral prefix, without flattening the dependent tuple representation of paths.
```
noncomputable def splitProjector (S : PrescribedTree n) (r : ℕ) :
    (d : ℕ) → KernelTower Ω (n+r+1+d) → (FinitePath Ω (n+r+1+d) → ℝ) →
      FinitePath Ω (n+r+1+d) → ℝ
  | 0,T,f,x => tailMean S (r+1) T f x
  | d+1,T,f,x => splitProjector S r d (T.2 x.1) (fun y => f (x.1,y)) x.2
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.tailMean
lemma OAI.DilutedSpinGlass.PrescribedTree.splitProjector_bound line 130
theorem OAI.DilutedSpinGlass.PrescribedTree.stem_doubled_projector_old_side line 140
Source documentation
The old-side geometric premise of the full signed matrix identity at an arbitrary evaluation depth d. All old leaves and sampled ancestors remain.
```
theorem stem_doubled_projector_old_side (S : PrescribedTree n) (r d : ℕ)
    (a b : (stem S r).Leaf) (T : KernelTower Ω (n+r+1+d))
    (f : FinitePath Ω (n+r+1+d) → Fin N → ℝ)
    (c : (stem (doubled (stem S r)) d).Leaf)
    (hc : splitDepth (stem (doubled (stem S r)) d)
      (stemLeaf (doubled (stem S r)) d ⟨0,a⟩) c=d)
    (z : Sample Ω (stem (doubled (stem S r)) d)) :
    (fun i => splitProjector S r d T (fun x => f x i)
      ((stem (doubled (stem S r)) d).pathAt c z)) =
    (fun i => splitProjector S r d T (fun x => f x i)
      ((stem (doubled (stem S r)) d).pathAt
        (stemLeaf (doubled (stem S r)) d ⟨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.stemLeaf, OAI.DilutedSpinGlass.PrescribedTree.Sample, OAI.DilutedSpinGlass.PrescribedTree.splitProjector, OAI.DilutedSpinGlass.PrescribedTree.pathAt