OAI/Probability/DilutedSpin/CavityProxy.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.UniversalDictionary.cavityProxy line 19
2. lemma OAI.DilutedSpinGlass.UniversalDictionary.cavitySiteEnergy_ae_bound line 28
3. lemma OAI.DilutedSpinGlass.UniversalDictionary.cavityBondEnergy_ae_bound line 41
4. lemma OAI.DilutedSpinGlass.UniversalDictionary.cavityProxy_comparison_tendsto line 52
5. def OAI.DilutedSpinGlass.functionalEnvelope line 119
6. lemma OAI.DilutedSpinGlass.functional_envelope line 122
7. lemma OAI.DilutedSpinGlass.variationalValue_le_functional_integrable line 151
8. lemma OAI.DilutedSpinGlass.FiniteLaw.pi_point line 179
9. lemma OAI.DilutedSpinGlass.mixedEnergy_true line 192
10. lemma OAI.DilutedSpinGlass.mixedEnergy_false line 199
11. def OAI.DilutedSpinGlass.PrescribedTree.edgeRoot line 213
12. lemma OAI.DilutedSpinGlass.PrescribedTree.mixedRootIncrement_true line 220
13. lemma OAI.DilutedSpinGlass.PrescribedTree.mixedRootIncrement_false line 237
14. lemma OAI.DilutedSpinGlass.PrescribedTree.integral_real_cavity_bound line 252

    Source documentation

    The upper local producer with an actual extensive energy in its old tree; the compensator is independent of that tree and is precisely an edge root.

    lemma integral_real_cavity_bound (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,(FiniteLaw.pi (fun _ : Fin p => (FiniteLaw.uniform : FiniteLaw (Fin N)))).expect (fun i =>
            KernelTower.backwardLog n T (fun j => m j.succ) (fun y => f y+z.1 (fun j => V y (i j)))-
              KernelTower.backwardLog n T (fun j => m j.succ) f) ∂M.disorder.toMeasure)+
          ((p-1:ℕ):ℝ)*(∫ z,edgeRoot Q U x (fun j => m j.succ) z ∂M.disorder.toMeasure) ≤
          (p:ℝ)*(∫ z,mixedRootIncrement T Q U V x m f z (fun l => decide (l=j)) ∂M.disorder.toMeasure) := by
    …

    Mentions: OAI.DilutedSpinGlass.Model, OAI.DilutedSpinGlass.Admissible, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.Spin, OAI.DilutedSpinGlass.FiniteLaw.pi, OAI.DilutedSpinGlass.FiniteLaw.uniform, OAI.DilutedSpinGlass.KernelTower.backwardLog, OAI.DilutedSpinGlass.PrescribedTree.edgeRoot, OAI.DilutedSpinGlass.PrescribedTree.mixedRootIncrement