OAI/Combinatorics/Progressions/Linear/ControlledProjectionUniformBudget.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.realificationLieSubalgebra_comap line 16
  2. def OAI.Erdos3.NilpotentLieFiltration.realSymbolProjection line 35
  3. theorem OAI.Erdos3.NilpotentLieFiltration.exists_symbolFactorizationIn_projection_pullback line 42
  4. def OAI.Erdos3.RationalFilteredNilmanifold.optionPairProjection line 144
  5. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionPairProjection_true line 151
  6. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionPairProjection_false line 155
  7. theorem OAI.Erdos3.RationalFilteredNilmanifold.pairFrequency_optionPairProjection line 159
  8. theorem OAI.Erdos3.RationalFilteredNilmanifold.realification_optionPairProjection_true line 165
  9. theorem OAI.Erdos3.RationalFilteredNilmanifold.realification_optionPairProjection_false line 173
  10. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionPairProjection_layers line 185
  11. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionPairProjection_layer_surjective line 195
  12. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionPairProjection_piRealOrbit_log line 222
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionPairProjection_jointOrbitSymbol line 261
  14. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionPairProjection_native_logHeight line 299
  15. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionPairProjection_adapted_logHeight line 316
  16. def OAI.Erdos3.NilpotentLieFiltration.controlledProjectionBudget line 344
  17. theorem OAI.Erdos3.NilpotentLieFiltration.controlledSymbolFactorizationAtFast_projection_pullback line 357
  18. theorem OAI.Erdos3.NilpotentLieFiltration.controlledSymbolFactorization_projection_pullback line 407
  19. theorem OAI.Erdos3.NilpotentLieFiltration.controlledProjectionBudget_nonneg line 440
  20. theorem OAI.Erdos3.NilpotentLieFiltration.le_controlledProjectionBudget line 446
  21. theorem OAI.Erdos3.NilpotentLieFiltration.exists_controlledProjectionBudget_power line 455
  22. def OAI.Erdos3.NilpotentLieFiltration.controlledProjectionDimensionInput line 479
  23. theorem OAI.Erdos3.NilpotentLieFiltration.ControlledSymbolFactorizationAtFast.mono line 486
  24. theorem OAI.Erdos3.NilpotentLieFiltration.controlledSymbolFactorizationAtFast_projection_of_dimensions line 503
  25. theorem OAI.Erdos3.NilpotentLieFiltration.le_controlledProjectionDimensionInput line 567
  26. theorem OAI.Erdos3.NilpotentLieFiltration.controlledProjectionDimensionInput_nonneg line 572
  27. theorem OAI.Erdos3.NilpotentLieFiltration.exists_controlledProjectionUniformBudget_power line 576