OAI/Combinatorics/Progressions/Estimates/PreparedRelativeFinalPower.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.centeredFiniteProbabilityMeasure_ae_centers line 19
  2. theorem OAI.Erdos3.exists_center_with_good_mass line 29
  3. theorem OAI.Erdos3.exists_center_finite_good_event line 51
  4. theorem OAI.Erdos3.exists_center_finite_productive_good_event line 99
  5. theorem OAI.Erdos3.exists_center_finite_productive_good_event_avoiding_residual line 125
  6. theorem OAI.Erdos3.exists_centered_joint_fixed_patch_function line 170
  7. theorem OAI.Erdos3.exists_centered_joint_fixed_patch_function_ae line 232
  8. theorem OAI.Erdos3.exists_centered_joint_returned_patch_normalization_ae line 301
  9. def OAI.Erdos3.RelativeReturnedFiberLaw line 385
  10. theorem OAI.Erdos3.RelativeReturnedFiberLaw.mono line 396
  11. theorem OAI.Erdos3.exists_centered_joint_returned_fiber_normalization_ae line 407
  12. theorem OAI.Erdos3.exists_relative_finite_returned_fiber_normalization line 480
  13. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSamplerFamily.exists_normalized_retained_center_of_event line 597
  14. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSamplerFamily.exists_normalized_retained_center line 638
  15. theorem OAI.Erdos3.VectorPolynomial.preparedFinalScalarBudget_ready_requirements line 683
  16. def OAI.Erdos3.VectorPolynomial.preparedRelativeFinalEnvelope line 741
  17. theorem OAI.Erdos3.VectorPolynomial.preparedRelativeFinalEnvelope_bounds line 748
  18. theorem OAI.Erdos3.VectorPolynomial.preparedRelativeFinalEnvelope_ready_requirements line 787
  19. theorem OAI.Erdos3.VectorPolynomial.exists_preparedRelativeFinalExtraction_power line 824
  20. theorem OAI.Erdos3.VectorPolynomial.preparedRelativeFinalExtraction_side_floor line 845