OAI/Combinatorics/Progressions/Estimates/PetalComparisonTree.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.realificationLieSubalgebra line 18
  2. theorem OAI.Erdos3.realificationLieSubalgebra_toSubmodule line 21
  3. theorem OAI.Erdos3.realificationLieHom_incl_injective line 24
  4. theorem OAI.Erdos3.rational_inclusion_mem_realificationLieSubalgebra_iff line 30
  5. def OAI.Erdos3.NilpotentLieBCHGroup.realificationSubgroup line 38
  6. theorem OAI.Erdos3.NilpotentLieBCHGroup.realificationMap_incl_injective line 42
  7. theorem OAI.Erdos3.NilpotentLieBCHGroup.realificationMap_incl_mem line 50
  8. theorem OAI.Erdos3.NilpotentLieBCHGroup.realificationMap_incl_range line 57
  9. theorem OAI.Erdos3.NilpotentLieBCHGroup.realification_subgroup_comap_incl line 69
  10. theorem OAI.Erdos3.lieSubalgebra_mem_iInf line 110
  11. theorem OAI.Erdos3.real_baseChange_ker line 116
  12. theorem OAI.Erdos3.real_baseChange_pi line 122
  13. theorem OAI.Erdos3.real_baseChange_iInf line 130
  14. theorem OAI.Erdos3.realificationLieSubalgebra_iInf line 157
  15. def OAI.Erdos3.MultidegreeLieFiltration.realWeightedGroupInclusion line 185
  16. theorem OAI.Erdos3.MultidegreeLieFiltration.realWeightedGroupInclusion_injective line 191
  17. def OAI.Erdos3.MultidegreeLieFiltration.realifiedWeightedOrbit line 198
  18. theorem OAI.Erdos3.MultidegreeLieFiltration.realifiedWeightedOrbit_eval line 207
  19. theorem OAI.Erdos3.MultidegreeLieFiltration.exists_real_normalized_frozen_orbit line 221
  20. theorem OAI.Erdos3.realification_sup line 249
  21. theorem OAI.Erdos3.real_four_projection line 263
  22. theorem OAI.Erdos3.real_four_single line 270
  23. theorem OAI.Erdos3.real_four_alternating line 282
  24. theorem OAI.Erdos3.mem_realified_four_product_iff line 288
  25. theorem OAI.Erdos3.realification_fourCommonModulo line 299
  26. theorem OAI.Erdos3.realification_fourBalancedDependent line 319
  27. theorem OAI.Erdos3.realification_fourRefinedRelation line 338
  28. theorem OAI.Erdos3.realification_fourPetalSpace line 349
  29. def OAI.Erdos3.NilpotentLieFiltration.symbolPointwiseSubalgebra line 385
  30. theorem OAI.Erdos3.NilpotentLieFiltration.mem_symbolPointwiseSubalgebra_iff line 389
  31. theorem OAI.Erdos3.NilpotentLieFiltration.mem_symbolPointwiseSubalgebra_iff_values line 394
  32. theorem OAI.Erdos3.NilpotentLieFiltration.gradedSymbolPolynomial_block_coefficient line 401
  33. theorem OAI.Erdos3.NilpotentLieFiltration.symbolPointwiseSubalgebra_blockInvariant line 426
  34. def OAI.Erdos3.petalComparisonSpace line 450
  35. theorem OAI.Erdos3.mem_petalComparisonSpace line 455
  36. theorem OAI.Erdos3.petalComparisonSpace_decompose line 458
  37. theorem OAI.Erdos3.petalComparisonSpace_le_pi line 472
  38. theorem OAI.Erdos3.real_pair_projection line 493
  39. theorem OAI.Erdos3.realification_petalComparisonSpace line 500
  40. theorem OAI.Erdos3.realification_map line 530
  41. theorem OAI.Erdos3.realificationLieSubalgebra_map line 542
  42. theorem OAI.Erdos3.toLin_baseChange_coordinates line 550
  43. def OAI.Erdos3.NilpotentLieFiltration.symbolSubalgebraQuotientMap line 576
  44. theorem OAI.Erdos3.NilpotentLieFiltration.symbolPointwiseSubalgebra_eq_ker line 580
  45. theorem OAI.Erdos3.NilpotentLieFiltration.symbolSubalgebraQuotientMap_real_coefficient line 602
  46. theorem OAI.Erdos3.NilpotentLieFiltration.mem_real_symbolPointwiseSubalgebra_iff_coefficients line 611
  47. theorem OAI.Erdos3.NilpotentLieFiltration.mem_real_symbolPointwiseSubalgebra_iff_values line 635
  48. theorem OAI.Erdos3.NilpotentLieFiltration.symbolPointwiseSubalgebra_iInf line 643
  49. def OAI.Erdos3.pairDifferenceFunctional line 664
  50. theorem OAI.Erdos3.pairDifferenceFunctional_apply line 667
  51. theorem OAI.Erdos3.petalComparisonSpace_top_tree line 672