SplitDepthContinuity.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.PrescribedTree.pairDivergence line 14

Source documentation

Divergence from one referenced leaf, with every old child retained.

noncomputable def pairDivergence : {n : ℕ} → (S : PrescribedTree n) →
    S.Leaf → (d : ℕ) → d < n → Divergence S
  | _+1, .node _ _, a, 0, _ => .here {a.1}
  | _+1, .node _ C, a, d+1, hd => .descend a.1 (pairDivergence (C a.1) a.2 d (by omega))

Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Divergence

lemma OAI.DilutedSpinGlass.PrescribedTree.pairDivergence_coefficient line 19
lemma OAI.DilutedSpinGlass.PrescribedTree.pairDivergence_old line 30
lemma OAI.DilutedSpinGlass.PrescribedTree.pairDivergence_fresh line 57
theorem OAI.DilutedSpinGlass.PrescribedTree.pair_choice_total line 91
Source documentation
Exact signed total of every path splitting from the anchor at d.
```
theorem pair_choice_total {n : ℕ} (S : PrescribedTree n) (a : S.Leaf)
    (d : ℕ) (hd : d < n) (m : Fin (n+1) → ℝ) (hend : m (Fin.last n) = 1) :
    (∑ b : S.Leaf, if splitDepth S a b = d then (1:ℝ) else 0) +
      (∑ v : S.Internal, if splitDepth (grow S v) (oldLeaf S v a) (newLeaf S v) = d
        then gamma S m v else 0) = m ⟨d,by omega⟩ - m ⟨d+1,by omega⟩ := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.splitDepth, OAI.DilutedSpinGlass.PrescribedTree.grow, OAI.DilutedSpinGlass.PrescribedTree.oldLeaf, OAI.DilutedSpinGlass.PrescribedTree.newLeaf, OAI.DilutedSpinGlass.PrescribedTree.gamma

def OAI.DilutedSpinGlass.PrescribedTree.stem line 112

Source documentation

Add an actual unary initial stem, preserving all descendant geometry.

def stem (S : PrescribedTree n) : (r : ℕ) → PrescribedTree (n+r)
  | 0 => S
  | r+1 => unary (stem S r)

/-- A literal family with one ranged split. The child shapes and all their
later branching depths are fixed. Moving d delays only this split. -/

Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.unary

def OAI.DilutedSpinGlass.PrescribedTree.splitFamily line 118
Source documentation
A literal family with one ranged split. The child shapes and all their later branching depths are fixed. Moving d delays only this split.
```
def splitFamily (k : ℕ+) (C : Fin k → PrescribedTree n) :
    (r : ℕ) → Fin (r+1) → PrescribedTree (n+r+1)
  | 0, _ => .node k C
  | r+1, d => Fin.cases (.node k (fun i => stem (C i) (r+1)))
      (fun j => unary (splitFamily k C r j)) d
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.stem, OAI.DilutedSpinGlass.PrescribedTree.unary
lemma OAI.DilutedSpinGlass.PrescribedTree.splitFamily_zero line 124
lemma OAI.DilutedSpinGlass.PrescribedTree.splitFamily_succ line 128
def OAI.DilutedSpinGlass.PrescribedTree.tailMean line 133
Source documentation
On one real kernel path, retain its prefix and compute the true mean of its descendant shape. Omitted sampled branches have integrated to one.
```
noncomputable def tailMean (S : PrescribedTree n) : (r : ℕ) → KernelTower Ω (n+r) →
    (FinitePath Ω (n+r) → ℝ) → FinitePath Ω (n+r) → ℝ
  | 0, T, f, _ => treeMean S T f
  | r+1, T, f, x => tailMean S r (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.treeMean
lemma OAI.DilutedSpinGlass.PrescribedTree.tailMean_bound line 138
lemma OAI.DilutedSpinGlass.PrescribedTree.tailMean_expect line 145
def OAI.DilutedSpinGlass.PrescribedTree.tailVariance line 158
lemma OAI.DilutedSpinGlass.PrescribedTree.tailVariance_nonneg line 162
lemma OAI.DilutedSpinGlass.PrescribedTree.tailVariance_le_one line 166
lemma OAI.DilutedSpinGlass.PrescribedTree.tailVariance_step line 170
def OAI.DilutedSpinGlass.PrescribedTree.splitShiftEnergy line 185
Source documentation
The sum of squared changes of the actual descendant mean when one split is ranged over ALL available depths, with arbitrary fixed later child shapes.
```
noncomputable def splitShiftEnergy (k : ℕ+) (C : Fin k → PrescribedTree n)
    (r : ℕ) (T : KernelTower Ω (n+r+1)) (f : FinitePath Ω (n+r+1) → ℝ) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath
lemma OAI.DilutedSpinGlass.PrescribedTree.splitShiftEnergy_step_le line 190
theorem OAI.DilutedSpinGlass.PrescribedTree.splitShiftEnergy_le_variance line 214
theorem OAI.DilutedSpinGlass.PrescribedTree.splitShiftEnergy_le line 235