ExternalAverageTaylor.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.HeterogeneousMarks.affine_one_lower line 27
lemma OAI.DilutedSpinGlass.HeterogeneousMarks.affine_two_lower line 33
theorem OAI.DilutedSpinGlass.HeterogeneousMarks.externalAverage_taylor_bound line 43
Source documentation
Full finite-volume disorder averaging of the uniform all-order Taylor bound. Physical fields, physical Poisson terms and the entire countable reservoir are unchanged as the new insertion parameter varies.
```
theorem externalAverage_taylor_bound {t : ℝ} (ht : t ∈ Set.Icc (0:ℝ) (1/2)) (k : ℕ) :
    |externalAverage ξ μ ν η r s S a T Q m base old D E f t 0 -
      ∑ j ∈ Finset.range (k+1), externalCoefficientAverage ξ μ ν η r s S a T Q m base old D E f j*t^j| ≤
        (B*PrescribedTree.derivativeBound (S.leaves+(Finset.univ.erase a).card) (k+1)/(k.factorial:ℝ))*t^(k+1) := by
…
```
Mentions: OAI.DilutedSpinGlass.HeterogeneousMarks.externalAverage, OAI.DilutedSpinGlass.HeterogeneousMarks.externalCoefficientAverage, OAI.DilutedSpinGlass.PrescribedTree.derivativeBound
theorem OAI.DilutedSpinGlass.HeterogeneousMarks.externalAverage_sub_le line 59