OAI/Combinatorics/Progressions/Estimates/NativeSubspaceFreeModel.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.realify_pairDifferenceFunctional line 11
  2. theorem OAI.Erdos3.pairDifferenceFunctional_eq_piFrequency line 22
  3. def OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.pairedObservable line 39
  4. theorem OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.pairedObservable_unit line 46
  5. theorem OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.pairedObservable_norm line 54
  6. theorem OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.pairedObservable_lipschitz line 59
  7. theorem OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.pairedObservable_vertical line 80
  8. def OAI.Erdos3.RationalFilteredNilmanifold.UnitVerticalObservable.paired line 96
  9. theorem OAI.Erdos3.VectorPolynomial.map_positiveUnivariate line 153
  10. theorem OAI.Erdos3.VectorPolynomial.positiveUnivariate_reconstruct line 157
  11. theorem OAI.Erdos3.NilpotentLieFiltration.exists_positiveUnivariate_orbit_lift line 196
  12. abbrev OAI.Erdos3.SubspaceFreeLift.Alphabet line 244
  13. def OAI.Erdos3.SubspaceFreeLift.weight line 246
  14. theorem OAI.Erdos3.SubspaceFreeLift.weight_pos line 248
  15. abbrev OAI.Erdos3.SubspaceFreeLift.Algebra line 250
  16. def OAI.Erdos3.SubspaceFreeLift.filtration line 252
  17. def OAI.Erdos3.SubspaceFreeLift.generator line 255
  18. def OAI.Erdos3.SubspaceFreeLift.generatorSpan line 258
  19. theorem OAI.Erdos3.SubspaceFreeLift.generatorSpan_le_layer line 261
  20. def OAI.Erdos3.SubspaceFreeLift.coefficientLift line 269
  21. theorem OAI.Erdos3.SubspaceFreeLift.coefficientLift_range line 272
  22. def OAI.Erdos3.SubspaceFreeLift.evaluation line 279
  23. theorem OAI.Erdos3.SubspaceFreeLift.evaluation_generator line 283
  24. theorem OAI.Erdos3.SubspaceFreeLift.evaluation_coefficientLift line 287
  25. def OAI.Erdos3.SubspaceFreeLift.realCoefficientLift line 298
  26. theorem OAI.Erdos3.SubspaceFreeLift.realCoefficientLift_baseChange line 303
  27. theorem OAI.Erdos3.SubspaceFreeLift.realCoefficientLift_mem line 309
  28. theorem OAI.Erdos3.SubspaceFreeLift.realEvaluation_coefficientLift line 320
  29. theorem OAI.Erdos3.SubspaceFreeLift.exists_polynomialOrbit line 332
  30. theorem OAI.Erdos3.SubspaceFreeLift.exists_native_polynomialOrbit line 392
  31. theorem OAI.Erdos3.SubspaceFreeLift.exists_native_pair_orbit line 453
  32. theorem OAI.Erdos3.SubspaceFreeLift.native_pair_observable_eval line 507
  33. theorem OAI.Erdos3.SubspaceFreeLift.alphabet_card_le line 543
  34. theorem OAI.Erdos3.SubspaceFreeLift.exists_native_model line 553