OAI/Combinatorics/BalancedRyser/Incidence/AffineMomentAlgebraLemmas.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.MomentAlgebra.centered_sum_expansion line 13
  2. theorem OAI.Balanced.MomentAlgebra.affine_centered_sum line 22
  3. theorem OAI.Balanced.MomentAlgebra.affine_variance_bound line 31
  4. theorem OAI.Balanced.MomentAlgebra.affine_centered_sum_le line 39
  5. theorem OAI.Balanced.MomentAlgebra.directional_variance_sum line 47
  6. theorem OAI.Balanced.MomentAlgebra.directional_variance_le_count line 55
  7. theorem OAI.Balanced.MomentAlgebra.directional_variance_bounds line 59
  8. theorem OAI.Balanced.StabilityAffineArithmetic.auxiliary_degree_lt_quarter line 71
  9. theorem OAI.Balanced.StabilityAffineArithmetic.tangent_margin line 80
  10. theorem OAI.Balanced.StabilityAffineArithmetic.degree_gap line 90
  11. theorem OAI.Balanced.StabilityAffineArithmetic.size_lt_second_alternative line 96
  12. theorem OAI.Balanced.StabilityArithmetic.delta_pos line 111
  13. theorem OAI.Balanced.StabilityArithmetic.hole_bound line 115
  14. theorem OAI.Balanced.StabilityArithmetic.reduction_bounds line 125
  15. theorem OAI.Balanced.StabilityFinalArithmetic.rounded_size_bound line 163
  16. theorem OAI.Balanced.StabilityFinalArithmetic.collinear_lower_bound line 182
  17. theorem OAI.Balanced.StabilityFinalArithmetic.collinear_lower_bound_of_source_bounds line 211