OAI/Combinatorics/ContingencyTables/Rooted/TreeExteriorPositions.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The narrow exterior tree intervals contain fewer than 2 gamma b positions

  1. lemma OAI.ContingencyTables.TreeExteriorPositions.positive_integer_positions line 18
  2. def OAI.ContingencyTables.TreeExteriorPositions.positions line 52
  3. theorem OAI.ContingencyTables.TreeExteriorPositions.card_positions_le line 59

    Source documentation

    Strict exterior distances avoid an additive rounding error even when gamma*b is smaller than one.

    theorem card_positions_le (ell : ℤ) (b U : ℕ) (delta : ℝ) (hd : 0 < delta) :
    ((positions ell b U delta).card:ℝ) ≤ 2*delta := by
…

    Mentions: OAI.ContingencyTables.TreeExteriorPositions.positions