UpperCountState.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.PrescribedTree.CavityState line 12
Source documentation
Each cavity interaction has its own independent p-tuple of trial trees.
```
def CavityState (Ω Λ : Type) (p : ℕ) : ℕ → Type
  | 0 => Ω
  | l+1 => CavityState Ω Λ p l × (Fin p → Λ)
```
instance OAI.DilutedSpinGlass.PrescribedTree.cavityStateFintype line 16
def OAI.DilutedSpinGlass.PrescribedTree.cavityProject line 23
def OAI.DilutedSpinGlass.PrescribedTree.cavityTower line 29
def OAI.DilutedSpinGlass.PrescribedTree.cavityEnergy line 34
lemma OAI.DilutedSpinGlass.PrescribedTree.pathMap_id line 45
lemma OAI.DilutedSpinGlass.PrescribedTree.pathMap_cavityProject line 51
lemma OAI.DilutedSpinGlass.PrescribedTree.cavityEnergy_add line 58
lemma OAI.DilutedSpinGlass.PrescribedTree.cavityEnergy_bound line 76
def OAI.DilutedSpinGlass.PrescribedTree.cavityRoot line 91
lemma OAI.DilutedSpinGlass.PrescribedTree.cavityRoot_bound line 99

lemma OAI.DilutedSpinGlass.PrescribedTree.cavityRoot_succ_difference line 110

Source documentation

Appending an actual cavity block is the fresh-tree term of the physical local interpolation. There is no endpoint or increment hypothesis.

lemma cavityRoot_succ_difference (T : KernelTower Ω n) (Q : FiniteLaw R)
    (U : R → KernelTower Λ n) (V : FinitePath Ω n → Fin N → Spin)
    (x : R → FinitePath Λ n → ℝ) (m : Fin (n+1) → ℝ) (j : Fin p) (l : ℕ)
    (r : RootPath (Fin p → R) l) (i : RootPath (Fin p → Fin N) l)
    (z : RootPath (InteractionSample p) l) (f : FinitePath Ω n → ℝ) (θ : InteractionSample p) :
    (FiniteLaw.pi (fun _ : Fin p => (FiniteLaw.uniform : FiniteLaw (Fin N)))).expect (fun a =>
      (FiniteLaw.pi (fun _ : Fin p => Q)).expect (fun b =>
        cavityRoot T U V x (fun d => m d.succ) j (l+1) (b,r) (a,i) (θ,z) f))-
      cavityRoot T U V x (fun d => m d.succ) j l r i z f =
    mixedRootIncrement (cavityTower T U l r) Q U
      (fun y => V (pathMap (cavityProject l) n y)) x m
      (cavityEnergy V x j l r i z f) θ (fun a => decide (a=j)) := by
…