def
definition
boundedBalancedSearch_of_rsPrimePhaseBoxTheorem
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.PrimePhaseDistribution on GitHub at line 76.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
BoundedBalancedSearchEngine -
boundedBalancedSearch_of_primePhaseBoxDistribution -
RSPrimePhaseBoxTheorem
used by
formal source
73
74/-- Once the RS prime phase box theorem is derived, it supplies the desired
75bounded balanced search engine. -/
76def boundedBalancedSearch_of_rsPrimePhaseBoxTheorem
77 (rs : RSPrimePhaseBoxTheorem) :
78 BoundedBalancedSearchEngine :=
79 boundedBalancedSearch_of_primePhaseBoxDistribution rs.distribution
80
81/-- Final conditional form, with the remaining theorem named explicitly. -/
82theorem erdos_straus_residual_from_rs_prime_phase_box
83 (rs : RSPrimePhaseBoxTheorem)
84 {n : ℕ} (hn : ResidualTrap n) :
85 ErdosStrausRCL.HasRationalErdosStrausRepr (n : ℚ) :=
86 bounded_balanced_search_solved
87 (boundedBalancedSearch_of_rsPrimePhaseBoxTheorem rs) hn
88
89end PrimePhaseDistribution
90end NumberTheory
91end IndisputableMonolith