ScheduledFrameError.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DilutedSpinGlass.ReducedTopology.shiftedFrameHeight line 14
def OAI.DilutedSpinGlass.ReducedTopology.delayedFrame line 17
Source documentation
The literal two delayed target sides, retaining all old depth coordinates.
```
def delayedFrame (H r d : ℕ) (k : ℕ+) (C : Fin k → ReducedTopology)
    (q : (j : Fin k) → (C j).Vertex → ℕ) : PrescribedTree (H+1+1+r+1+d) :=
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.PrescribedTree
theorem OAI.DilutedSpinGlass.ReducedTopology.scheduled_frame_target_error_le line 26
Source documentation
Complete target projection comparison at the SAME height as the old frame. Both projectors and both entire target sides are the literal scheduled trees. No desired covariance estimate is an input.
```
theorem scheduled_frame_target_error_le (H r d : ℕ) (k : ℕ+) (hk : 2≤(k:ℕ))
    (a : α) (C : Fin k → ReducedTopology)
    (e : (j : Fin k) → (C j).Vertex → {j : α // j≠a})
    (Q : α → Fin (H+1+1+r+1+d)) (ha : (Q a).val=r+1+d)
    (hQ : ∀ j v, (Q a).val+1≤(Q (e j v)).val)
    (T : KernelTower Ω (H+1+1+r+1+d))
    (f : FinitePath Ω (H+1+1+r+1+d) → Fin N → ℝ) (hf : ∀ x i, |f x i|≤1) :
    let ht := shiftedFrameHeight H r d
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.ReducedTopology.shiftedFrameHeight
lemma OAI.DilutedSpinGlass.kernelHeightCast_succ_fst line 95
lemma OAI.DilutedSpinGlass.kernelHeightCast_succ_snd line 101
lemma OAI.DilutedSpinGlass.vectorHeightCast_succ_pair line 108
lemma OAI.DilutedSpinGlass.PrescribedTree.descendantEnergyAt_eq_shapeEnergyAt line 119
Source documentation
A proper-child covariance is the SAME single-copy covariance evaluated at the child's retained evaluation coordinate. Its two successive prefix averages are just one original-kernel prefix, not an independent pair of copies.
```
lemma descendantEnergyAt_eq_shapeEnergyAt (C : PrescribedTree n) (r d : ℕ)
    (T : KernelTower Ω (n+1+r+1+d)) (f : FinitePath Ω (n+1+r+1+d) → Fin N → ℝ) :
    descendantEnergyAt C r d T f = shapeEnergyAt C (r+1+d)
      (kernelHeightCast (by omega) T) (vectorHeightCast (by omega) f) := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.descendantEnergyAt, OAI.DilutedSpinGlass.PrescribedTree.shapeEnergyAt, OAI.DilutedSpinGlass.kernelHeightCast, OAI.DilutedSpinGlass.vectorHeightCast