OAI/Combinatorics/Progressions/Linear/KernelScaleIndependence.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.realKernelJet_exists_minor line 13
  2. theorem OAI.Erdos3.realKernelJet_exists_controlled_pivot line 49
  3. theorem OAI.Erdos3.monomialScale_le_uniform_pow line 70
  4. theorem OAI.Erdos3.kernelCoefficientScale_lower line 83
  5. theorem OAI.Erdos3.boundedDegreeIntegerJetMatrix_entry_bound line 91
  6. theorem OAI.Erdos3.normalizedIntegerColumns_submatrix line 118
  7. theorem OAI.Erdos3.integerPivot_det_ne_zero_of_normalized line 127
  8. theorem OAI.Erdos3.normalizedBoundedIntegerJet_exists_pivot line 136
  9. def OAI.Erdos3.remainingMatrixColumns line 177
  10. theorem OAI.Erdos3.selectedMatrix_fromCols line 180
  11. theorem OAI.Erdos3.selectedMatrix_full_image line 187
  12. theorem OAI.Erdos3.selectedMatrix_smooth_law line 193
  13. theorem OAI.Erdos3.normalized_remainingMatrixColumns line 206
  14. theorem OAI.Erdos3.normalized_remainingMatrixColumns_norm line 216
  15. def OAI.Erdos3.normalizedScalarKernelJet line 231
  16. theorem OAI.Erdos3.goodScalarKernelTuple_jet_pivot line 237
  17. def OAI.Erdos3.scalarKernelIntegerJet line 260
  18. theorem OAI.Erdos3.normalizedScalarKernelJet_eq line 265
  19. theorem OAI.Erdos3.goodScalarKernelTuple_integer_jet_pivot line 274
  20. def OAI.Erdos3.kernelJetCoefficientScale line 301
  21. theorem OAI.Erdos3.kernelJetCoefficientScale_pos line 304
  22. theorem OAI.Erdos3.kernelJetCoefficientScale_lower line 309
  23. theorem OAI.Erdos3.normalized_scalarKernel_pivot line 314
  24. theorem OAI.Erdos3.goodScalarKernelTuple_fixed_jet_pivot line 326
  25. theorem OAI.Erdos3.fromCols_left_pivot line 348
  26. theorem OAI.Erdos3.scalarKernelJet_extended_period line 354
  27. theorem OAI.Erdos3.scalarKernelJet_extended_index line 365
  28. def OAI.Erdos3.scalarKernelFixedPivot line 375
  29. def OAI.Erdos3.scalarKernelFixedFree line 386
  30. theorem OAI.Erdos3.scalarKernel_pivot_scale_independent line 394
  31. theorem OAI.Erdos3.scalarKernel_free_scale_independent line 411