Theorem: BrunTitchmarsh.floor_div_approx (PrimeNumberTheoremAnd/BrunTitchmarsh.lean)

State before:
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
⊢ ∃ C, |C| ≤ 2 ∧ ↑(⌊x⌋₊ / d) = x / ↑d + C
Tactic:
by_cases hd : d = 0
State after:
case pos
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : d = 0
⊢ ∃ C, |C| ≤ 2 ∧ ↑(⌊x⌋₊ / d) = x / ↑d + C

case neg
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
⊢ ∃ C, |C| ≤ 2 ∧ ↑(⌊x⌋₊ / d) = x / ↑d + C

State before:
case neg
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
⊢ ∃ C, |C| ≤ 2 ∧ ↑(⌊x⌋₊ / d) = x / ↑d + C
Tactic:
obtain ⟨C₁, hC₁_le, hC₁⟩ := nat_div_approx (Nat.floor x) d
State after:
case neg.intro.intro
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
⊢ ∃ C, |C| ≤ 2 ∧ ↑(⌊x⌋₊ / d) = x / ↑d + C

State before:
case neg.intro.intro
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
⊢ ∃ C, |C| ≤ 2 ∧ ↑(⌊x⌋₊ / d) = x / ↑d + C
Tactic:
obtain ⟨C₂, hC₂_le, hC₂⟩ := floor_approx x hx
State after:
case neg.intro.intro.intro.intro
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
⊢ ∃ C, |C| ≤ 2 ∧ ↑(⌊x⌋₊ / d) = x / ↑d + C

State before:
case neg.intro.intro.intro.intro
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
⊢ ∃ C, |C| ≤ 2 ∧ ↑(⌊x⌋₊ / d) = x / ↑d + C
Tactic:
rw[hC₁, hC₂]
State after:
case neg.intro.intro.intro.intro
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
⊢ ∃ C, |C| ≤ 2 ∧ (x + C₂) / ↑d + C₁ = x / ↑d + C

State before:
case neg.intro.intro.intro.intro
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
⊢ ∃ C, |C| ≤ 2 ∧ (x + C₂) / ↑d + C₁ = x / ↑d + C
Tactic:
use  C₁ + C₂/d
State after:
case h
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
⊢ |C₁ + C₂ / ↑d| ≤ 2 ∧ (x + C₂) / ↑d + C₁ = x / ↑d + (C₁ + C₂ / ↑d)

State before:
case h
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
⊢ |C₁ + C₂ / ↑d| ≤ 2 ∧ (x + C₂) / ↑d + C₁ = x / ↑d + (C₁ + C₂ / ↑d)
Tactic:
refine ⟨?_, by ring⟩
State after:
case h
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
⊢ |C₁ + C₂ / ↑d| ≤ 2

State before:
case h
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
⊢ |C₁ + C₂ / ↑d| ≤ 2
Tactic:
have : |C₁ + C₂/d| ≤ |C₁| + |C₂/d| := abs_add C₁ (C₂ / ↑d)
State after:
case h
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
this : |C₁ + C₂ / ↑d| ≤ |C₁| + |C₂ / ↑d|
⊢ |C₁ + C₂ / ↑d| ≤ 2

State before:
case h
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
this✝ : |C₁ + C₂ / ↑d| ≤ |C₁| + |C₂ / ↑d|
this : |C₂ / ↑d| ≤ |C₂|
⊢ |C₁ + C₂ / ↑d| ≤ 2
Tactic:
linarith
State after:
no goals

State before:
case pos
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : d = 0
⊢ ∃ C, |C| ≤ 2 ∧ ↑(⌊x⌋₊ / d) = x / ↑d + C
Tactic:
simp [hd]
State after:
no goals

State before:
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
⊢ (x + C₂) / ↑d + C₁ = x / ↑d + (C₁ + C₂ / ↑d)
Tactic:
ring
State after:
no goals

State before:
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
this : |C₁ + C₂ / ↑d| ≤ |C₁| + |C₂ / ↑d|
⊢ |C₂ / ↑d| ≤ |C₂|
Tactic:
rw[abs_div]
State after:
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
this : |C₁ + C₂ / ↑d| ≤ |C₁| + |C₂ / ↑d|
⊢ |C₂| / |↑d| ≤ |C₂|

State before:
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
this : |C₁ + C₂ / ↑d| ≤ |C₁| + |C₂ / ↑d|
⊢ |C₂| / |↑d| ≤ |C₂|
Tactic:
apply div_le_self
State after:
case ha
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
this : |C₁ + C₂ / ↑d| ≤ |C₁| + |C₂ / ↑d|
⊢ 0 ≤ |C₂|

case hb
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
this : |C₁ + C₂ / ↑d| ≤ |C₁| + |C₂ / ↑d|
⊢ 1 ≤ |↑d|

State before:
case ha
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
this : |C₁ + C₂ / ↑d| ≤ |C₁| + |C₂ / ↑d|
⊢ 0 ≤ |C₂|
Tactic:
exact abs_nonneg C₂
State after:
no goals

State before:
case hb
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
this : |C₁ + C₂ / ↑d| ≤ |C₁| + |C₂ / ↑d|
⊢ 1 ≤ |↑d|
Tactic:
simp only [Nat.abs_cast, Nat.one_le_cast]
State after:
case hb
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
this : |C₁ + C₂ / ↑d| ≤ |C₁| + |C₂ / ↑d|
⊢ 1 ≤ d

State before:
case hb
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
this : |C₁ + C₂ / ↑d| ≤ |C₁| + |C₂ / ↑d|
⊢ 1 ≤ d
Tactic:
omega
State after:
no goals