OAI/Probability/DilutedSpin/SelectedPalm.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.HeterogeneousMarks.selectedNumerator line 13
2. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.selectedNumerator_bound line 19
3. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.selectedTreeScore_sum line 26
4. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.selectedTreeScore_one line 42
5. theorem OAI.DilutedSpinGlass.HeterogeneousMarks.selected_palm line 57

   Source documentation

   Selected score Palm at a fixed physical realization. The whole original root-label reservoir is retained; only one independent label/mark is inserted.

   theorem selected_palm (S : PrescribedTree L) (a : S.Leaf)
       (s : ℝ≥0) (T : KernelTower Ω L) (Q : (i : I) → Fin L → FiniteLaw (A i)) (m : Fin L → ℝ)
       (base : FinitePath Ω L → ℝ) (sel : I → Bool)
       (fixed D E : (i : I) → FinitePath Ω L → FinitePath (A i) L → ℝ)
       (t u : ℝ) (f : (S.Leaf → FinitePath Ω L) → ℝ) {B : ℝ}
       (hf : ∀ x, |f x| ≤ B) (hE : ∀ i x y, |E i x y| ≤ 1)
       (hA : ∀ i x y, 1/2 ≤ selectedFactor sel fixed D E t u i x y) :
       (∫ n : ℕ, ∫ y, selectedTreeScore S a T Q m base (rootArray n y) sel fixed D E t u f
         ∂rootLaw n (fun _ => ν) ∂poissonMeasure s) =
         (s:ℝ) * ∫ n : ℕ, ∫ i, ∫ y,
           insertedTreeScore S a T Q m base (rootArray n y) i
             (selectedFactor sel fixed D E t u) (selectedNumerator sel E) f
   …

   Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.KernelTower, OAI.DilutedSpinGlass.FiniteLaw, OAI.DilutedSpinGlass.FinitePath, OAI.DilutedSpinGlass.HeterogeneousMarks.selectedFactor, OAI.DilutedSpinGlass.HeterogeneousMarks.selectedTreeScore, OAI.DilutedSpinGlass.rootArray, OAI.DilutedSpinGlass.rootLaw, OAI.DilutedSpinGlass.HeterogeneousMarks.insertedTreeScore, OAI.DilutedSpinGlass.HeterogeneousMarks.selectedNumerator