OAI/Probability/DilutedSpin/UpperRegularized.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.PrescribedTree.mixedLogAvg line 12
2. lemma OAI.DilutedSpinGlass.PrescribedTree.mixedQMoment_eq line 21
3. lemma OAI.DilutedSpinGlass.PrescribedTree.mixedLogAvg_negative_tail line 37
4. lemma OAI.DilutedSpinGlass.PrescribedTree.measurable_mixedLogAvg line 56
5. lemma OAI.DilutedSpinGlass.PrescribedTree.integrable_mixedLogAvg line 69
6. lemma OAI.DilutedSpinGlass.PrescribedTree.integral_mixedLogAvg_negative_tail line 83
7. lemma OAI.DilutedSpinGlass.PrescribedTree.negative_series_combination line 107
8. lemma OAI.DilutedSpinGlass.PrescribedTree.integral_mixedLog_combination_nonpos line 130

   Source documentation

   The common-tree regularized interpolation derivative has the required sign under the original factorization and positivity hypotheses.

   lemma integral_mixedLog_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)
       (hnz : ∀ j : Fin n,m j.succ≠0) (hroot : m 0=0) (hend : m (Fin.last n)=1)
       (j : Fin p) {t : ℝ} (ht0 : 0≤t) (ht : t<1) :
       (∫ z,mixedLogAvg T Q U V x m z (fun _ => true) t ∂M.disorder.toMeasure)-
         (p:ℝ)*(∫ z,mixedLogAvg T Q U V x m z (fun l => decide (l=j)) t ∂M.disorder.toMeasure)+
         ((p-1:ℕ):ℝ)*(∫ z,mixedLogAvg T Q U V x m z (fun _ => false) t ∂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.mixedLogAvg