OAI/Probability/DilutedSpin/HeightTransport.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.kernelHeightCast line 10

   Source documentation

   Transport along equality of total depths only; no change to a kernel.

   def kernelHeightCast {Ω : Type} [Fintype Ω] {n m : ℕ} (h : n=m)
       (T : KernelTower Ω n) : KernelTower Ω m := h ▸ T

   Mentions: OAI.DilutedSpinGlass.KernelTower

2. def OAI.DilutedSpinGlass.pathHeightCast line 13
3. def OAI.DilutedSpinGlass.vectorHeightCast line 16
4. theorem OAI.DilutedSpinGlass.kernelHeightCast_inv line 20
5. theorem OAI.DilutedSpinGlass.vectorHeightCast_inv line 22
6. def OAI.DilutedSpinGlass.PrescribedTree.heightCast line 28
7. def OAI.DilutedSpinGlass.PrescribedTree.leafHeightCast line 30
8. lemma OAI.DilutedSpinGlass.PrescribedTree.leafHeightCast_bijective line 33
9. theorem OAI.DilutedSpinGlass.PrescribedTree.splitDepth_heightCast line 36
10. theorem OAI.DilutedSpinGlass.PrescribedTree.matrixProjectionError_heightCast line 41
11. theorem OAI.DilutedSpinGlass.ReducedTopology.conditionalScheduledProduct_heightCast line 53
12. theorem OAI.DilutedSpinGlass.ReducedTopology.projectionShiftError_heightCast line 60