OAI/NumberTheory/Jacobsthal/Estimates/FullEndpointData.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosVarianceEffective.effectiveSize line 14
  2. theorem OAI.Erdos970.ErdosVarianceEffective.effective_ratio_identity line 17
  3. theorem OAI.Erdos970.ErdosVarianceEffective.effective_ratio_upper line 33
  4. theorem OAI.Erdos970.ErdosVarianceEffective.effective_size_ratio_le line 53
  5. theorem OAI.Erdos970.ErdosVarianceEffective.denominator_le_effectiveModulus line 100
  6. theorem OAI.Erdos970.ErdosVarianceEffective.nonaligned_le_effectiveModulus line 106
  7. theorem OAI.Erdos970.ErdosVarianceEffective.alignedCofactor_le_full line 112
  8. theorem OAI.Erdos970.ErdosVarianceEffective.soft_effective_bounds line 117
  9. theorem OAI.Erdos970.ErdosVarianceEffective.large_factor_aligns_of_soft line 132
  10. theorem OAI.Erdos970.ErdosVarianceSmallModel.source_effective_point_domination line 154
  11. theorem OAI.Erdos970.ErdosVarianceEffective.actual_numerator_triangle line 183
  12. theorem OAI.Erdos970.ErdosVarianceEffective.soft_global_heights line 205
  13. theorem OAI.Erdos970.ErdosVarianceEffective.source_effective_heights line 245
  14. theorem OAI.Erdos970.ErdosVarianceEffective.soft_full_factor_alignment line 288
  15. theorem OAI.Erdos970.ErdosVarianceEffective.soft_endpoint_eligible line 299
  16. theorem OAI.Erdos970.ErdosVarianceEligible.structured_endpoint_heights line 328
  17. theorem OAI.Erdos970.ErdosVarianceEligible.full_endpoint_data line 406