OAI/Combinatorics/Progressions/Estimates/AllocatedWholeProfileEnvelope.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.booleanJointLogEnvelope line 13
  2. def OAI.Erdos3.booleanParameterLogEnvelope line 16
  3. def OAI.Erdos3.booleanRegularizationLogEnvelope line 19
  4. theorem OAI.Erdos3.booleanJointLogEnvelope_nonneg line 25
  5. theorem OAI.Erdos3.jointBooleanLogs_le_envelope line 31
  6. theorem OAI.Erdos3.exists_physicalIdealLogs_dimension_bound line 59
  7. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_active_site_probability_majorant line 246
  8. def OAI.Erdos3.VectorPolynomial.fullBooleanRowSetFintype line 312
  9. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_active_site_uniform_majorant line 363
  10. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_active_site_uniform_sampled_error line 452
  11. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_active_site_sampled_error line 566
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedBlock_card_sum_le_variables line 673
  13. def OAI.Erdos3.VectorPolynomial.allocatedBooleanLogDimension line 686
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedBooleanLogDimension_bounds line 692
  15. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedPhysicalIdealLogs_bound line 713
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedWholeProfile_reference_envelope_mass line 800