StemCovarianceTransfer.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.PrescribedTree.oldProjectionError_doubled_sq line 13
Source documentation
The old projection error and the physical two-copy projection energy are exactly the same coupling, not only equal separate marginal errors.
```
lemma oldProjectionError_doubled_sq (S : PrescribedTree n) (a : S.Leaf)
    (T : KernelTower Ω (n+1)) (f X : FinitePath Ω (n+1) → Fin N → ℝ) :
    (oldProjectionError (doubled S) T ⟨0,a⟩ ⟨1,a⟩ (doubledOverlap S f) X)^2 =
      branchProjectionSq S T a f X := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.oldProjectionError, OAI.DilutedSpinGlass.PrescribedTree.doubled, OAI.DilutedSpinGlass.PrescribedTree.doubledOverlap, OAI.DilutedSpinGlass.PrescribedTree.branchProjectionSq
theorem OAI.DilutedSpinGlass.PrescribedTree.branchProjectionSq_stem_le line 33
Source documentation
The proper-child covariance estimate for the exact coupled projection energy required by the three-copy transfer.
```
theorem branchProjectionSq_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) :
    branchProjectionSq (stem (.node k C) r) T (stemLeaf (.node k C) r a) f
      (fun x i => tailMean (.node k C) (r+1) T (fun y => f y i) x) ≤
      4*(k:ℝ)*∑ i, Real.sqrt (shapeEnergyAt (C i) (r+1) T f) := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.branchProjectionSq, OAI.DilutedSpinGlass.PrescribedTree.stem, OAI.DilutedSpinGlass.PrescribedTree.stemLeaf, OAI.DilutedSpinGlass.PrescribedTree.tailMean, OAI.DilutedSpinGlass.PrescribedTree.shapeEnergyAt
theorem OAI.DilutedSpinGlass.PrescribedTree.stem_covariance_three_copy_le line 49
Source documentation
The left side is the covariance energy of the actual entire multileaf shape. Thus the full projected THREE-copy observable, not just projected covariance, is the only outstanding scalar in this transfer.
```
theorem stem_covariance_three_copy_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) :
    childEnergy (stem (.node k C) r) T f ≤
      2*KernelTower.halfTripleDifferenceAt (n+1+r+1) T 0
        (fun x i => tailMean (.node k C) (r+1) T (fun y => f y i) x) +
      16*(k:ℝ)*∑ i, Real.sqrt (shapeEnergyAt (C i) (r+1) T f) := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.childEnergy, OAI.DilutedSpinGlass.PrescribedTree.stem, OAI.DilutedSpinGlass.KernelTower.halfTripleDifferenceAt, OAI.DilutedSpinGlass.PrescribedTree.tailMean, OAI.DilutedSpinGlass.PrescribedTree.shapeEnergyAt