OAI/Probability/DilutedSpin/DictionaryPalm.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.insertedTreeScore_selected line 14
2. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.fullInserted_select_type line 48

   Source documentation

   The exact mass of a selected type emerges from the full law, with its site average independent of the unchanged complete reservoir.

   lemma fullInserted_select_type
       (hb : ∀ k y, Measurable (fun z : RootPath Y M × RootPath X k => base z.1 k z.2 y))
       {B : ℝ} (hB : 0 ≤ B) (hf : ∀ x, |f x| ≤ B)
       (hE : ∀ i x y, |E i x y| ≤ 1)
       (hA : ∀ i x y, 1/2 ≤ 1+t*D i x y+u*E i x y) :
       (∫ z, fullInsertedTreeScore (ν.prod τ) S a T Q (fun l => m l.succ) base
         (selectedFactor (fun i => decide (i.1 = j)) fixed D E t u)
         (selectedNumerator (fun i => decide (i.1 = j)) E) f z ∂fullRootLaw ξ μ (ν.prod τ) r s) =
         ν.real {j} * externalAverage ξ μ (ν.prod τ) (τ.map (fun z => (j,z))) r s S a T Q m base
           (selectedFactor (fun i => decide (i.1 = j)) fixed D E t u) D E f t u := by
   …

   Mentions: OAI.DilutedSpinGlass.RootPath, OAI.DilutedSpinGlass.HeterogeneousMarks.fullInsertedTreeScore, OAI.DilutedSpinGlass.HeterogeneousMarks.selectedFactor, OAI.DilutedSpinGlass.HeterogeneousMarks.selectedNumerator, OAI.DilutedSpinGlass.fullRootLaw, OAI.DilutedSpinGlass.HeterogeneousMarks.externalAverage