OAI/Combinatorics/Progressions/Estimates/NativeFrozenComparison.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NativePolynomialOrbitFactors.middle_model_orbit_normalized line 21
  2. structure OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization line 49
  3. def OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.mono line 76
  4. theorem OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.spaceMap_eval line 82
  5. theorem OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.inclusion_mem_top line 89
  6. theorem OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.spaceMap_top_smul line 97
  7. def OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.pullTest line 120
  8. theorem OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.pullTest_eval line 132
  9. theorem OAI.Erdos3.NativePolynomialOrbitFactors.FrozenMiddleRealization.pullTest_complexity line 137
  10. theorem OAI.Erdos3.exists_native_frozen_middle_realization line 159
  11. theorem OAI.Erdos3.exists_fixed_model_frozen_comparison line 228
  12. theorem OAI.Erdos3.RationalFilteredNilmanifold.frozen_refiltered_group_action line 314
  13. theorem OAI.Erdos3.exists_native_frozen_comparison line 345