OAI/Probability/DilutedSpin/SelectedTree.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.HeterogeneousMarks.selectedTreeMean line 15
2. def OAI.DilutedSpinGlass.HeterogeneousMarks.selectedTreeScore line 24
3. def OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedTreeMean line 41
4. def OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedTreeScore line 44
5. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_fullSelectedTreeMean line 47
6. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_fullSelectedTreeScore line 60
7. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedTreeMean_bound line 74
8. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedTreeScore_bound line 79
9. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedTree_centered_bound line 94

   Source documentation

   Exact old-tree/one-path estimate at every disorder realization, with the identical selected tower used in the globally centered score error.

   lemma fullSelectedTree_centered_bound {B center : ℝ} (hB : 0 ≤ B) (hf : ∀ x, |f x| ≤ B)
       (z : FullRootState Y X I M) :
       |fullSelectedTreeScore S a T Q m base sel fixed D E t u f z -
         fullSelectedTreeMean S T Q m base sel fixed D E t u f z * center| ≤
         B * fullSelectedDeviation T Q m base sel fixed D E t z u center := by
   …

   Mentions: OAI.DilutedSpinGlass.FullRootState, OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedTreeScore, OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedTreeMean, OAI.DilutedSpinGlass.HeterogeneousMarks.fullSelectedDeviation