OAI/Combinatorics/Progressions/Estimates/NativeMarkedFreezingPhysicalData.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.RationalFilteredNilmanifold.nativeMarkedFreezingExponent line 12
2. theorem OAI.Erdos3.RationalFilteredNilmanifold.nativeMarkedFreezingExponent_ge_two line 16
3. def OAI.Erdos3.RationalFilteredNilmanifold.nativeMarkedFreezingPhysicalParameter line 21
4. theorem OAI.Erdos3.RationalFilteredNilmanifold.nativeMarkedFreezingPhysicalParameter_bounds line 24
5. structure OAI.Erdos3.RationalFilteredNilmanifold.NativeMarkedFreezingPhysicalData line 49
6. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_nativeMarkedFreezingPhysicalData line 69