OAI/Combinatorics/Progressions/Estimates/TensorSquarePairComparison.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NativeMultidegreeNilcharacter.rationalDilation line 20
  2. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.rationalDilation_eval_rescaled line 23
  3. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_quadratic_integer_translation_equivalence line 44
  4. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.half_dilation_integer_representative line 85
  5. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_half_dilation_equivalence line 97
  6. theorem OAI.Erdos3.norm_unit_pair_replacement_error line 176
  7. def OAI.Erdos3.NativeMultidegreeNilcharacter.halfDilationExchangeCorrection line 214
  8. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.halfDilationExchangeCorrection_pointwise_error line 222
  9. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.halfDilationExchangeCorrection_mean_error line 245
  10. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.halfDilationExchangeCorrection_norm line 276
  11. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_halfDilationExchangeCorrection_expansion line 308
  12. def OAI.Erdos3.NativeMultidegreeNilcharacter.tensorSquareExchangeCorrection line 396
  13. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.tensorSquare_antisymmetricKernel line 402
  14. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.tensorSquareExchangeCorrection_norm line 411
  15. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.tensorSquareExchangeCorrection_mean_error line 420
  16. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_tensorSquareExchangeCorrection_expansion line 456
  17. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.explicit_half_root_exchange_mean_error line 468
  18. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_explicit_half_root_exchange_expansion line 487