ShiftedTree.lean`

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.PrescribedTree.bottomUnary line 16
Source documentation
Extending the final unary edge keeps every internal branching depth. In contrast, unary S delays all of them by exactly one.
```
def bottomUnary : {n : ℕ} → PrescribedTree n → PrescribedTree (n+1)
  | 0, .leaf => unary .leaf
  | _+1, .node k C => .node k (fun i => bottomUnary (C i))
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.unary
def OAI.DilutedSpinGlass.PrescribedTree.bottomLeaf line 20
lemma OAI.DilutedSpinGlass.PrescribedTree.bottomLeaf_bijective line 24
lemma OAI.DilutedSpinGlass.PrescribedTree.splitDepth_bottom_ne line 49
lemma OAI.DilutedSpinGlass.PrescribedTree.branchingCount_bottom line 65
lemma OAI.DilutedSpinGlass.PrescribedTree.branchingCount_unary line 74
lemma OAI.DilutedSpinGlass.PrescribedTree.leaves_bottom line 81
lemma OAI.DilutedSpinGlass.PrescribedTree.leaves_unary line 88
lemma OAI.DilutedSpinGlass.PrescribedTree.branchingCount_eq_vertexSum line 94
Source documentation
Literal branching-vertex count as a sum. Distinct vertices at equal depths occur separately; no count by distinct depth values is substituted.
```
lemma branchingCount_eq_vertexSum {n : ℕ} (S : PrescribedTree n) (P : ℕ → Prop) :
    branchingCount S P = ∑ v : S.Internal,
      if 1 < vertexArity S v ∧ P (vertexDepth S v) then 1 else 0 := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.branchingCount, OAI.DilutedSpinGlass.PrescribedTree.vertexArity, OAI.DilutedSpinGlass.PrescribedTree.vertexDepth
def OAI.DilutedSpinGlass.PrescribedTree.branchingDepths line 107
lemma OAI.DilutedSpinGlass.PrescribedTree.mem_branchingDepths line 111
lemma OAI.DilutedSpinGlass.PrescribedTree.branchingCount_congr_on line 116
lemma OAI.DilutedSpinGlass.PrescribedTree.branchingCount_eq_zero_iff line 128
def OAI.DilutedSpinGlass.PrescribedTree.doubled line 145
Source documentation
Both copies are aligned, but the two occurrences are different vertices.
```
def doubled {n : ℕ} (S : PrescribedTree n) : PrescribedTree (n+1) := .node 2 (fun _ => S)
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree
def OAI.DilutedSpinGlass.PrescribedTree.shiftedTwinDepths line 147
lemma OAI.DilutedSpinGlass.PrescribedTree.zero_not_mem_shiftedTwinDepths line 150
def OAI.DilutedSpinGlass.PrescribedTree.NoAdjacentBranchDepths line 157
Source documentation
Regular depth assignments imply this no-adjacent-depth condition once eta L > 1. It is precisely the geometric premise of shifted charging.
```
def NoAdjacentBranchDepths {n : ℕ} (S : PrescribedTree n) : Prop :=
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree
lemma OAI.DilutedSpinGlass.PrescribedTree.shifted_twin_old_count line 160
lemma OAI.DilutedSpinGlass.PrescribedTree.shifted_twin_target_count line 173
lemma OAI.DilutedSpinGlass.PrescribedTree.shifted_twin_total_count line 188
def OAI.DilutedSpinGlass.PrescribedTree.stemLeaf line 212
Source documentation
Retain a specified descendant leaf through the actual unary prefix.
```
def stemLeaf (S : PrescribedTree n) : (r : ℕ) → S.Leaf → (stem S r).Leaf
  | 0, a => a
  | r+1, a => ⟨0,stemLeaf S r a⟩
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.stem, OAI.DilutedSpinGlass.PrescribedTree.Leaf
lemma OAI.DilutedSpinGlass.PrescribedTree.sampleLaw_unary_expect line 216
lemma OAI.DilutedSpinGlass.PrescribedTree.leafProduct_unary line 225
def OAI.DilutedSpinGlass.PrescribedTree.stemContractionSq line 235
Source documentation
The true L2 contraction projection error, retaining the entire sampled prefix to the designated branching node. The projector is the literal conditional descendant mean evaluated on the chosen leaf's path.
```
noncomputable def stemContractionSq (S : PrescribedTree n) (a : S.Leaf) (r : ℕ)
    (T : KernelTower Ω (n+r)) (f : FinitePath Ω (n+r) → Fin N → ℝ) (B : Fin N → ℝ) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath
lemma OAI.DilutedSpinGlass.PrescribedTree.stemContractionSq_step line 241
theorem OAI.DilutedSpinGlass.PrescribedTree.stem_node_contraction_sq_le line 260
Source documentation
Actual projection at an arbitrary later first split; child covariances are averaged over the very same ancestral prefix. No decorrelation premise is assumed. Constants are dimension-free, including zero spatial size.
```
theorem stem_node_contraction_sq_le (k : ℕ+) (C : Fin k → PrescribedTree n)
    (a : (PrescribedTree.node k C).Leaf) (r : ℕ)
    (T : KernelTower Ω (n+1+r)) (f : FinitePath Ω (n+1+r) → Fin N → ℝ)
    (hf : ∀ x i, |f x i|≤1) (B : Fin N → ℝ) (hB : ∀ i, |B i|≤1) :
    stemContractionSq (.node k C) a r T f B ≤
      (k:ℝ)*∑ i, Real.sqrt (shapeEnergyAt (C i) r T f) := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.stemContractionSq, OAI.DilutedSpinGlass.PrescribedTree.shapeEnergyAt
theorem OAI.DilutedSpinGlass.PrescribedTree.stem_node_projection_independent line 287
Source documentation
A separate complete sampled side may multiply the contraction. It is independent below the common evaluation prefix, not averaged away.
```
theorem stem_node_projection_independent {Λ : Type*} [Fintype Λ]
    (Q : FiniteLaw Λ) (k : ℕ+) (C : Fin k → PrescribedTree n)
    (a : (PrescribedTree.node k C).Leaf) (r : ℕ)
    (T : KernelTower Ω (n+1+r)) (f : FinitePath Ω (n+1+r) → Fin N → ℝ)
    (hf : ∀ x i, |f x i|≤1) (B : Λ → Fin N → ℝ) (hB : ∀ x i, |B x i|≤1) :
    let S := PrescribedTree.node k C
…
```
Mentions: OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath