OAI/Combinatorics/Progressions/Estimates/UniformControlledNativeExternalNetsOfRecovery.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.positiveImageExtension line 18
  2. theorem OAI.Erdos3.positiveImageExtension_unit_interval line 22
  3. theorem OAI.Erdos3.positiveImageExtension_norm_le_one line 28
  4. theorem OAI.Erdos3.positiveImageExtension_lipschitz line 31
  5. theorem OAI.Erdos3.positiveImageExtension_eq line 38
  6. theorem OAI.Erdos3.positiveImageExtension_nonexpansive line 49
  7. theorem OAI.Erdos3.positiveImageExtension_bound_of_reconstruction line 64
  8. def OAI.Erdos3.positiveImageSlice line 91
  9. theorem OAI.Erdos3.positiveImageSlice_lipschitz line 94
  10. theorem OAI.Erdos3.positiveImageSlice_eq line 101
  11. theorem OAI.Erdos3.positiveImageSlice_parameter_bound line 107
  12. theorem OAI.Erdos3.exists_stable_positive_reconstruction line 131
  13. theorem OAI.Erdos3.positiveImageExtension_reconstructs_of_positiveImageSlice_eq line 170
  14. theorem OAI.Erdos3.exists_lipschitz_reconstruction_of_positiveImageSlice_eq line 177
  15. theorem OAI.Erdos3.exists_external_test_net line 193
  16. def OAI.Erdos3.NilpotentLieFiltration.adaptedPolynomialRealValueHom line 263
  17. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedPolynomialRealValueHom_coord line 267
  18. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedPolynomialRealValueHom_constant line 272
  19. theorem OAI.Erdos3.RationalFilteredNilmanifold.lattice_factorization_quotient line 285
  20. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.evalReal_of_lattice_factorization line 304
  21. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.eval_of_lattice_factorization line 315
  22. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.observable_change_left line 345
  23. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.observable_freeze_factors line 360
  24. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.eval_freeze_of_lattice_factorization line 372
  25. theorem OAI.Erdos3.RationalFilteredNilmanifold.frozen_observable_change_left line 410
  26. theorem OAI.Erdos3.RationalFilteredNilmanifold.frozen_observable_variation line 429
  27. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_frozen_external_test_net line 453
  28. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_controlled_native_external_net line 502
  29. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_uniform_controlled_native_external_nets line 590
  30. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_uniform_controlled_native_external_nets_of_recovery line 663