SiteDegreeTail.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Conditional row variance gives a common degree event

theorem OAI.JointDickman.finiteProbability_markov line 12

Source documentation

Markov's inequality for the finite nonnegative weights used here.

theorem finiteProbability_markov {Ω : Type*} [Fintype Ω]
    (w f : Ω → ℝ) (hw : ∀ x, 0 ≤ w x) (hf : ∀ x, 0 ≤ f x)
    {t : ℝ} (ht : 0 < t) :
    finiteProbability w (fun x => t < f x) ≤ finiteExpectation w f/t := by
…

Mentions: OAI.JointDickman.finiteProbability, OAI.JointDickman.finiteExpectation

theorem OAI.JointDickman.siteRow_degree_tail line 27

Source documentation

The mean is bounded for every row type, but the variance bound is integrated over that type. This is sufficient for the degree tail.

theorem siteRow_degree_tail {ι A : Type*} [Fintype ι] [DecidableEq ι] [Fintype A]
    (p : ι → A → ℝ) (hp : ∀ i a, 0 ≤ p i a) (hpone : ∀ i, ∑ a, p i a = 1)
    (K : ι → ι → A → A → ℝ) (hdiag : ∀ i a, K i i a a = 0)
    (i : ι) {C d : ℝ} (hgap : C < d)
    (hmean : ∀ a, |siteRowMean p K i a| ≤ C) :
    finiteProbability (siteProductMass p) (fun x => d < siteRowSum K i x) ≤
      siteRowSquareMass p K i/(d-C)^2 := by
…

Mentions: OAI.JointDickman.siteRowMean, OAI.JointDickman.finiteProbability, OAI.JointDickman.siteRowSum, OAI.JointDickman.siteRowSquareMass

theorem OAI.JointDickman.siteDegree_bad_probability line 48

Source documentation

Union over all rows pays only the number of positions.

theorem siteDegree_bad_probability {ι A : Type*} [Fintype ι] [DecidableEq ι] [Fintype A]
    (p : ι → A → ℝ) (hp : ∀ i a, 0 ≤ p i a) (hpone : ∀ i, ∑ a, p i a = 1)
    (K : ι → ι → A → A → ℝ) (hdiag : ∀ i a, K i i a a = 0)
    {C d q : ℝ} (hgap : C < d)
    (hmean : ∀ i a, |siteRowMean p K i a| ≤ C)
    (hsquare : ∀ i, siteRowSquareMass p K i ≤ q) :
    finiteProbability (siteProductMass p) (fun x => ¬ ∀ i, siteRowSum K i x ≤ d) ≤
      (Fintype.card ι : ℝ)*q/(d-C)^2 := by
…

Mentions: OAI.JointDickman.siteRowMean, OAI.JointDickman.siteRowSquareMass, OAI.JointDickman.finiteProbability, OAI.JointDickman.siteRowSum