OAI/Combinatorics/SquareDifference/Endpoint.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SquareDifference.NatSquareFree line 13
  2. def OAI.SquareDifference.natIndicator line 16
  3. lemma OAI.SquareDifference.natIndicator_bound line 18
  4. lemma OAI.SquareDifference.natIndicator_nonneg line 22
  5. lemma OAI.SquareDifference.natIndicator_vanish line 26
  6. lemma OAI.SquareDifference.sum_natIndicator line 30
  7. def OAI.SquareDifference.squareChild line 37
  8. lemma OAI.SquareDifference.squareChild_sub line 40
  9. lemma OAI.SquareDifference.squareChild_free line 42
  10. lemma OAI.SquareDifference.squareChild_indicator line 51
  11. def OAI.SquareDifference.setFunctional line 64
  12. lemma OAI.SquareDifference.setFunctional_nonneg line 67
  13. lemma OAI.SquareDifference.setFunctional_density line 70