OAI/NumberTheory/Jacobsthal/Estimates/EffectiveSurvivors.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.ErdosVarianceEffective.effectiveBase line 15
2. def OAI.Erdos970.ErdosVarianceEffective.effectiveSurvivors line 19
3. theorem OAI.Erdos970.ErdosVarianceEffective.effectiveBase_eq_sourceParentBase line 24
4. theorem OAI.Erdos970.ErdosVarianceEffective.effectiveSurvivors_eq_parent line 33
5. theorem OAI.Erdos970.ErdosVarianceEffective.hypothetical_candidates_eq_effective_image line 50
6. theorem OAI.Erdos970.ErdosVarianceEffective.hypothetical_count_eq_effective_card line 59
7. theorem OAI.Erdos970.ErdosVarianceEffective.actual_aligned_count_eq_effective_card line 67
8. theorem OAI.Erdos970.ErdosVarianceEffective.effective_length_error line 75