OAI/Probability/DilutedSpin/RootPatternComparison.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.HeterogeneousMarks.rootPatternMass line 25
2. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.root_pattern_replacement line 29
3. lemma OAI.DilutedSpinGlass.Pattern.empirical_eq_uniform line 93
4. lemma OAI.DilutedSpinGlass.Pattern.uniform_patterns line 100
5. lemma OAI.DilutedSpinGlass.PrescribedTree.treeMean_uniform_patterns line 123
6. lemma OAI.DilutedSpinGlass.PrescribedTree.integral_logInsertion_tail line 147
7. lemma OAI.DilutedSpinGlass.PrescribedTree.logExpansion_comparison line 177

   Source documentation

   Comparing two integrated finite expansions only requires finitely many coefficient errors, with the same uniform geometric remainder.

   lemma logExpansion_comparison {A B : ℝ} {a b : ℕ → ℝ} (K : ℕ) {t R : ℝ}
       (hA : |A-∑ k∈Finset.range K,(-1:ℝ)^k/(k+1)*a k*t^(k+1)|≤R)
       (hB : |B-∑ k∈Finset.range K,(-1:ℝ)^k/(k+1)*b k*t^(k+1)|≤R) :
       |A-B|≤2*R+∑ k∈Finset.range K, |t|^(k+1)/(k+1)*|a k-b k| := by
   …