OAI/Combinatorics/Progressions/Geometry/ProgressionTupleSliceSupport.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.FiniteProbabilityWeights.condition_weight_pos_iff line 14
2. theorem OAI.Erdos3.FiniteProbabilityWeights.pi_weight_pos_component line 21
3. theorem OAI.Erdos3.scalarCubeResidueWeights_cube_support line 32
4. theorem OAI.Erdos3.integerScalarCube_endpoint_normalized_norm_le line 42
5. theorem OAI.Erdos3.affineCubeTuple_norm_le line 58
6. theorem OAI.Erdos3.progressionTuple_norm_le line 73