OAI/Combinatorics/Progressions/Estimates/RealFirstCoefficientHorizontal.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NilpotentLieFiltration.realAdaptedDirectionalDerivative line 17
  2. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedDirectionalDerivative_polynomial line 22
  3. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedDirectionalDerivative_tensor line 39
  4. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedDirectionalDerivative_bound line 46
  5. def OAI.Erdos3.NilpotentLieFiltration.realAdaptedPolynomialJet line 87
  6. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedPolynomialJet_base line 92
  7. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedPolynomialJet_tangent line 98
  8. def OAI.Erdos3.NilpotentLieFiltration.realAdaptedLogDerivative line 104
  9. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedLogDerivative_tensor line 109
  10. theorem OAI.Erdos3.NilpotentLieFiltration.exists_real_adapted_log_derivative_bound line 124
  11. theorem OAI.Erdos3.VectorPolynomial.directionalDerivative_single line 193
  12. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedLogDerivative_eq_formal line 205
  13. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedLogDerivative_eq_formal line 220
  14. def OAI.Erdos3.NilpotentLieFiltration.realFullPolynomialLie line 232
  15. theorem OAI.Erdos3.NilpotentLieFiltration.realFullPolynomialLie_apply line 237
  16. def OAI.Erdos3.NilpotentLieFiltration.realFullPolynomialHom line 242
  17. theorem OAI.Erdos3.NilpotentLieFiltration.realFullPolynomialHom_coord line 247
  18. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedAdjoint_eq_formal line 251
  19. theorem OAI.Erdos3.NilpotentLieFiltration.realAdapted_derivative_system_to_formal line 257
  20. def OAI.Erdos3.NilpotentLieFiltration.realAdaptedDirectionalTangent line 285
  21. def OAI.Erdos3.NilpotentLieFiltration.realLogDerivativeDirectionMap line 304
  22. theorem OAI.Erdos3.NilpotentLieFiltration.realLogDerivativeDirectionMap_rat line 311
  23. theorem OAI.Erdos3.NilpotentLieFiltration.realLogDerivativeDirectionMap_polynomial line 319
  24. def OAI.Erdos3.NilpotentLieFiltration.realShiftedCoefficientSubmodule line 340
  25. theorem OAI.Erdos3.NilpotentLieFiltration.realShiftedCoefficient_lie_mem line 344
  26. abbrev OAI.Erdos3.NilpotentLieFiltration.RealFirstCoefficientModule line 349
  27. def OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientMap line 353
  28. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientMap_eq_zero_iff line 358
  29. def OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientAdjoint line 363
  30. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientAdjoint_map line 370
  31. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedDirectionalDerivative_mem_first line 378
  32. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedLogDerivative_mem_first line 388
  33. theorem OAI.Erdos3.NilpotentLieFiltration.realLogDerivativeDirectionMap_mem_first line 398
  34. def OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientDirectionMap line 415
  35. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientDirectionMap_rat line 422
  36. def OAI.Erdos3.NilpotentLieFiltration.firstCoefficientRealEquiv line 444
  37. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientRealEquiv_map line 448
  38. def OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientHorizontal line 453
  39. def OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientHorizontalSection line 457
  40. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientHorizontal_section line 461
  41. def OAI.Erdos3.NilpotentLieFiltration.realNormalizedFirstCoefficientMap line 471
  42. theorem OAI.Erdos3.NilpotentLieFiltration.realNormalizedFirstCoefficientMap_range line 475