Theorem: integrability_aux₀ (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
a b : ℝ
⊢ ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict [[a, b]], ‖↑⌊x⌋‖ ≤ max ‖a‖ ‖b‖ + 1
Tactic:
apply (MeasureTheory.ae_restrict_iff' measurableSet_Icc).mpr
State after:
a b : ℝ
⊢ ∀ᵐ (x : ℝ), x ∈ Icc (a ⊓ b) (a ⊔ b) → ‖↑⌊x⌋‖ ≤ max ‖a‖ ‖b‖ + 1

State before:
a b : ℝ
⊢ ∀ᵐ (x : ℝ), x ∈ Icc (a ⊓ b) (a ⊔ b) → ‖↑⌊x⌋‖ ≤ max ‖a‖ ‖b‖ + 1
Tactic:
refine MeasureTheory.ae_of_all _ (fun x hx ↦ ?_)
State after:
a b x : ℝ
hx : x ∈ Icc (a ⊓ b) (a ⊔ b)
⊢ ‖↑⌊x⌋‖ ≤ max ‖a‖ ‖b‖ + 1

State before:
a b x : ℝ
hx : x ∈ Icc (a ⊓ b) (a ⊔ b)
⊢ ‖↑⌊x⌋‖ ≤ max ‖a‖ ‖b‖ + 1
Tactic:
simp only [inf_le_iff, le_sup_iff, mem_Icc] at hx
State after:
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
⊢ ‖↑⌊x⌋‖ ≤ max ‖a‖ ‖b‖ + 1

State before:
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
⊢ ‖↑⌊x⌋‖ ≤ max ‖a‖ ‖b‖ + 1
Tactic:
simp only [norm_int, Real.norm_eq_abs]
State after:
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
⊢ |↑⌊x⌋| ≤ max |a| |b| + 1

State before:
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
this : |x| ≤ max |a| |b|
⊢ |↑⌊x⌋| ≤ max |a| |b| + 1
Tactic:
cases' abs_cases x with hx hx
State after:
case inl
a b x : ℝ
hx✝ : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
this : |x| ≤ max |a| |b|
hx : |x| = x ∧ 0 ≤ x
⊢ |↑⌊x⌋| ≤ max |a| |b| + 1

case inr
a b x : ℝ
hx✝ : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
this : |x| ≤ max |a| |b|
hx : |x| = -x ∧ x < 0
⊢ |↑⌊x⌋| ≤ max |a| |b| + 1

State before:
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
⊢ |x| ≤ max |a| |b|
Tactic:
cases' hx.1 with x_ge_a x_ge_b <;> cases' hx.2 with x_le_a x_le_b
State after:
case inl.inl
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_a : a ≤ x
x_le_a : x ≤ a
⊢ |x| ≤ max |a| |b|

case inl.inr
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_a : a ≤ x
x_le_b : x ≤ b
⊢ |x| ≤ max |a| |b|

case inr.inl
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_b : b ≤ x
x_le_a : x ≤ a
⊢ |x| ≤ max |a| |b|

case inr.inr
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_b : b ≤ x
x_le_b : x ≤ b
⊢ |x| ≤ max |a| |b|

State before:
case inl.inl
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_a : a ≤ x
x_le_a : x ≤ a
⊢ |x| ≤ max |a| |b|
Tactic:
rw [(by linarith : x = a)]
State after:
case inl.inl
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_a : a ≤ x
x_le_a : x ≤ a
⊢ |a| ≤ max |a| |b|

State before:
case inl.inl
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_a : a ≤ x
x_le_a : x ≤ a
⊢ |a| ≤ max |a| |b|
Tactic:
apply le_max_left
State after:
no goals

State before:
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_a : a ≤ x
x_le_a : x ≤ a
⊢ x = a
Tactic:
linarith
State after:
no goals

State before:
case inl.inr
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_a : a ≤ x
x_le_b : x ≤ b
⊢ |x| ≤ max |a| |b|
Tactic:
apply abs_le_max_abs_abs x_ge_a x_le_b
State after:
no goals

State before:
case inr.inl
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_b : b ≤ x
x_le_a : x ≤ a
⊢ |x| ≤ max |a| |b|
Tactic:
rw [max_comm]
State after:
case inr.inl
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_b : b ≤ x
x_le_a : x ≤ a
⊢ |x| ≤ max |b| |a|

State before:
case inr.inl
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_b : b ≤ x
x_le_a : x ≤ a
⊢ |x| ≤ max |b| |a|
Tactic:
apply abs_le_max_abs_abs x_ge_b x_le_a
State after:
no goals

State before:
case inr.inr
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_b : b ≤ x
x_le_b : x ≤ b
⊢ |x| ≤ max |a| |b|
Tactic:
rw [(by linarith : x = b)]
State after:
case inr.inr
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_b : b ≤ x
x_le_b : x ≤ b
⊢ |b| ≤ max |a| |b|

State before:
case inr.inr
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_b : b ≤ x
x_le_b : x ≤ b
⊢ |b| ≤ max |a| |b|
Tactic:
apply le_max_right
State after:
no goals

State before:
a b x : ℝ
hx : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
x_ge_b : b ≤ x
x_le_b : x ≤ b
⊢ x = b
Tactic:
linarith
State after:
no goals

State before:
case inl
a b x : ℝ
hx✝ : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
this : |x| ≤ max |a| |b|
hx : |x| = x ∧ 0 ≤ x
⊢ |↑⌊x⌋| ≤ max |a| |b| + 1
Tactic:
rw [_root_.abs_of_nonneg <| by exact_mod_cast Int.floor_nonneg.mpr hx.2]
State after:
case inl
a b x : ℝ
hx✝ : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
this : |x| ≤ max |a| |b|
hx : |x| = x ∧ 0 ≤ x
⊢ ↑⌊x⌋ ≤ max |a| |b| + 1

State before:
case inl
a b x : ℝ
hx✝ : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
this : |x| ≤ max |a| |b|
hx : |x| = x ∧ 0 ≤ x
⊢ ↑⌊x⌋ ≤ max |a| |b| + 1
Tactic:
apply le_trans (Int.floor_le x) <| le_trans (hx.1 ▸ this) (by simp)
State after:
no goals

State before:
a b x : ℝ
hx✝ : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
this : |x| ≤ max |a| |b|
hx : |x| = x ∧ 0 ≤ x
⊢ 0 ≤ ↑⌊x⌋
Tactic:
exact_mod_cast Int.floor_nonneg.mpr hx.2
State after:
no goals

State before:
a b x : ℝ
hx✝ : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
this : |x| ≤ max |a| |b|
hx : |x| = x ∧ 0 ≤ x
⊢ max |a| |b| ≤ max |a| |b| + 1
Tactic:
simp
State after:
no goals

State before:
case inr
a b x : ℝ
hx✝ : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
this : |x| ≤ max |a| |b|
hx : |x| = -x ∧ x < 0
⊢ |↑⌊x⌋| ≤ max |a| |b| + 1
Tactic:
rw [_root_.abs_of_nonpos <| by exact_mod_cast Int.floor_nonpos hx.2.le]
State after:
case inr
a b x : ℝ
hx✝ : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
this : |x| ≤ max |a| |b|
hx : |x| = -x ∧ x < 0
⊢ -↑⌊x⌋ ≤ max |a| |b| + 1

State before:
case inr
a b x : ℝ
hx✝ : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
this : |x| ≤ max |a| |b|
hx : |x| = -x ∧ x < 0
⊢ -↑⌊x⌋ ≤ max |a| |b| + 1
Tactic:
linarith [(Int.lt_floor_add_one x).le]
State after:
no goals

State before:
a b x : ℝ
hx✝ : (a ≤ x ∨ b ≤ x) ∧ (x ≤ a ∨ x ≤ b)
this : |x| ≤ max |a| |b|
hx : |x| = -x ∧ x < 0
⊢ ↑⌊x⌋ ≤ 0
Tactic:
exact_mod_cast Int.floor_nonpos hx.2.le
State after:
no goals