OAI/Probability/DilutedSpin/InsertionStability.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.map_familyLaw_sum line 11
2. lemma OAI.DilutedSpinGlass.map_iid_energy line 31
3. lemma OAI.DilutedSpinGlass.map_compoundRoot_energy line 46

   Source documentation

   The physical recursive Poisson container has exactly the compound-sum energy law, including its independent random count.

   lemma map_compoundRoot_energy (μ : Measure X) [IsProbabilityMeasure μ]
       (V : X → E) (hV : Measurable V) (r : ℝ≥0) :
       Measure.map (fun z : Sigma (RootPath X) => ∑ i, V (rootArray z.1 z.2 i)) (compoundRootLaw μ r) =
         compoundPoisson r (Measure.map V μ) := by
   …

   Mentions: OAI.DilutedSpinGlass.RootPath, OAI.DilutedSpinGlass.rootArray, OAI.DilutedSpinGlass.compoundRootLaw, OAI.DilutedSpinGlass.compoundPoisson

4. lemma OAI.DilutedSpinGlass.FiniteLaw.spinLog_stability line 63
5. lemma OAI.DilutedSpinGlass.UniversalDictionary.reservoirInsertion_lipschitz line 75
6. lemma OAI.DilutedSpinGlass.UniversalDictionary.reservoirTrialLog_lipschitz line 102