OAI/Combinatorics/Progressions/Linear/NativeMarkedKernelRepresentatives.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.basisMatrixKernelEquiv line 19
  2. theorem OAI.Erdos3.basisMatrixKernelEquiv_repr line 34
  3. theorem OAI.Erdos3.exists_bounded_linearMap_kernel_basis line 40
  4. theorem OAI.Erdos3.exists_bounded_lie_kernel_basis line 67
  5. theorem OAI.Erdos3.exists_bounded_lie_kernel_subalgebra_basis line 77
  6. theorem OAI.Erdos3.exists_lie_kernel_basis_exp_height line 87
  7. theorem OAI.Erdos3.exists_lie_kernel_subalgebra_basis_logHeight line 103
  8. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_topLayer_basis_logHeight line 132
  9. def OAI.Erdos3.markedKernelCommonHeight line 149
  10. theorem OAI.Erdos3.markedKernelCommonHeight_pos line 152
  11. theorem OAI.Erdos3.markedKernelCommonHeight_le_exp line 156
  12. theorem OAI.Erdos3.rationalHeightLE_markedKernelCommonHeight line 160
  13. theorem OAI.Erdos3.exists_marked_kernel_basis_commonHeight line 177
  14. theorem OAI.Erdos3.exists_marked_kernel_basis_commonHeight_of_dim line 189
  15. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_nativeTopMarkKernel_spanning_budget line 211
  16. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_native_marked_kernel_representatives line 280