OAI/Combinatorics/Progressions/Estimates/AllocatedSlicedDiscreteIdeal.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedSlicedPhysicalEndpointIdeal line 38
  2. def OAI.Erdos3.VectorPolynomial.allocatedSlicedPhysicalJetIdeal line 42
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedPhysicalEndpointIdeal_measurable line 45
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedPhysicalJetIdeal_measurable line 51
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedPhysicalEndpointIdeal_probability line 56
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedPhysicalJetIdeal_probability line 68
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedPhysicalJetIdeal_test line 80
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedPhysicalJetIdeal_uniform_bounds line 130
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedPhysicalJetIdeal_zero_off_ball line 160
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedLongJetProxy_uniform_l1 line 218
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedPhysicalJetIdeal_normalized_sites line 295
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedLongJetProxy_output_bounds line 364
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedLongJetProxy_zero_off_ball line 378
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedPhysicalJetIdeal_normalized_coordinates line 423
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedPhysicalJetIdeal_cutoff line 436
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedLongProfile_integrable line 496
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedLongJetProxy_residue_l1 line 563
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedDiscreteIdeal_l1 line 681