def
definition
effectivePrimePhaseInput_of_rsPrimePhaseEquidistribution
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.EffectivePrimePhaseInput on GitHub at line 67.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
64 phase distribution, not from finite search. -/
65 from_rcl_prime_ledger : True
66
67def effectivePrimePhaseInput_of_rsPrimePhaseEquidistribution
68 (rs : RSPrimePhaseEquidistribution) :
69 EffectivePrimePhaseInput :=
70 rs.effective_input
71
72theorem erdos_straus_residual_from_rsPrimePhaseEquidistribution
73 (rs : RSPrimePhaseEquidistribution)
74 {n : ℕ} (hn : ResidualTrap n) :
75 ErdosStrausRCL.HasRationalErdosStrausRepr (n : ℚ) :=
76 erdos_straus_residual_from_effectivePrimePhaseInput
77 (effectivePrimePhaseInput_of_rsPrimePhaseEquidistribution rs) hn
78
79end PrimePhaseInput
80end NumberTheory
81end IndisputableMonolith