RankSelection.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.HyperbolicObstruction.FiniteLaw.bernoulliProduct_sum_expect line 12
lemma OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.expect_join line 31
lemma OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.rank_bad_join_bound line 47

theorem OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.exists_tables_of_estimate line 60

Source documentation

Simultaneous selection with the genuine bounded-rank event, not independent new copies of the arrays used for sampling.

theorem exists_tables_of_estimate {J : Type*} [Fintype J]
    (T : J → ConditionalTest) (M n : ℕ) {α β δ ε τ : ℝ}
    (ha : 0 ≤ α) (hb : 7*α ≤ β) (hd : 0 ≤ δ)
    (hsmall : ∀ j, ((T j).k+1:ℝ)*(β+90*δ) ≤ 1/2)
    (hN : ∀ j, (T j).threshold ≤ Fintype.card (SymmetricAlphabet n))
    (hε0 : 0 < ε) (hε1 : ε < 1) (hτ0 : 0 < τ) (hτ2 : τ ≤ 2)
    (hest : (∑ j, (T j).rate (Fintype.card (SymmetricAlphabet n))) +
      ε*(60*(Fintype.card (SymmetricAlphabet n):ℝ)^2*
        Real.exp (-τ^2*(Fintype.card (SymmetricAlphabet n):ℝ)^(1-δ)/4) +
        rankRate M α β δ (Fintype.card (SymmetricAlphabet n))) < ε) :
    ∃ (w : TableModel.Entry (A := SymmetricAlphabet n) rowSupport → Bool)
…

Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.ConditionalTest, OAI.HyperbolicObstruction.IncidenceTemplate.SymmetricAlphabet, OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.rankRate, OAI.HyperbolicObstruction.TableModel.Entry, OAI.HyperbolicObstruction.IncidenceTemplate.rowSupport