ShapeProjectionEnergy.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.PrescribedTree.branch_leaf_triple line 12

Source documentation

Pulling three independent copies of one sampled branch back to any one leaf keeps exactly the three independent path law.

lemma branch_leaf_triple (C : PrescribedTree n) (T : KernelTower Ω (n+1))
    (a : C.Leaf) (F : FinitePath Ω (n+1) → FinitePath Ω (n+1) →
      FinitePath Ω (n+1) → ℝ) :
    (T.1.bind (fun z => C.sampleLaw (T.2 z))).expect (fun x =>
      (T.1.bind (fun z => C.sampleLaw (T.2 z))).expect (fun y =>
        (T.1.bind (fun z => C.sampleLaw (T.2 z))).expect (fun w =>
          F (x.1,C.pathAt a x.2) (y.1,C.pathAt a y.2) (w.1,C.pathAt a w.2)))) =
    KernelTower.tripleExpectAt (n+1) T 0 F := by
…

Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.KernelTower.tripleExpectAt

def OAI.DilutedSpinGlass.PrescribedTree.branchProjectionSq line 42
Source documentation
The error is measured in the genuine two-copy branch law, in the same coupling as the physical spin products, not in a surrogate law.
```
noncomputable def branchProjectionSq (C : PrescribedTree n) (T : KernelTower Ω (n+1))
    (a : C.Leaf) (f Y : FinitePath Ω (n+1) → Fin N → ℝ) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath
lemma OAI.DilutedSpinGlass.PrescribedTree.branch_energy_projection_transfer line 48
def OAI.DilutedSpinGlass.PrescribedTree.shapeEnergyAt line 63
Source documentation
Conditional covariance of the actual shape with d preceding unary transitions, averaged over their genuine kernel prefix.
```
noncomputable def shapeEnergyAt (C : PrescribedTree n) : (d : ℕ) →
    KernelTower Ω (n+1+d) → (FinitePath Ω (n+1+d) → Fin N → ℝ) → ℝ
  | 0, T, f => childEnergy C T f
  | d+1, T, f => T.1.expect (fun z => shapeEnergyAt C d (T.2 z) (fun y => f (z,y)))
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.childEnergy
def OAI.DilutedSpinGlass.PrescribedTree.shapeProjectionSqAt line 68
theorem OAI.DilutedSpinGlass.PrescribedTree.shape_energy_projection_transfer line 77
Source documentation
Three-copy transfer at an arbitrary prefix above a complete literal multileaf shape. The shape's actual covariance is on the left.
```
theorem shape_energy_projection_transfer (C : PrescribedTree n) (a : C.Leaf)
    (d : ℕ) (T : KernelTower Ω (n+1+d))
    (f Y : FinitePath Ω (n+1+d) → Fin N → ℝ) :
    shapeEnergyAt C d T f ≤ 2*KernelTower.halfTripleDifferenceAt (n+1+d) T d Y +
      4*shapeProjectionSqAt C a d T f Y := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.PrescribedTree.shapeEnergyAt, OAI.DilutedSpinGlass.KernelTower.halfTripleDifferenceAt, OAI.DilutedSpinGlass.PrescribedTree.shapeProjectionSqAt
lemma OAI.DilutedSpinGlass.PrescribedTree.shapeEnergyAt_nonneg line 92
lemma OAI.DilutedSpinGlass.PrescribedTree.shapeProjectionSqAt_nonneg line 98