Source indexedtheorem · leanprover/lean4:v4.32.0

BrunTitchmarsh.floor_div_approx

PrimeNumberTheoremAnd.BrunTitchmarsh · PrimeNumberTheoremAnd/BrunTitchmarsh.lean:164 to 178

Mathematical statement

Exact Lean statement

theorem floor_div_approx (x : ℝ) (hx : 0 ≤ x) (d : ℕ) :
    ∃ C, |C| ≤ 2 ∧ ↑((Nat.floor x)/d) = x / d + C

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem floor_div_approx (x : ℝ) (hx : 0 ≤ x) (d : ℕ) :    ∃ C, |C| ≤ 2 ∧ ↑((Nat.floor x)/d) = x / d + C := by  by_cases hd : d = 0  · simp [hd]  · obtain ⟨C₁, hC₁_le, hC₁⟩ := nat_div_approx (Nat.floor x) d    obtain ⟨C₂, hC₂_le, hC₂⟩ := floor_approx x hx    rw [hC₁, hC₂]    refine ⟨C₁ + C₂/d, ?_, by ring⟩    have : |C₁ + C₂/d| ≤ |C₁| + |C₂/d| := abs_add_le C₁ (C₂ / ↑d)    have : |C₂/d| ≤ |C₂| := by      rw [abs_div]      refine div_le_self (abs_nonneg C₂) ?_      simp only [Nat.abs_cast, Nat.one_le_cast]      omega    linarith