UpperRootInsertion.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.PrescribedTree.mixedRootIncrement line 13
Source documentation
The actual root energy difference on appending a fresh independent block, with the ordinary physical energy held fixed.
```
noncomputable def mixedRootIncrement (T : KernelTower Ω n)
    (Q : FiniteLaw R) (U : R → KernelTower Λ n)
    (V : FinitePath Ω n → Fin N → Spin) (x : R → FinitePath Λ n → ℝ)
    (m : Fin (n+1) → ℝ) (f : FinitePath Ω n → ℝ)
    (z : InteractionSample p) (sel : Fin p → Bool) : ℝ :=
…
```
Mentions: OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.InteractionSample
lemma OAI.DilutedSpinGlass.PrescribedTree.mixedRootIncrement_eq line 24

lemma OAI.DilutedSpinGlass.PrescribedTree.integral_mixedRoot_combination_nonpos line 41

Source documentation

The local upper interpolation decrement, now a difference of actual unperturbed root free energies rather than an assumed tilted increment.

lemma integral_mixedRoot_combination_nonpos (M : Model p) (hM : Admissible M)
    (T : KernelTower Ω n) (Q : FiniteLaw R) (U : R → KernelTower Λ n)
    (V : FinitePath Ω n → Fin N → Spin) (x : R → FinitePath Λ n → ℝ)
    (m : Fin (n+1) → ℝ) (hm : Monotone m) (hpos : ∀ j,0 ≤ m j)
    (hstrict : ∀ j : Fin n,0 < m j.succ) (hroot : m 0=0) (hend : m (Fin.last n)=1)
    (f : FinitePath Ω n → ℝ) (j : Fin p) :
    (∫ z,mixedRootIncrement T Q U V x m f z (fun _ => true) ∂M.disorder.toMeasure)-
      (p:ℝ)*(∫ z,mixedRootIncrement T Q U V x m f z (fun l => decide (l=j)) ∂M.disorder.toMeasure)+
      ((p-1:ℕ):ℝ)*(∫ z,mixedRootIncrement T Q U V x m f z (fun _ => false) ∂M.disorder.toMeasure) ≤0 := by
…

Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.Admissible, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.PrescribedTree.mixedRootIncrement