OAI/Combinatorics/DiscreteConvexity/DensityConstants.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Symbolic constants for the original-density argument

Only the small factor 32 = 2^5 is evaluated. The number of rows and the final tuple length remain symbolic powers throughout the construction.

  1. theorem OAI.TalagrandDiscreteConvexity.density_rows_gt_one line 20
  2. theorem OAI.TalagrandDiscreteConvexity.density_rows_pos line 23
  3. theorem OAI.TalagrandDiscreteConvexity.density_tuple_count line 26
  4. theorem OAI.TalagrandDiscreteConvexity.density_tuple_count_real line 29
  5. theorem OAI.TalagrandDiscreteConvexity.density_failure_budget line 35

    Source documentation

    A density loss of at most 1 / (32 L) spends at most 1 / 32 across rows.

    theorem density_failure_budget {L a : ℝ} (hL : 0 < L)
    (ha : 1 - 1 / (32 * L) ≤ a) : L * (1 - a) ≤ 1 / 32 := by
…