OAI/Combinatorics/Progressions/Estimates/CommonPivotQuotientTop.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NilpotentLieFiltration.prod line 14
  2. theorem OAI.Erdos3.NilpotentLieFiltration.prod_layer line 26
  3. theorem OAI.Erdos3.NilpotentLieFiltration.mem_prod_layer line 30
  4. def OAI.Erdos3.NilpotentLieFiltration.pivotQuotientFiltration line 41
  5. theorem OAI.Erdos3.NilpotentLieFiltration.pivotQuotientFiltration_layer line 45
  6. def OAI.Erdos3.NilpotentLieFiltration.pivotProductQuotientFiltration line 49
  7. theorem OAI.Erdos3.NilpotentLieFiltration.pivotProductQuotientMap_mem_layer line 53
  8. theorem OAI.Erdos3.NilpotentLieFiltration.pivotProductQuotientMap_layer_surjective line 59
  9. theorem OAI.Erdos3.NilpotentLieFiltration.pivotProductQuotientMap_layer_map line 66
  10. theorem OAI.Erdos3.NilpotentLieFiltration.frequency_zero_on_refilteredLayer_of_real line 88
  11. def OAI.Erdos3.NilpotentLieFiltration.commonPivotQuotientFast line 105
  12. theorem OAI.Erdos3.NilpotentLieFiltration.commonFastTop_le_joinedFrequencyTop line 118
  13. theorem OAI.Erdos3.NilpotentLieFiltration.commonFastTop_quotient_le_joinedFrequencyQuotientTop line 128
  14. theorem OAI.Erdos3.NilpotentLieFiltration.commonFastTop_quotient_kernel_eq_zero line 136
  15. theorem OAI.Erdos3.NilpotentLieFiltration.commonPivotQuotientFast_layer_eq line 154
  16. theorem OAI.Erdos3.NilpotentLieFiltration.commonPivotQuotientFast_graded line 166
  17. theorem OAI.Erdos3.NilpotentLieFiltration.commonPivotQuotientFast_top_le line 177
  18. theorem OAI.Erdos3.NilpotentLieFiltration.commonPivotQuotientFast_top_kernel_eq_zero line 186
  19. theorem OAI.Erdos3.NilpotentLieFiltration.commonPivotQuotientFast_graded_top_kernel line 197