OAI/Combinatorics/Progressions/Estimates/RealSymbolRepresentativeSplitting.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualAdjoint_smul_real line 15
  2. def OAI.Erdos3.NilpotentLieBCHGroup.dualAdjointRealLinearEquiv line 26
  3. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualAdjointRealLinearEquiv_apply line 30
  4. theorem OAI.Erdos3.NilpotentLieBCHGroup.dualAdjoint_real_mem_of_invariant line 46
  5. def OAI.Erdos3.NilpotentLieBCHGroup.invariantRealAdjoint line 52
  6. theorem OAI.Erdos3.NilpotentLieBCHGroup.invariantRealAdjoint_coe line 63
  7. theorem OAI.Erdos3.NilpotentLieBCHGroup.invariantRealAdjoint_map_submodule line 68
  8. def OAI.Erdos3.NilpotentLieBCHGroup.invariantRealAdjointQuotient line 81
  9. theorem OAI.Erdos3.NilpotentLieBCHGroup.invariantRealAdjointQuotient_mk line 89
  10. theorem OAI.Erdos3.realification_ideal_intertwining line 110
  11. def OAI.Erdos3.realIdealAdjoint line 127
  12. theorem OAI.Erdos3.realIdealAdjoint_inclusion line 135
  13. theorem OAI.Erdos3.realIdealMap_adjoint line 148
  14. def OAI.Erdos3.NilpotentLieFiltration.realSymbolRepresentative line 195
  15. def OAI.Erdos3.NilpotentLieFiltration.realSymbolOfPolynomial line 208
  16. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolRepresentative_coefficient line 214
  17. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolRepresentative_coefficient_of_ne line 226
  18. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolOfPolynomial_coordinate line 237
  19. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolOfPolynomial_representative line 247
  20. theorem OAI.Erdos3.NilpotentLieFiltration.real_mem_layer_iff_basis_coordinates line 255
  21. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolRepresentative_adapted line 261
  22. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolRepresentative_constant line 270
  23. def OAI.Erdos3.NilpotentLieFiltration.realAdaptedSymbolRepresentative line 279
  24. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedSymbolRepresentative_coe line 285
  25. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolOfPolynomial_eq_zero_iff line 289
  26. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolOfPolynomial_eq_iff_symbolMap_eq line 311
  27. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedSymbolRepresentative_symbolMap line 322
  28. theorem OAI.Erdos3.NilpotentLieFiltration.realBasis_mem_layer line 348
  29. theorem OAI.Erdos3.NilpotentLieFiltration.dualAdjoint_realBasis_coordinate line 355
  30. theorem OAI.Erdos3.NilpotentLieFiltration.dualAdjoint_realMatrix_entry line 365
  31. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolRepresentative_slow_coefficients line 389
  32. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolRepresentative_rational_coefficients line 401
  33. def OAI.Erdos3.NilpotentLieFiltration.gradedBasisSplitting line 438
  34. theorem OAI.Erdos3.NilpotentLieFiltration.gradedBasisSplitting_coordinate line 441
  35. theorem OAI.Erdos3.NilpotentLieFiltration.gradedBasisSplitting_real_coordinate line 446
  36. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolRepresentative_coefficient_splitting line 459
  37. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolRepresentative_eq_map line 473
  38. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolRepresentative_eval₂ line 483