OAI/Combinatorics/Progressions/Estimates/NativeOptionFixedSourceQuotientMarkStrong.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos3.RationalFilteredNilmanifold.AdaptedModelData line 17
  2. def OAI.Erdos3.RationalFilteredNilmanifold.AdaptedModelData.model line 30
  3. theorem OAI.Erdos3.RationalFilteredNilmanifold.AdaptedModelData.model_layers line 33
  4. theorem OAI.Erdos3.RationalFilteredNilmanifold.AdaptedModelData.original_dist_le line 39
  5. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_adapted_model_data line 54
  6. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_prescribed_adapted_model line 84
  7. structure OAI.Erdos3.RationalFilteredNilmanifold.AdaptedMapGeometryData line 133
  8. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_native_adapted_map_geometry line 159
  9. structure OAI.Erdos3.RationalFilteredNilmanifold.FixedSourceAdaptedMarkGeometryData line 232
  10. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_native_fixedSource_adapted_mark_geometry line 253
  11. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionOriginalObservable_unit_interval line 319
  12. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionOriginalObservable_member_net line 328
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionOriginalObservable_member_nets line 339
  14. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionOriginalObservable_adapted_unit_interval line 354
  15. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionOriginalObservable_adapted_member_nets line 364
  16. def OAI.Erdos3.RationalFilteredNilmanifold.optionOriginalAdaptedLipschitzBound line 378
  17. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionOriginalAdaptedLipschitzBound_le_exp line 387
  18. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionOriginalObservable_lipschitz line 419
  19. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionOriginalObservable_adapted_lipschitz line 430
  20. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionOriginalObservable_adapted_lipschitz_of_logHeight line 465
  21. def OAI.Erdos3.RationalFilteredNilmanifold.nativeOptionFixedSourceMarkExponent line 491
  22. theorem OAI.Erdos3.RationalFilteredNilmanifold.nativeOptionFixedSourceMarkExponent_ge_two line 494
  23. def OAI.Erdos3.RationalFilteredNilmanifold.nativeOptionFixedSourceQuotientMarkInput line 498
  24. theorem OAI.Erdos3.RationalFilteredNilmanifold.nativeOptionFixedSourceQuotientMarkInput_bounds line 501
  25. theorem OAI.Erdos3.RationalFilteredNilmanifold.nativeOptionFixedSourceQuotientMark_mem_layer line 532
  26. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_nativeOptionFixedSourceQuotientMarkGeometry line 555
  27. theorem OAI.Erdos3.RationalFilteredNilmanifold.optionAdaptedModel_layers line 609
  28. theorem OAI.Erdos3.RationalFilteredNilmanifold.nativeOptionFixedSourceQuotientMark_layer_surjective line 655
  29. theorem OAI.Erdos3.RationalFilteredNilmanifold.nativeOptionFixedSourceQuotientMark_adaptedTarget_layer_surjective line 685