OAI/Combinatorics/Progressions/Estimates/FastHorizontalFactorization.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NilpotentLieFiltration.realLayerOneLieSection line 17
  2. theorem OAI.Erdos3.NilpotentLieFiltration.realLayerOneLieSection_rightInverse line 21
  3. theorem OAI.Erdos3.NilpotentLieFiltration.realLayerOneLieSection_coordinate line 25
  4. theorem OAI.Erdos3.NilpotentLieFiltration.realLayerOneLieSection_coordinate_zero line 31
  5. theorem OAI.Erdos3.NilpotentLieFiltration.realLayerOneLieSection_norm line 36
  6. theorem OAI.Erdos3.NilpotentLieFiltration.realLayerOneLieSection_grid line 41
  7. def OAI.Erdos3.NilpotentLieFiltration.layerOnePolynomialCorrection line 49
  8. theorem OAI.Erdos3.NilpotentLieFiltration.layerOnePolynomialCorrection_log line 53
  9. theorem OAI.Erdos3.NilpotentLieFiltration.layerOnePolynomialCorrection_horizontal line 57
  10. theorem OAI.Erdos3.NilpotentLieFiltration.layerOnePolynomialCorrection_constant line 64
  11. theorem OAI.Erdos3.NilpotentLieFiltration.layerOnePolynomialCorrection_slow line 69
  12. theorem OAI.Erdos3.NilpotentLieFiltration.layerOnePolynomialCorrection_grid line 80
  13. def OAI.Erdos3.NilpotentLieFiltration.realLayerOneCorrection line 113
  14. theorem OAI.Erdos3.NilpotentLieFiltration.realLayerOneCorrection_realize line 117
  15. theorem OAI.Erdos3.NilpotentLieFiltration.realLayerOneCorrection_log line 122
  16. theorem OAI.Erdos3.NilpotentLieFiltration.realLayerOneCorrection_slow line 129
  17. theorem OAI.Erdos3.NilpotentLieFiltration.realLayerOneCorrection_grid line 138
  18. theorem OAI.Erdos3.NilpotentLieFiltration.realLayerOneProjection_coordinate line 148
  19. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedLogDerivative_constant_unit line 154
  20. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientDirectionMap_horizontal_unit line 167
  21. theorem OAI.Erdos3.NilpotentLieFiltration.realLayerOneCorrection_horizontal_derivative line 187
  22. theorem OAI.Erdos3.VectorPolynomial.homogeneous_one_eq_linearPolynomial line 212
  23. theorem OAI.Erdos3.NilpotentLieFiltration.realLayerOneLieSection_of_grade line 229
  24. theorem OAI.Erdos3.NilpotentLieFiltration.homogeneous_one_eq_realLayerOneCorrection_log line 243
  25. def OAI.Erdos3.NilpotentLieFiltration.layerOneGradedMap line 275
  26. theorem OAI.Erdos3.NilpotentLieFiltration.layerOneGradedMap_mk line 279
  27. theorem OAI.Erdos3.NilpotentLieFiltration.realLayerOneGradedMap_mk line 295
  28. theorem OAI.Erdos3.NilpotentLieFiltration.realLayerOneGradedMap_section line 304
  29. def OAI.Erdos3.NilpotentLieFiltration.layerOneGradedSubmodule line 312
  30. theorem OAI.Erdos3.NilpotentLieFiltration.mem_realLayerOneGradedSubmodule line 316
  31. theorem OAI.Erdos3.NilpotentLieFiltration.mem_realLayerOneGradedSubmodule_mk line 323
  32. theorem OAI.Erdos3.NilpotentLieFiltration.realLayerOneCorrection_mem_pointwise line 345
  33. theorem OAI.Erdos3.NilpotentLieFiltration.pointwise_horizontal_coefficient_mem line 364
  34. theorem OAI.Erdos3.NilpotentLieFiltration.pointwise_horizontal_derivative_mem line 378
  35. def OAI.Erdos3.NilpotentLieFiltration.realFastCoefficientDirectionMap line 403
  36. theorem OAI.Erdos3.NilpotentLieFiltration.realFastCoefficientDirectionMap_mul line 415
  37. theorem OAI.Erdos3.NilpotentLieFiltration.realFastCoefficientDirectionMap_triple line 427
  38. theorem OAI.Erdos3.NilpotentLieFiltration.realFastCoefficient_remove_derivative line 460
  39. theorem OAI.Erdos3.NilpotentLieFiltration.realFastCoefficient_remove_lifts line 479
  40. theorem OAI.Erdos3.NilpotentLieFiltration.realFastCoefficient_remove_horizontal_lifts line 491
  41. def OAI.Erdos3.NilpotentLieFiltration.realPointwisePolynomialSubgroup line 524
  42. theorem OAI.Erdos3.NilpotentLieFiltration.mem_realPointwisePolynomialSubgroup line 529
  43. theorem OAI.Erdos3.NilpotentLieFiltration.realLayerOneCorrection_mem_pointwiseSubgroup line 538
  44. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedReducedRealSymbolHom_coord line 558
  45. theorem OAI.Erdos3.NilpotentLieFiltration.realPointwisePolynomialSubgroup_le_fast line 566
  46. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedCoefficientBound_inv line 592
  47. theorem OAI.Erdos3.NilpotentLieFiltration.realFastCoefficientAction_symm line 601
  48. theorem OAI.Erdos3.NilpotentLieFiltration.fastCoefficientAdjoint_norm_bound line 609
  49. theorem OAI.Erdos3.NilpotentLieFiltration.fastCoefficientDirection_norm_bound line 641
  50. def OAI.Erdos3.NilpotentLieFiltration.realFastLayerOneCorrection line 692
  51. theorem OAI.Erdos3.NilpotentLieFiltration.realFastLayerOneCorrection_horizontal line 698
  52. theorem OAI.Erdos3.NilpotentLieFiltration.realFastLayerOneCorrection_slow line 706
  53. theorem OAI.Erdos3.NilpotentLieFiltration.realFastLayerOneCorrection_grid line 714
  54. theorem OAI.Erdos3.NilpotentLieFiltration.realFast_horizontal_normalization line 723
  55. theorem OAI.Erdos3.NilpotentLieFiltration.realFast_bounded_horizontal_normalization line 823
  56. theorem OAI.Erdos3.NilpotentLieFiltration.realFast_controlled_horizontal_factorization line 896