A moving prefix of positive relative length has uniform positive density
ProvedErdos390.WholePaper.BankPaperRealization.exists_uniform_movingPrefix_density_lower_bound_of_fraction_compactanalytic-number-theoryerdos-390erdos390-source-construction
Fix a head pattern , real , and . There are and such that for every and integer endpoint with and normalized physical prefix fraction at least ,
Here the prefix fraction is exactly , using the real physical endpoints before rounding. The lower bound is uniform over the moving endpoint.
Preamble
import Definitions.Def_erdos390_remaining_analytic_propositions_007
Formal statement
theorem Erdos390.WholePaper.BankPaperRealization.exists_uniform_movingPrefix_density_lower_bound_of_fraction_compact : Erdos390.RemainingAnalyticGoal007_007 := by sorry
Source