OAI/Probability/DilutedSpin/CompoundSuperposition.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DilutedSpinGlass.probeLow line 11
2. def OAI.DilutedSpinGlass.probeHigh line 12
3. lemma OAI.DilutedSpinGlass.extractionProbe_le_quarter line 14
4. lemma OAI.DilutedSpinGlass.extractionProbe_abs_le_quarter line 20
5. lemma OAI.DilutedSpinGlass.probeLow_pos line 24
6. lemma OAI.DilutedSpinGlass.probeLow_lt_high line 25
7. lemma OAI.DilutedSpinGlass.probeHigh_lt_quarter line 29
8. lemma OAI.DilutedSpinGlass.probe_interval_quarter line 36
9. lemma OAI.DilutedSpinGlass.charFunDual_nnreal_smul line 56
10. lemma OAI.DilutedSpinGlass.charFunDual_add_measure line 61
11. lemma OAI.DilutedSpinGlass.compoundPoisson_superposition line 71

    Source documentation

    Superposition of marked Poisson sums follows solely from equality of the finite intensity measures. No independence of coordinates of a mark is needed.

    lemma compoundPoisson_superposition [CompleteSpace E] (s t : ℝ≥0)
        (μ ν τ : Measure E) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] [IsProbabilityMeasure τ]
        (h : ((s+t:ℝ≥0):ℝ≥0∞) • μ = (s:ℝ≥0∞) • ν+(t:ℝ≥0∞) • τ) :
        compoundPoisson (s+t) μ = compoundPoisson s ν ∗ compoundPoisson t τ := by
    …

    Mentions: OAI.DilutedSpinGlass.compoundPoisson

12. lemma OAI.DilutedSpinGlass.compoundPoisson_add line 87
13. lemma OAI.DilutedSpinGlass.mixture_double_limit line 102