[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
x : E
⊢ sqrt (1 + ‖x‖ ^ 2) ≤ 1 + ‖x‖
[PROOFSTEP]
rw [sqrt_le_left (by positivity)]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
x : E
⊢ 0 ≤ 1 + ‖x‖
[PROOFSTEP]
positivity
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
x : E
⊢ 1 + ‖x‖ ^ 2 ≤ (1 + ‖x‖) ^ 2
[PROOFSTEP]
simp [add_sq]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
x : E
⊢ 1 + ‖x‖ ≤ sqrt 2 * sqrt (1 + ‖x‖ ^ 2)
[PROOFSTEP]
rw [← sqrt_mul zero_le_two]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
x : E
⊢ 1 + ‖x‖ ≤ sqrt (2 * (1 + ‖x‖ ^ 2))
[PROOFSTEP]
have := sq_nonneg (‖x‖ - 1)
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
x : E
this : 0 ≤ (‖x‖ - 1) ^ 2
⊢ 1 + ‖x‖ ≤ sqrt (2 * (1 + ‖x‖ ^ 2))
[PROOFSTEP]
apply le_sqrt_of_sq_le
[GOAL]
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
x : E
this : 0 ≤ (‖x‖ - 1) ^ 2
⊢ (1 + ‖x‖) ^ 2 ≤ 2 * (1 + ‖x‖ ^ 2)
[PROOFSTEP]
linarith
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ (1 + ‖x‖ ^ 2) ^ (-r / 2) = 2 ^ (r / 2) * ((sqrt 2 * sqrt (1 + ‖x‖ ^ 2)) ^ r)⁻¹
[PROOFSTEP]
rw [rpow_div_two_eq_sqrt, rpow_div_two_eq_sqrt, mul_rpow, mul_inv, rpow_neg, mul_inv_cancel_left₀]
[GOAL]
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ sqrt 2 ^ r ≠ 0
[PROOFSTEP]
positivity
[GOAL]
case hx
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 0 ≤ sqrt (1 + ‖x‖ ^ 2)
[PROOFSTEP]
positivity
[GOAL]
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 0 ≤ sqrt 2
[PROOFSTEP]
positivity
[GOAL]
case h₁
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 0 ≤ sqrt (1 + ‖x‖ ^ 2)
[PROOFSTEP]
positivity
[GOAL]
case hx
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 0 ≤ 2
[PROOFSTEP]
positivity
[GOAL]
case hx
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 0 ≤ 1 + ‖x‖ ^ 2
[PROOFSTEP]
positivity
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 2 ^ (r / 2) * ((sqrt 2 * sqrt (1 + ‖x‖ ^ 2)) ^ r)⁻¹ ≤ 2 ^ (r / 2) * ((1 + ‖x‖) ^ r)⁻¹
[PROOFSTEP]
gcongr
[GOAL]
case h.h.h₁
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 1 + ‖x‖ ≤ sqrt 2 * sqrt (1 + ‖x‖ ^ 2)
[PROOFSTEP]
apply one_add_norm_le_sqrt_two_mul_sqrt
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 2 ^ (r / 2) * ((1 + ‖x‖) ^ r)⁻¹ = 2 ^ (r / 2) * (1 + ‖x‖) ^ (-r)
[PROOFSTEP]
rw [rpow_neg]
[GOAL]
case hx
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ
x : E
hr : 0 < r
⊢ 0 ≤ 1 + ‖x‖
[PROOFSTEP]
positivity
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
r t : ℝ
hr : 0 < r
ht : 0 < t
x : E
⊢ t ≤ (1 + ‖x‖) ^ (-r) ↔ ‖x‖ ≤ t ^ (-r⁻¹) - 1
[PROOFSTEP]
rw [le_sub_iff_add_le', neg_inv]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
r t : ℝ
hr : 0 < r
ht : 0 < t
x : E
⊢ t ≤ (1 + ‖x‖) ^ (-r) ↔ 1 + ‖x‖ ≤ t ^ (-r)⁻¹
[PROOFSTEP]
exact (Real.le_rpow_inv_iff_of_neg (by positivity) ht (neg_lt_zero.mpr hr)).symm
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
r t : ℝ
hr : 0 < r
ht : 0 < t
x : E
⊢ 0 < 1 + ‖x‖
[PROOFSTEP]
positivity
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
r t : ℝ
hr : 0 < r
ht : 1 < t
⊢ Metric.closedBall 0 (t ^ (-r⁻¹) - 1) = ∅
[PROOFSTEP]
rw [Metric.closedBall_eq_empty, sub_neg]
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
r t : ℝ
hr : 0 < r
ht : 1 < t
⊢ t ^ (-r⁻¹) < 1
[PROOFSTEP]
exact Real.rpow_lt_one_of_one_lt_of_neg ht (by simp only [hr, Right.neg_neg_iff, inv_pos])
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
r t : ℝ
hr : 0 < r
ht : 1 < t
⊢ -r⁻¹ < 0
[PROOFSTEP]
simp only [hr, Right.neg_neg_iff, inv_pos]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ
n : ℕ
hnr : ↑n < r
⊢ ∫⁻ (x : ℝ) in Ioc 0 1, ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) < ⊤
[PROOFSTEP]
have hr : 0 < r := lt_of_le_of_lt n.cast_nonneg hnr
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ
n : ℕ
hnr : ↑n < r
hr : 0 < r
⊢ ∫⁻ (x : ℝ) in Ioc 0 1, ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) < ⊤
[PROOFSTEP]
have h_int : ∀ x : ℝ, x ∈ Ioc (0 : ℝ) 1 → ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * n))) :=
  fun x hx ↦ by
  apply ENNReal.ofReal_le_ofReal
  rw [← neg_mul, rpow_mul hx.1.le, rpow_nat_cast]
  refine' pow_le_pow_of_le_left _ (by simp only [sub_le_self_iff, zero_le_one]) n
  rw [le_sub_iff_add_le', add_zero]
  refine' Real.one_le_rpow_of_pos_of_le_one_of_nonpos hx.1 hx.2 _
  rw [Right.neg_nonpos_iff, inv_nonneg]
  exact hr.le
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ
n : ℕ
hnr : ↑n < r
hr : 0 < r
x : ℝ
hx : x ∈ Ioc 0 1
⊢ ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * ↑n)))
[PROOFSTEP]
apply ENNReal.ofReal_le_ofReal
[GOAL]
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ
n : ℕ
hnr : ↑n < r
hr : 0 < r
x : ℝ
hx : x ∈ Ioc 0 1
⊢ (x ^ (-r⁻¹) - 1) ^ n ≤ x ^ (-(r⁻¹ * ↑n))
[PROOFSTEP]
rw [← neg_mul, rpow_mul hx.1.le, rpow_nat_cast]
[GOAL]
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ
n : ℕ
hnr : ↑n < r
hr : 0 < r
x : ℝ
hx : x ∈ Ioc 0 1
⊢ (x ^ (-r⁻¹) - 1) ^ n ≤ (x ^ (-r⁻¹)) ^ n
[PROOFSTEP]
refine' pow_le_pow_of_le_left _ (by simp only [sub_le_self_iff, zero_le_one]) n
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ
n : ℕ
hnr : ↑n < r
hr : 0 < r
x : ℝ
hx : x ∈ Ioc 0 1
⊢ x ^ (-r⁻¹) - 1 ≤ x ^ (-r⁻¹)
[PROOFSTEP]
simp only [sub_le_self_iff, zero_le_one]
[GOAL]
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ
n : ℕ
hnr : ↑n < r
hr : 0 < r
x : ℝ
hx : x ∈ Ioc 0 1
⊢ 0 ≤ x ^ (-r⁻¹) - 1
[PROOFSTEP]
rw [le_sub_iff_add_le', add_zero]
[GOAL]
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ
n : ℕ
hnr : ↑n < r
hr : 0 < r
x : ℝ
hx : x ∈ Ioc 0 1
⊢ 1 ≤ x ^ (-r⁻¹)
[PROOFSTEP]
refine' Real.one_le_rpow_of_pos_of_le_one_of_nonpos hx.1 hx.2 _
[GOAL]
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ
n : ℕ
hnr : ↑n < r
hr : 0 < r
x : ℝ
hx : x ∈ Ioc 0 1
⊢ -r⁻¹ ≤ 0
[PROOFSTEP]
rw [Right.neg_nonpos_iff, inv_nonneg]
[GOAL]
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ
n : ℕ
hnr : ↑n < r
hr : 0 < r
x : ℝ
hx : x ∈ Ioc 0 1
⊢ 0 ≤ r
[PROOFSTEP]
exact hr.le
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ
n : ℕ
hnr : ↑n < r
hr : 0 < r
h_int : ∀ (x : ℝ), x ∈ Ioc 0 1 → ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * ↑n)))
⊢ ∫⁻ (x : ℝ) in Ioc 0 1, ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) < ⊤
[PROOFSTEP]
refine' lt_of_le_of_lt (set_lintegral_mono' measurableSet_Ioc h_int) _
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ
n : ℕ
hnr : ↑n < r
hr : 0 < r
h_int : ∀ (x : ℝ), x ∈ Ioc 0 1 → ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * ↑n)))
⊢ ∫⁻ (x : ℝ) in Ioc 0 1, ENNReal.ofReal (x ^ (-(r⁻¹ * ↑n))) < ⊤
[PROOFSTEP]
refine' IntegrableOn.set_lintegral_lt_top _
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ
n : ℕ
hnr : ↑n < r
hr : 0 < r
h_int : ∀ (x : ℝ), x ∈ Ioc 0 1 → ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * ↑n)))
⊢ IntegrableOn (fun x => x ^ (-(r⁻¹ * ↑n))) (Ioc 0 1)
[PROOFSTEP]
rw [← intervalIntegrable_iff_integrable_Ioc_of_le zero_le_one]
[GOAL]
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ
n : ℕ
hnr : ↑n < r
hr : 0 < r
h_int : ∀ (x : ℝ), x ∈ Ioc 0 1 → ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * ↑n)))
⊢ IntervalIntegrable (fun x => x ^ (-(r⁻¹ * ↑n))) volume 0 1
[PROOFSTEP]
apply intervalIntegral.intervalIntegrable_rpow'
[GOAL]
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ
n : ℕ
hnr : ↑n < r
hr : 0 < r
h_int : ∀ (x : ℝ), x ∈ Ioc 0 1 → ENNReal.ofReal ((x ^ (-r⁻¹) - 1) ^ n) ≤ ENNReal.ofReal (x ^ (-(r⁻¹ * ↑n)))
⊢ -1 < -(r⁻¹ * ↑n)
[PROOFSTEP]
rwa [neg_lt_neg_iff, inv_mul_lt_iff' hr, one_mul]
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
⊢ ∫⁻ (x : E), ENNReal.ofReal ((1 + ‖x‖) ^ (-r)) < ⊤
[PROOFSTEP]
have hr : 0 < r := lt_of_le_of_lt (finrank ℝ E).cast_nonneg hnr
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
⊢ ∫⁻ (x : E), ENNReal.ofReal ((1 + ‖x‖) ^ (-r)) < ⊤
[PROOFSTEP]
have h_meas : Measurable fun ω : E => (1 + ‖ω‖) ^ (-r) :=
  -- porting note: was `by measurability`(measurable_norm.const_add _).pow_const _
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
⊢ ∫⁻ (x : E), ENNReal.ofReal ((1 + ‖x‖) ^ (-r)) < ⊤
[PROOFSTEP]
have h_pos : ∀ x : E, 0 ≤ (1 + ‖x‖) ^ (-r) := fun x ↦ by positivity
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
x : E
⊢ 0 ≤ (1 + ‖x‖) ^ (-r)
[PROOFSTEP]
positivity
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
⊢ ∫⁻ (x : E), ENNReal.ofReal ((1 + ‖x‖) ^ (-r)) < ⊤
[PROOFSTEP]
rw [lintegral_eq_lintegral_meas_le volume h_pos h_meas]
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
⊢ ∫⁻ (t : ℝ) in Ioi 0, ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} < ⊤
[PROOFSTEP]
have h_int : ∀ t, 0 < t → volume {a : E | t ≤ (1 + ‖a‖) ^ (-r)} = volume (Metric.closedBall (0 : E) (t ^ (-r⁻¹) - 1)) :=
  fun t ht ↦ by
  congr 1
  ext x
  simp only [mem_setOf_eq, mem_closedBall_zero_iff]
  exact le_rpow_one_add_norm_iff_norm_le hr (mem_Ioi.mp ht) x
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
t : ℝ
ht : 0 < t
⊢ ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} = ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
[PROOFSTEP]
congr 1
[GOAL]
case e_a
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
t : ℝ
ht : 0 < t
⊢ {a | t ≤ (1 + ‖a‖) ^ (-r)} = Metric.closedBall 0 (t ^ (-r⁻¹) - 1)
[PROOFSTEP]
ext x
[GOAL]
case e_a.h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
t : ℝ
ht : 0 < t
x : E
⊢ x ∈ {a | t ≤ (1 + ‖a‖) ^ (-r)} ↔ x ∈ Metric.closedBall 0 (t ^ (-r⁻¹) - 1)
[PROOFSTEP]
simp only [mem_setOf_eq, mem_closedBall_zero_iff]
[GOAL]
case e_a.h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
t : ℝ
ht : 0 < t
x : E
⊢ t ≤ (1 + ‖x‖) ^ (-r) ↔ ‖x‖ ≤ t ^ (-r⁻¹) - 1
[PROOFSTEP]
exact le_rpow_one_add_norm_iff_norm_le hr (mem_Ioi.mp ht) x
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} = ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
⊢ ∫⁻ (t : ℝ) in Ioi 0, ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} < ⊤
[PROOFSTEP]
rw [set_lintegral_congr_fun measurableSet_Ioi (eventually_of_forall h_int)]
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} = ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
⊢ ∫⁻ (x : ℝ) in Ioi 0, ↑↑volume (Metric.closedBall 0 (x ^ (-r⁻¹) - 1)) < ⊤
[PROOFSTEP]
set f := fun t : ℝ ↦ volume (Metric.closedBall (0 : E) (t ^ (-r⁻¹) - 1))
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} = ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t => ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
⊢ lintegral (Measure.restrict volume (Ioi 0)) f < ⊤
[PROOFSTEP]
set mB :=
  volume
    (Metric.ball (0 : E) 1)
      -- the next two inequalities are in fact equalities but we don't need that
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} = ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t => ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := ↑↑volume (Metric.ball 0 1)
⊢ lintegral (Measure.restrict volume (Ioi 0)) f < ⊤
[PROOFSTEP]
calc
  ∫⁻ t in Ioi 0, f t ≤ ∫⁻ t in Ioc 0 1 ∪ Ioi 1, f t := lintegral_mono_set Ioi_subset_Ioc_union_Ioi
  _ ≤ (∫⁻ t in Ioc 0 1, f t) + ∫⁻ t in Ioi 1, f t := (lintegral_union_le _ _ _)
  _ < ∞ := ENNReal.add_lt_top.2 ⟨?_, ?_⟩
[GOAL]
case calc_1
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} = ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t => ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := ↑↑volume (Metric.ball 0 1)
⊢ ∫⁻ (t : ℝ) in Ioc 0 1, f t < ⊤
[PROOFSTEP]
have h_int' : ∀ t ∈ Ioc (0 : ℝ) 1, f t = ENNReal.ofReal ((t ^ (-r⁻¹) - 1) ^ finrank ℝ E) * mB := fun t ht ↦
  by
  refine' volume.addHaar_closedBall (0 : E) _
  rw [sub_nonneg]
  exact Real.one_le_rpow_of_pos_of_le_one_of_nonpos ht.1 ht.2 (by simp [hr.le])
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} = ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t => ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := ↑↑volume (Metric.ball 0 1)
t : ℝ
ht : t ∈ Ioc 0 1
⊢ f t = ENNReal.ofReal ((t ^ (-r⁻¹) - 1) ^ finrank ℝ E) * mB
[PROOFSTEP]
refine' volume.addHaar_closedBall (0 : E) _
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} = ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t => ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := ↑↑volume (Metric.ball 0 1)
t : ℝ
ht : t ∈ Ioc 0 1
⊢ 0 ≤ t ^ (-r⁻¹) - 1
[PROOFSTEP]
rw [sub_nonneg]
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} = ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t => ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := ↑↑volume (Metric.ball 0 1)
t : ℝ
ht : t ∈ Ioc 0 1
⊢ 1 ≤ t ^ (-r⁻¹)
[PROOFSTEP]
exact Real.one_le_rpow_of_pos_of_le_one_of_nonpos ht.1 ht.2 (by simp [hr.le])
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} = ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t => ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := ↑↑volume (Metric.ball 0 1)
t : ℝ
ht : t ∈ Ioc 0 1
⊢ -r⁻¹ ≤ 0
[PROOFSTEP]
simp [hr.le]
[GOAL]
case calc_1
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} = ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t => ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := ↑↑volume (Metric.ball 0 1)
h_int' : ∀ (t : ℝ), t ∈ Ioc 0 1 → f t = ENNReal.ofReal ((t ^ (-r⁻¹) - 1) ^ finrank ℝ E) * mB
⊢ ∫⁻ (t : ℝ) in Ioc 0 1, f t < ⊤
[PROOFSTEP]
rw [set_lintegral_congr_fun measurableSet_Ioc (ae_of_all _ h_int'), lintegral_mul_const' _ _ measure_ball_lt_top.ne]
[GOAL]
case calc_1
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} = ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t => ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := ↑↑volume (Metric.ball 0 1)
h_int' : ∀ (t : ℝ), t ∈ Ioc 0 1 → f t = ENNReal.ofReal ((t ^ (-r⁻¹) - 1) ^ finrank ℝ E) * mB
⊢ (∫⁻ (a : ℝ) in Ioc 0 1, ENNReal.ofReal ((a ^ (-r⁻¹) - 1) ^ finrank ℝ E)) * ↑↑volume (Metric.ball 0 1) < ⊤
[PROOFSTEP]
exact ENNReal.mul_lt_top (finite_integral_rpow_sub_one_pow_aux (finrank ℝ E) hnr).ne measure_ball_lt_top.ne
[GOAL]
case calc_2
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} = ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t => ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := ↑↑volume (Metric.ball 0 1)
⊢ ∫⁻ (t : ℝ) in Ioi 1, f t < ⊤
[PROOFSTEP]
have h_int'' : ∀ t ∈ Ioi (1 : ℝ), f t = 0 := fun t ht => by
  simp only [closedBall_rpow_sub_one_eq_empty_aux E hr ht, measure_empty]
    -- The integral over the constant zero function is finite:
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} = ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t => ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := ↑↑volume (Metric.ball 0 1)
t : ℝ
ht : t ∈ Ioi 1
⊢ f t = 0
[PROOFSTEP]
simp only [closedBall_rpow_sub_one_eq_empty_aux E hr ht, measure_empty]
  -- The integral over the constant zero function is finite:
[GOAL]
case calc_2
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} = ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t => ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := ↑↑volume (Metric.ball 0 1)
h_int'' : ∀ (t : ℝ), t ∈ Ioi 1 → f t = 0
⊢ ∫⁻ (t : ℝ) in Ioi 1, f t < ⊤
[PROOFSTEP]
rw [set_lintegral_congr_fun measurableSet_Ioi (ae_of_all volume <| h_int''), lintegral_const 0, zero_mul]
[GOAL]
case calc_2
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
h_meas : Measurable fun ω => (1 + ‖ω‖) ^ (-r)
h_pos : ∀ (x : E), 0 ≤ (1 + ‖x‖) ^ (-r)
h_int : ∀ (t : ℝ), 0 < t → ↑↑volume {a | t ≤ (1 + ‖a‖) ^ (-r)} = ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
f : ℝ → ℝ≥0∞ := fun t => ↑↑volume (Metric.closedBall 0 (t ^ (-r⁻¹) - 1))
mB : ℝ≥0∞ := ↑↑volume (Metric.ball 0 1)
h_int'' : ∀ (t : ℝ), t ∈ Ioi 1 → f t = 0
⊢ 0 < ⊤
[PROOFSTEP]
exact WithTop.zero_lt_top
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
⊢ Integrable fun x => (1 + ‖x‖) ^ (-r)
[PROOFSTEP]
constructor
[GOAL]
case left
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
⊢ AEStronglyMeasurable (fun x => (1 + ‖x‖) ^ (-r)) volume
[PROOFSTEP]
exact ((measurable_norm.const_add _).pow_const _).aestronglyMeasurable
[GOAL]
case right
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
⊢ HasFiniteIntegral fun x => (1 + ‖x‖) ^ (-r)
[PROOFSTEP]
have : (∫⁻ a : E, ‖(1 + ‖a‖) ^ (-r)‖₊) = ∫⁻ a : E, ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) :=
  lintegral_nnnorm_eq_of_nonneg fun _ => rpow_nonneg_of_nonneg (by positivity) _
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
x✝ : E
⊢ 0 ≤ 1 + ‖x✝‖
[PROOFSTEP]
positivity
[GOAL]
case right
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
this : ∫⁻ (a : E), ↑‖(1 + ‖a‖) ^ (-r)‖₊ = ∫⁻ (a : E), ENNReal.ofReal ((1 + ‖a‖) ^ (-r))
⊢ HasFiniteIntegral fun x => (1 + ‖x‖) ^ (-r)
[PROOFSTEP]
rw [HasFiniteIntegral, this]
[GOAL]
case right
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
this : ∫⁻ (a : E), ↑‖(1 + ‖a‖) ^ (-r)‖₊ = ∫⁻ (a : E), ENNReal.ofReal ((1 + ‖a‖) ^ (-r))
⊢ ∫⁻ (a : E), ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) < ⊤
[PROOFSTEP]
exact finite_integral_one_add_norm hnr
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
⊢ Integrable fun x => (1 + ‖x‖ ^ 2) ^ (-r / 2)
[PROOFSTEP]
have hr : 0 < r := lt_of_le_of_lt (finrank ℝ E).cast_nonneg hnr
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
⊢ Integrable fun x => (1 + ‖x‖ ^ 2) ^ (-r / 2)
[PROOFSTEP]
refine ((integrable_one_add_norm hnr).const_mul <| (2 : ℝ) ^ (r / 2)).mono' ?_ (eventually_of_forall fun x => ?_)
[GOAL]
case refine_1
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
⊢ AEStronglyMeasurable (fun x => (1 + ‖x‖ ^ 2) ^ (-r / 2)) volume
[PROOFSTEP]
exact (((measurable_id.norm.pow_const _).const_add _).pow_const _).aestronglyMeasurable
[GOAL]
case refine_2
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
x : E
⊢ ‖(1 + ‖x‖ ^ 2) ^ (-r / 2)‖ ≤ 2 ^ (r / 2) * (1 + ‖x‖) ^ (-r)
[PROOFSTEP]
refine (abs_of_pos ?_).trans_le (rpow_neg_one_add_norm_sq_le x hr)
[GOAL]
case refine_2
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasureSpace E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
r : ℝ
hnr : ↑(finrank ℝ E) < r
hr : 0 < r
x : E
⊢ 0 < (1 + ‖x‖ ^ 2) ^ (-r / 2)
[PROOFSTEP]
positivity


[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
⊢ (fun x => eval x P) ~[atTop] fun x => leadingCoeff P * x ^ natDegree P
[PROOFSTEP]
by_cases h : P = 0
[GOAL]
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P = 0
⊢ (fun x => eval x P) ~[atTop] fun x => leadingCoeff P * x ^ natDegree P
[PROOFSTEP]
simp [h, IsEquivalent.refl]
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : ¬P = 0
⊢ (fun x => eval x P) ~[atTop] fun x => leadingCoeff P * x ^ natDegree P
[PROOFSTEP]
simp only [Polynomial.eval_eq_sum_range, sum_range_succ]
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : ¬P = 0
⊢ (fun x =>
      (Finset.sum (range (natDegree P)) fun i => coeff P i * x ^ i) + coeff P (natDegree P) * x ^ natDegree P) ~[atTop]
    fun x => leadingCoeff P * x ^ natDegree P
[PROOFSTEP]
exact
  IsLittleO.add_isEquivalent
    (IsLittleO.sum fun i hi =>
      IsLittleO.const_mul_left
        ((IsLittleO.const_mul_right fun hz => h <| leadingCoeff_eq_zero.mp hz) <|
          isLittleO_pow_pow_atTop_of_lt (mem_range.mp hi))
        _)
    IsEquivalent.refl
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
⊢ Tendsto (fun x => eval x P) atTop atTop ↔ 0 < degree P ∧ 0 ≤ leadingCoeff P
[PROOFSTEP]
refine' ⟨fun h => _, fun h => tendsto_atTop_of_leadingCoeff_nonneg P h.1 h.2⟩
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : Tendsto (fun x => eval x P) atTop atTop
⊢ 0 < degree P ∧ 0 ≤ leadingCoeff P
[PROOFSTEP]
have : Tendsto (fun x => P.leadingCoeff * x ^ P.natDegree) atTop atTop := (isEquivalent_atTop_lead P).tendsto_atTop h
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : Tendsto (fun x => eval x P) atTop atTop
this : Tendsto (fun x => leadingCoeff P * x ^ natDegree P) atTop atTop
⊢ 0 < degree P ∧ 0 ≤ leadingCoeff P
[PROOFSTEP]
rw [tendsto_const_mul_pow_atTop_iff, ← pos_iff_ne_zero, natDegree_pos_iff_degree_pos] at this
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : Tendsto (fun x => eval x P) atTop atTop
this : 0 < degree P ∧ 0 < leadingCoeff P
⊢ 0 < degree P ∧ 0 ≤ leadingCoeff P
[PROOFSTEP]
exact ⟨this.1, this.2.le⟩
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
⊢ Tendsto (fun x => eval x P) atTop atBot ↔ 0 < degree P ∧ leadingCoeff P ≤ 0
[PROOFSTEP]
simp only [← tendsto_neg_atTop_iff, ← eval_neg, tendsto_atTop_iff_leadingCoeff_nonneg, degree_neg, leadingCoeff_neg,
  neg_nonneg]
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : 0 < degree P
⊢ Tendsto (fun x => |eval x P|) atTop atTop
[PROOFSTEP]
cases' le_total 0 P.leadingCoeff with hP hP
[GOAL]
case inl
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : 0 < degree P
hP : 0 ≤ leadingCoeff P
⊢ Tendsto (fun x => |eval x P|) atTop atTop
[PROOFSTEP]
exact tendsto_abs_atTop_atTop.comp (P.tendsto_atTop_of_leadingCoeff_nonneg hdeg hP)
[GOAL]
case inr
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : 0 < degree P
hP : leadingCoeff P ≤ 0
⊢ Tendsto (fun x => |eval x P|) atTop atTop
[PROOFSTEP]
exact tendsto_abs_atBot_atTop.comp (P.tendsto_atBot_of_leadingCoeff_nonpos hdeg hP)
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
⊢ (IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => |eval x P|) ↔ degree P ≤ 0
[PROOFSTEP]
refine'
  ⟨fun h => _, fun h =>
    ⟨|P.coeff 0|,
      eventually_map.mpr
        (eventually_of_forall
          (forall_imp (fun _ => le_of_eq) fun x =>
            congr_arg abs <| _root_.trans (congr_arg (eval x) (eq_C_of_degree_le_zero h)) eval_C))⟩⟩
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => |eval x P|
⊢ degree P ≤ 0
[PROOFSTEP]
contrapose! h
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : 0 < degree P
⊢ ¬IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop fun x => |eval x P|
[PROOFSTEP]
exact not_isBoundedUnder_of_tendsto_atTop (abs_tendsto_atTop P h)
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
⊢ Tendsto (fun x => eval x P) atTop (𝓝 c) ↔ leadingCoeff P = c ∧ degree P ≤ 0
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
⊢ leadingCoeff P = c ∧ degree P ≤ 0
[PROOFSTEP]
have := P.isEquivalent_atTop_lead.tendsto_nhds h
[GOAL]
case refine'_1
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
this : Tendsto (fun x => leadingCoeff P * x ^ natDegree P) atTop (𝓝 c)
⊢ leadingCoeff P = c ∧ degree P ≤ 0
[PROOFSTEP]
by_cases hP : P.leadingCoeff = 0
[GOAL]
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
this : Tendsto (fun x => leadingCoeff P * x ^ natDegree P) atTop (𝓝 c)
hP : leadingCoeff P = 0
⊢ leadingCoeff P = c ∧ degree P ≤ 0
[PROOFSTEP]
simp only [hP, zero_mul, tendsto_const_nhds_iff] at this
[GOAL]
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
hP : leadingCoeff P = 0
this : 0 = c
⊢ leadingCoeff P = c ∧ degree P ≤ 0
[PROOFSTEP]
refine' ⟨_root_.trans hP this, by simp [leadingCoeff_eq_zero.1 hP]⟩
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
hP : leadingCoeff P = 0
this : 0 = c
⊢ degree P ≤ 0
[PROOFSTEP]
simp [leadingCoeff_eq_zero.1 hP]
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
this : Tendsto (fun x => leadingCoeff P * x ^ natDegree P) atTop (𝓝 c)
hP : ¬leadingCoeff P = 0
⊢ leadingCoeff P = c ∧ degree P ≤ 0
[PROOFSTEP]
rw [tendsto_const_mul_pow_nhds_iff hP, natDegree_eq_zero_iff_degree_le_zero] at this
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
this : degree P ≤ 0 ∧ leadingCoeff P = c
hP : ¬leadingCoeff P = 0
⊢ leadingCoeff P = c ∧ degree P ≤ 0
[PROOFSTEP]
exact this.symm
[GOAL]
case refine'_2
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : leadingCoeff P = c ∧ degree P ≤ 0
⊢ Tendsto (fun x => eval x P) atTop (𝓝 c)
[PROOFSTEP]
refine' P.isEquivalent_atTop_lead.symm.tendsto_nhds _
[GOAL]
case refine'_2
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : leadingCoeff P = c ∧ degree P ≤ 0
⊢ Tendsto (fun x => leadingCoeff P * x ^ natDegree P) atTop (𝓝 c)
[PROOFSTEP]
have : P.natDegree = 0 := natDegree_eq_zero_iff_degree_le_zero.2 h.2
[GOAL]
case refine'_2
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : leadingCoeff P = c ∧ degree P ≤ 0
this : natDegree P = 0
⊢ Tendsto (fun x => leadingCoeff P * x ^ natDegree P) atTop (𝓝 c)
[PROOFSTEP]
simp only [h.1, this, pow_zero, mul_one]
[GOAL]
case refine'_2
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : leadingCoeff P = c ∧ degree P ≤ 0
this : natDegree P = 0
⊢ Tendsto (fun x => c) atTop (𝓝 c)
[PROOFSTEP]
exact tendsto_const_nhds
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
⊢ (fun x => eval x P / eval x Q) ~[atTop] fun x =>
    leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree P) - ↑(natDegree Q))
[PROOFSTEP]
by_cases hP : P = 0
[GOAL]
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : P = 0
⊢ (fun x => eval x P / eval x Q) ~[atTop] fun x =>
    leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree P) - ↑(natDegree Q))
[PROOFSTEP]
simp [hP, IsEquivalent.refl]
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : ¬P = 0
⊢ (fun x => eval x P / eval x Q) ~[atTop] fun x =>
    leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree P) - ↑(natDegree Q))
[PROOFSTEP]
by_cases hQ : Q = 0
[GOAL]
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : ¬P = 0
hQ : Q = 0
⊢ (fun x => eval x P / eval x Q) ~[atTop] fun x =>
    leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree P) - ↑(natDegree Q))
[PROOFSTEP]
simp [hQ, IsEquivalent.refl]
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : ¬P = 0
hQ : ¬Q = 0
⊢ (fun x => eval x P / eval x Q) ~[atTop] fun x =>
    leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree P) - ↑(natDegree Q))
[PROOFSTEP]
refine'
  (P.isEquivalent_atTop_lead.symm.div Q.isEquivalent_atTop_lead.symm).symm.trans
    (EventuallyEq.isEquivalent ((eventually_gt_atTop 0).mono fun x hx => _))
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hP : ¬P = 0
hQ : ¬Q = 0
x : 𝕜
hx : 0 < x
⊢ (fun x => leadingCoeff P * x ^ natDegree P / (leadingCoeff Q * x ^ natDegree Q)) x =
    (fun x => leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree P) - ↑(natDegree Q))) x
[PROOFSTEP]
simp [← div_mul_div_comm, hP, hQ, zpow_sub₀ hx.ne.symm]
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree P < degree Q
⊢ Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
[PROOFSTEP]
by_cases hP : P = 0
[GOAL]
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree P < degree Q
hP : P = 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
[PROOFSTEP]
simp [hP, tendsto_const_nhds]
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree P < degree Q
hP : ¬P = 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
[PROOFSTEP]
rw [← natDegree_lt_natDegree_iff hP] at hdeg
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree P < natDegree Q
hP : ¬P = 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
[PROOFSTEP]
refine' (isEquivalent_atTop_div P Q).symm.tendsto_nhds _
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree P < natDegree Q
hP : ¬P = 0
⊢ Tendsto (fun x => leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree P) - ↑(natDegree Q))) atTop (𝓝 0)
[PROOFSTEP]
rw [← mul_zero]
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree P < natDegree Q
hP : ¬P = 0
⊢ Tendsto (fun x => leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree P) - ↑(natDegree Q))) atTop (𝓝 (?neg✝ * 0))
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree P < natDegree Q
hP : ¬P = 0
⊢ 𝕜
[PROOFSTEP]
refine' (tendsto_zpow_atTop_zero _).const_mul _
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree P < natDegree Q
hP : ¬P = 0
⊢ ↑(natDegree P) - ↑(natDegree Q) < 0
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0) ↔ degree P < degree Q
[PROOFSTEP]
refine' ⟨fun h => _, div_tendsto_zero_of_degree_lt P Q⟩
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
⊢ degree P < degree Q
[PROOFSTEP]
by_cases hPQ : P.leadingCoeff / Q.leadingCoeff = 0
[GOAL]
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hPQ : leadingCoeff P / leadingCoeff Q = 0
⊢ degree P < degree Q
[PROOFSTEP]
simp only [div_eq_mul_inv, inv_eq_zero, mul_eq_zero] at hPQ
[GOAL]
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hPQ : leadingCoeff P = 0 ∨ leadingCoeff Q = 0
⊢ degree P < degree Q
[PROOFSTEP]
cases' hPQ with hP0 hQ0
[GOAL]
case pos.inl
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hP0 : leadingCoeff P = 0
⊢ degree P < degree Q
[PROOFSTEP]
rw [leadingCoeff_eq_zero.1 hP0, degree_zero]
[GOAL]
case pos.inl
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hP0 : leadingCoeff P = 0
⊢ ⊥ < degree Q
[PROOFSTEP]
exact bot_lt_iff_ne_bot.2 fun hQ' => hQ (degree_eq_bot.1 hQ')
[GOAL]
case pos.inr
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hQ0 : leadingCoeff Q = 0
⊢ degree P < degree Q
[PROOFSTEP]
exact absurd (leadingCoeff_eq_zero.1 hQ0) hQ
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬leadingCoeff P / leadingCoeff Q = 0
⊢ degree P < degree Q
[PROOFSTEP]
have := (isEquivalent_atTop_div P Q).tendsto_nhds h
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬leadingCoeff P / leadingCoeff Q = 0
this : Tendsto (fun x => leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree P) - ↑(natDegree Q))) atTop (𝓝 0)
⊢ degree P < degree Q
[PROOFSTEP]
rw [tendsto_const_mul_zpow_atTop_nhds_iff hPQ] at this
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬leadingCoeff P / leadingCoeff Q = 0
this :
  ↑(natDegree P) - ↑(natDegree Q) = 0 ∧ leadingCoeff P / leadingCoeff Q = 0 ∨
    ↑(natDegree P) - ↑(natDegree Q) < 0 ∧ 0 = 0
⊢ degree P < degree Q
[PROOFSTEP]
cases' this with h h
[GOAL]
case neg.inl
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h✝ : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬leadingCoeff P / leadingCoeff Q = 0
h : ↑(natDegree P) - ↑(natDegree Q) = 0 ∧ leadingCoeff P / leadingCoeff Q = 0
⊢ degree P < degree Q
[PROOFSTEP]
exact absurd h.2 hPQ
[GOAL]
case neg.inr
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h✝ : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬leadingCoeff P / leadingCoeff Q = 0
h : ↑(natDegree P) - ↑(natDegree Q) < 0 ∧ 0 = 0
⊢ degree P < degree Q
[PROOFSTEP]
rw [sub_lt_iff_lt_add, zero_add, Int.ofNat_lt] at h
[GOAL]
case neg.inr
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h✝ : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬leadingCoeff P / leadingCoeff Q = 0
h : natDegree P < natDegree Q ∧ 0 = 0
⊢ degree P < degree Q
[PROOFSTEP]
exact degree_lt_degree h.1
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree P = degree Q
⊢ Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 (leadingCoeff P / leadingCoeff Q))
[PROOFSTEP]
refine' (isEquivalent_atTop_div P Q).symm.tendsto_nhds _
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree P = degree Q
⊢ Tendsto (fun x => leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree P) - ↑(natDegree Q))) atTop
    (𝓝 (leadingCoeff P / leadingCoeff Q))
[PROOFSTEP]
rw [show (P.natDegree : ℤ) = Q.natDegree by simp [hdeg, natDegree]]
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree P = degree Q
⊢ ↑(natDegree P) = ↑(natDegree Q)
[PROOFSTEP]
simp [hdeg, natDegree]
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree P = degree Q
⊢ Tendsto (fun x => leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree Q) - ↑(natDegree Q))) atTop
    (𝓝 (leadingCoeff P / leadingCoeff Q))
[PROOFSTEP]
simp [tendsto_const_nhds]
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree Q < degree P
hpos : 0 < leadingCoeff P / leadingCoeff Q
⊢ Tendsto (fun x => eval x P / eval x Q) atTop atTop
[PROOFSTEP]
have hQ : Q ≠ 0 := fun h => by
  simp only [h, div_zero, leadingCoeff_zero] at hpos
  exact hpos.false
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree Q < degree P
hpos : 0 < leadingCoeff P / leadingCoeff Q
h : Q = 0
⊢ False
[PROOFSTEP]
simp only [h, div_zero, leadingCoeff_zero] at hpos
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree Q < degree P
h : Q = 0
hpos : 0 < 0
⊢ False
[PROOFSTEP]
exact hpos.false
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree Q < degree P
hpos : 0 < leadingCoeff P / leadingCoeff Q
hQ : Q ≠ 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop atTop
[PROOFSTEP]
rw [← natDegree_lt_natDegree_iff hQ] at hdeg
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree Q < natDegree P
hpos : 0 < leadingCoeff P / leadingCoeff Q
hQ : Q ≠ 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop atTop
[PROOFSTEP]
refine' (isEquivalent_atTop_div P Q).symm.tendsto_atTop _
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree Q < natDegree P
hpos : 0 < leadingCoeff P / leadingCoeff Q
hQ : Q ≠ 0
⊢ Tendsto (fun x => leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree P) - ↑(natDegree Q))) atTop atTop
[PROOFSTEP]
apply Tendsto.const_mul_atTop hpos
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree Q < natDegree P
hpos : 0 < leadingCoeff P / leadingCoeff Q
hQ : Q ≠ 0
⊢ Tendsto (fun x => x ^ (↑(natDegree P) - ↑(natDegree Q))) atTop atTop
[PROOFSTEP]
apply tendsto_zpow_atTop_atTop
[GOAL]
case hn
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree Q < natDegree P
hpos : 0 < leadingCoeff P / leadingCoeff Q
hQ : Q ≠ 0
⊢ 0 < ↑(natDegree P) - ↑(natDegree Q)
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree Q < degree P
hneg : leadingCoeff P / leadingCoeff Q < 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop atBot
[PROOFSTEP]
have hQ : Q ≠ 0 := fun h => by
  simp only [h, div_zero, leadingCoeff_zero] at hneg
  exact hneg.false
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree Q < degree P
hneg : leadingCoeff P / leadingCoeff Q < 0
h : Q = 0
⊢ False
[PROOFSTEP]
simp only [h, div_zero, leadingCoeff_zero] at hneg
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree Q < degree P
h : Q = 0
hneg : 0 < 0
⊢ False
[PROOFSTEP]
exact hneg.false
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree Q < degree P
hneg : leadingCoeff P / leadingCoeff Q < 0
hQ : Q ≠ 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop atBot
[PROOFSTEP]
rw [← natDegree_lt_natDegree_iff hQ] at hdeg
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree Q < natDegree P
hneg : leadingCoeff P / leadingCoeff Q < 0
hQ : Q ≠ 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop atBot
[PROOFSTEP]
refine' (isEquivalent_atTop_div P Q).symm.tendsto_atBot _
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree Q < natDegree P
hneg : leadingCoeff P / leadingCoeff Q < 0
hQ : Q ≠ 0
⊢ Tendsto (fun x => leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree P) - ↑(natDegree Q))) atTop atBot
[PROOFSTEP]
apply Tendsto.neg_const_mul_atTop hneg
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree Q < natDegree P
hneg : leadingCoeff P / leadingCoeff Q < 0
hQ : Q ≠ 0
⊢ Tendsto (fun x => x ^ (↑(natDegree P) - ↑(natDegree Q))) atTop atTop
[PROOFSTEP]
apply tendsto_zpow_atTop_atTop
[GOAL]
case hn
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree Q < natDegree P
hneg : leadingCoeff P / leadingCoeff Q < 0
hQ : Q ≠ 0
⊢ 0 < ↑(natDegree P) - ↑(natDegree Q)
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree Q < degree P
hQ : Q ≠ 0
⊢ Tendsto (fun x => |eval x P / eval x Q|) atTop atTop
[PROOFSTEP]
by_cases h : 0 ≤ P.leadingCoeff / Q.leadingCoeff
[GOAL]
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree Q < degree P
hQ : Q ≠ 0
h : 0 ≤ leadingCoeff P / leadingCoeff Q
⊢ Tendsto (fun x => |eval x P / eval x Q|) atTop atTop
[PROOFSTEP]
exact tendsto_abs_atTop_atTop.comp (P.div_tendsto_atTop_of_degree_gt Q hdeg hQ h)
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree Q < degree P
hQ : Q ≠ 0
h : ¬0 ≤ leadingCoeff P / leadingCoeff Q
⊢ Tendsto (fun x => |eval x P / eval x Q|) atTop atTop
[PROOFSTEP]
push_neg at h
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree Q < degree P
hQ : Q ≠ 0
h : leadingCoeff P / leadingCoeff Q < 0
⊢ Tendsto (fun x => |eval x P / eval x Q|) atTop atTop
[PROOFSTEP]
exact tendsto_abs_atBot_atTop.comp (P.div_tendsto_atBot_of_degree_gt Q hdeg hQ h.le)
[GOAL]
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : degree P ≤ degree Q
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q
[PROOFSTEP]
by_cases hp : P = 0
[GOAL]
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : degree P ≤ degree Q
hp : P = 0
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q
[PROOFSTEP]
simpa [hp] using isBigO_zero (fun x => eval x Q) atTop
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : degree P ≤ degree Q
hp : ¬P = 0
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q
[PROOFSTEP]
have hq : Q ≠ 0 := ne_zero_of_degree_ge_degree h hp
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : degree P ≤ degree Q
hp : ¬P = 0
hq : Q ≠ 0
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q
[PROOFSTEP]
have hPQ : ∀ᶠ x : 𝕜 in atTop, eval x Q = 0 → eval x P = 0 :=
  Filter.mem_of_superset (Polynomial.eventually_no_roots Q hq) fun x h h' => absurd h' h
[GOAL]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : degree P ≤ degree Q
hp : ¬P = 0
hq : Q ≠ 0
hPQ : ∀ᶠ (x : 𝕜) in atTop, eval x Q = 0 → eval x P = 0
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q
[PROOFSTEP]
cases' le_iff_lt_or_eq.mp h with h h
[GOAL]
case neg.inl
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h✝ : degree P ≤ degree Q
hp : ¬P = 0
hq : Q ≠ 0
hPQ : ∀ᶠ (x : 𝕜) in atTop, eval x Q = 0 → eval x P = 0
h : degree P < degree Q
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q
[PROOFSTEP]
exact isBigO_of_div_tendsto_nhds hPQ 0 (div_tendsto_zero_of_degree_lt P Q h)
[GOAL]
case neg.inr
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h✝ : degree P ≤ degree Q
hp : ¬P = 0
hq : Q ≠ 0
hPQ : ∀ᶠ (x : 𝕜) in atTop, eval x Q = 0 → eval x P = 0
h : degree P = degree Q
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q
[PROOFSTEP]
exact isBigO_of_div_tendsto_nhds hPQ _ (div_tendsto_leadingCoeff_div_of_degree_eq P Q h)


[GOAL]
z✝ y x✝ : ℝ
x z : ℂ
hz : ‖z‖ ≤ 1
⊢ ‖exp (x + z) - exp x - z * exp x‖ = ‖exp x * (exp z - 1 - z)‖
[PROOFSTEP]
congr
[GOAL]
case e_a
z✝ y x✝ : ℝ
x z : ℂ
hz : ‖z‖ ≤ 1
⊢ exp (x + z) - exp x - z * exp x = exp x * (exp z - 1 - z)
[PROOFSTEP]
rw [exp_add]
[GOAL]
case e_a
z✝ y x✝ : ℝ
x z : ℂ
hz : ‖z‖ ≤ 1
⊢ exp x * exp z - exp x - z * exp x = exp x * (exp z - 1 - z)
[PROOFSTEP]
ring
[GOAL]
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
⊢ ‖exp y - exp x‖ ≤ (1 + r) * ‖exp x‖ * ‖y - x‖
[PROOFSTEP]
have hy_eq : y = x + (y - x) := by abel
[GOAL]
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
⊢ y = x + (y - x)
[PROOFSTEP]
abel
[GOAL]
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
⊢ y = x + (y - x)
[PROOFSTEP]
abel
[GOAL]
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
⊢ ‖exp y - exp x‖ ≤ (1 + r) * ‖exp x‖ * ‖y - x‖
[PROOFSTEP]
have hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖ := by
  rw [pow_two]
  exact mul_le_mul hyx.le le_rfl (norm_nonneg _) hr_nonneg
[GOAL]
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
⊢ ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
[PROOFSTEP]
rw [pow_two]
[GOAL]
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
⊢ ‖y - x‖ * ‖y - x‖ ≤ r * ‖y - x‖
[PROOFSTEP]
exact mul_le_mul hyx.le le_rfl (norm_nonneg _) hr_nonneg
[GOAL]
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
⊢ ‖exp y - exp x‖ ≤ (1 + r) * ‖exp x‖ * ‖y - x‖
[PROOFSTEP]
have h_sq : ∀ z, ‖z‖ ≤ 1 → ‖exp (x + z) - exp x‖ ≤ ‖z‖ * ‖exp x‖ + ‖exp x‖ * ‖z‖ ^ 2 :=
  by
  intro z hz
  have : ‖exp (x + z) - exp x - z • exp x‖ ≤ ‖exp x‖ * ‖z‖ ^ 2 := exp_bound_sq x z hz
  rw [← sub_le_iff_le_add', ← norm_smul z]
  exact (norm_sub_norm_le _ _).trans this
[GOAL]
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
⊢ ∀ (z : ℂ), ‖z‖ ≤ 1 → ‖exp (x + z) - exp x‖ ≤ ‖z‖ * ‖exp x‖ + ‖exp x‖ * ‖z‖ ^ 2
[PROOFSTEP]
intro z hz
[GOAL]
z✝ y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
z : ℂ
hz : ‖z‖ ≤ 1
⊢ ‖exp (x + z) - exp x‖ ≤ ‖z‖ * ‖exp x‖ + ‖exp x‖ * ‖z‖ ^ 2
[PROOFSTEP]
have : ‖exp (x + z) - exp x - z • exp x‖ ≤ ‖exp x‖ * ‖z‖ ^ 2 := exp_bound_sq x z hz
[GOAL]
z✝ y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
z : ℂ
hz : ‖z‖ ≤ 1
this : ‖exp (x + z) - exp x - z • exp x‖ ≤ ‖exp x‖ * ‖z‖ ^ 2
⊢ ‖exp (x + z) - exp x‖ ≤ ‖z‖ * ‖exp x‖ + ‖exp x‖ * ‖z‖ ^ 2
[PROOFSTEP]
rw [← sub_le_iff_le_add', ← norm_smul z]
[GOAL]
z✝ y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
z : ℂ
hz : ‖z‖ ≤ 1
this : ‖exp (x + z) - exp x - z • exp x‖ ≤ ‖exp x‖ * ‖z‖ ^ 2
⊢ ‖exp (x + z) - exp x‖ - ‖z • exp x‖ ≤ ‖exp x‖ * ‖z‖ ^ 2
[PROOFSTEP]
exact (norm_sub_norm_le _ _).trans this
[GOAL]
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
h_sq : ∀ (z : ℂ), ‖z‖ ≤ 1 → ‖exp (x + z) - exp x‖ ≤ ‖z‖ * ‖exp x‖ + ‖exp x‖ * ‖z‖ ^ 2
⊢ ‖exp y - exp x‖ ≤ (1 + r) * ‖exp x‖ * ‖y - x‖
[PROOFSTEP]
calc
  ‖exp y - exp x‖ = ‖exp (x + (y - x)) - exp x‖ := by nth_rw 1 [hy_eq]
  _ ≤ ‖y - x‖ * ‖exp x‖ + ‖exp x‖ * ‖y - x‖ ^ 2 := (h_sq (y - x) (hyx.le.trans hr_le))
  _ ≤ ‖y - x‖ * ‖exp x‖ + ‖exp x‖ * (r * ‖y - x‖) :=
    (add_le_add_left (mul_le_mul le_rfl hyx_sq_le (sq_nonneg _) (norm_nonneg _)) _)
  _ = (1 + r) * ‖exp x‖ * ‖y - x‖ := by ring
[GOAL]
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
h_sq : ∀ (z : ℂ), ‖z‖ ≤ 1 → ‖exp (x + z) - exp x‖ ≤ ‖z‖ * ‖exp x‖ + ‖exp x‖ * ‖z‖ ^ 2
⊢ ‖exp y - exp x‖ = ‖exp (x + (y - x)) - exp x‖
[PROOFSTEP]
nth_rw 1 [hy_eq]
[GOAL]
z y✝ x✝ r : ℝ
hr_nonneg : 0 ≤ r
hr_le : r ≤ 1
x y : ℂ
hyx : ‖y - x‖ < r
hy_eq : y = x + (y - x)
hyx_sq_le : ‖y - x‖ ^ 2 ≤ r * ‖y - x‖
h_sq : ∀ (z : ℂ), ‖z‖ ≤ 1 → ‖exp (x + z) - exp x‖ ≤ ‖z‖ * ‖exp x‖ + ‖exp x‖ * ‖z‖ ^ 2
⊢ ‖y - x‖ * ‖exp x‖ + ‖exp x‖ * (r * ‖y - x‖) = (1 + r) * ‖exp x‖ * ‖y - x‖
[PROOFSTEP]
ring
[GOAL]
z y✝ x✝ : ℝ
x y : ℂ
⊢ dist y x < 1 → dist (exp y) (exp x) ≤ 2 * ‖exp x‖ * dist y x
[PROOFSTEP]
convert locally_lipschitz_exp zero_le_one le_rfl x y using 2
[GOAL]
case h'.h.e'_4
z y✝ x✝ : ℝ
x y : ℂ
a✝ : ‖y - x‖ < 1
⊢ 2 * ‖exp x‖ * dist y x = (1 + 1) * ‖exp x‖ * ‖y - x‖
[PROOFSTEP]
congr
[GOAL]
case h'.h.e'_4.e_a.e_a
z y✝ x✝ : ℝ
x y : ℂ
a✝ : ‖y - x‖ < 1
⊢ 2 = 1 + 1
[PROOFSTEP]
ring
[GOAL]
α : Type u_1
x✝ y z : ℝ
l : Filter α
x : ℝ
⊢ exp (x / 2) = sqrt (exp x)
[PROOFSTEP]
rw [eq_comm, sqrt_eq_iff_sq_eq, sq, ← exp_add, add_halves]
[GOAL]
case hx
α : Type u_1
x✝ y z : ℝ
l : Filter α
x : ℝ
⊢ 0 ≤ exp x
[PROOFSTEP]
exact (exp_pos _).le
[GOAL]
case hy
α : Type u_1
x✝ y z : ℝ
l : Filter α
x : ℝ
⊢ 0 ≤ exp (x / 2)
[PROOFSTEP]
exact (exp_pos _).le
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
⊢ Tendsto exp atTop atTop
[PROOFSTEP]
have A : Tendsto (fun x : ℝ => x + 1) atTop atTop := tendsto_atTop_add_const_right atTop 1 tendsto_id
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
A : Tendsto (fun x => x + 1) atTop atTop
⊢ Tendsto exp atTop atTop
[PROOFSTEP]
have B : ∀ᶠ x in atTop, x + 1 ≤ exp x := eventually_atTop.2 ⟨0, fun x _ => add_one_le_exp x⟩
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
A : Tendsto (fun x => x + 1) atTop atTop
B : ∀ᶠ (x : ℝ) in atTop, x + 1 ≤ exp x
⊢ Tendsto exp atTop atTop
[PROOFSTEP]
exact tendsto_atTop_mono' atTop B A
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
⊢ Tendsto exp (𝓝 0) (𝓝 1)
[PROOFSTEP]
convert continuous_exp.tendsto 0
[GOAL]
case h.e'_5.h.e'_3
α : Type u_1
x y z : ℝ
l : Filter α
⊢ 1 = exp 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
n : ℕ
⊢ Tendsto (fun x => exp x / x ^ n) atTop atTop
[PROOFSTEP]
refine' (atTop_basis_Ioi.tendsto_iff (atTop_basis' 1)).2 fun C hC₁ => _
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
⊢ ∃ ia, True ∧ ∀ (x : ℝ), x ∈ Set.Ioi ia → exp x / x ^ n ∈ Set.Ici C
[PROOFSTEP]
have hC₀ : 0 < C := zero_lt_one.trans_le hC₁
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
⊢ ∃ ia, True ∧ ∀ (x : ℝ), x ∈ Set.Ioi ia → exp x / x ^ n ∈ Set.Ici C
[PROOFSTEP]
have : 0 < (exp 1 * C)⁻¹ := inv_pos.2 (mul_pos (exp_pos _) hC₀)
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (exp 1 * C)⁻¹
⊢ ∃ ia, True ∧ ∀ (x : ℝ), x ∈ Set.Ioi ia → exp x / x ^ n ∈ Set.Ici C
[PROOFSTEP]
obtain ⟨N, hN⟩ : ∃ N : ℕ, ∀ k ≥ N, (↑k : ℝ) ^ n / exp 1 ^ k < (exp 1 * C)⁻¹ :=
  eventually_atTop.1
    ((tendsto_pow_const_div_const_pow_of_one_lt n (one_lt_exp_iff.2 zero_lt_one)).eventually (gt_mem_nhds this))
[GOAL]
case intro
α : Type u_1
x y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (exp 1 * C)⁻¹
N : ℕ
hN : ∀ (k : ℕ), k ≥ N → ↑k ^ n / exp 1 ^ k < (exp 1 * C)⁻¹
⊢ ∃ ia, True ∧ ∀ (x : ℝ), x ∈ Set.Ioi ia → exp x / x ^ n ∈ Set.Ici C
[PROOFSTEP]
simp only [← exp_nat_mul, mul_one, div_lt_iff, exp_pos, ← div_eq_inv_mul] at hN
[GOAL]
case intro
α : Type u_1
x y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (exp 1 * C)⁻¹
N : ℕ
hN : ∀ (k : ℕ), k ≥ N → ↑k ^ n < exp ↑k / (exp 1 * C)
⊢ ∃ ia, True ∧ ∀ (x : ℝ), x ∈ Set.Ioi ia → exp x / x ^ n ∈ Set.Ici C
[PROOFSTEP]
refine' ⟨N, trivial, fun x hx => _⟩
[GOAL]
case intro
α : Type u_1
x✝ y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (exp 1 * C)⁻¹
N : ℕ
hN : ∀ (k : ℕ), k ≥ N → ↑k ^ n < exp ↑k / (exp 1 * C)
x : ℝ
hx : x ∈ Set.Ioi ↑N
⊢ exp x / x ^ n ∈ Set.Ici C
[PROOFSTEP]
rw [Set.mem_Ioi] at hx
[GOAL]
case intro
α : Type u_1
x✝ y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (exp 1 * C)⁻¹
N : ℕ
hN : ∀ (k : ℕ), k ≥ N → ↑k ^ n < exp ↑k / (exp 1 * C)
x : ℝ
hx : ↑N < x
⊢ exp x / x ^ n ∈ Set.Ici C
[PROOFSTEP]
have hx₀ : 0 < x := (Nat.cast_nonneg N).trans_lt hx
[GOAL]
case intro
α : Type u_1
x✝ y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (exp 1 * C)⁻¹
N : ℕ
hN : ∀ (k : ℕ), k ≥ N → ↑k ^ n < exp ↑k / (exp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ exp x / x ^ n ∈ Set.Ici C
[PROOFSTEP]
rw [Set.mem_Ici, le_div_iff (pow_pos hx₀ _), ← le_div_iff' hC₀]
[GOAL]
case intro
α : Type u_1
x✝ y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (exp 1 * C)⁻¹
N : ℕ
hN : ∀ (k : ℕ), k ≥ N → ↑k ^ n < exp ↑k / (exp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ x ^ n ≤ exp x / C
[PROOFSTEP]
calc
  x ^ n ≤ ⌈x⌉₊ ^ n := by exact_mod_cast pow_le_pow_of_le_left hx₀.le (Nat.le_ceil _) _
  _ ≤ exp ⌈x⌉₊ / (exp 1 * C) := by exact_mod_cast (hN _ (Nat.lt_ceil.2 hx).le).le
  _ ≤ exp (x + 1) / (exp 1 * C) :=
    (div_le_div_of_le (mul_pos (exp_pos _) hC₀).le (exp_le_exp.2 <| (Nat.ceil_lt_add_one hx₀.le).le))
  _ = exp x / C := by rw [add_comm, exp_add, mul_div_mul_left _ _ (exp_pos _).ne']
[GOAL]
α : Type u_1
x✝ y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (exp 1 * C)⁻¹
N : ℕ
hN : ∀ (k : ℕ), k ≥ N → ↑k ^ n < exp ↑k / (exp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ x ^ n ≤ ↑(⌈x⌉₊ ^ n)
[PROOFSTEP]
exact_mod_cast pow_le_pow_of_le_left hx₀.le (Nat.le_ceil _) _
[GOAL]
α : Type u_1
x✝ y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (exp 1 * C)⁻¹
N : ℕ
hN : ∀ (k : ℕ), k ≥ N → ↑k ^ n < exp ↑k / (exp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ ↑(⌈x⌉₊ ^ n) ≤ exp ↑⌈x⌉₊ / (exp 1 * C)
[PROOFSTEP]
exact_mod_cast (hN _ (Nat.lt_ceil.2 hx).le).le
[GOAL]
α : Type u_1
x✝ y z : ℝ
l : Filter α
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (exp 1 * C)⁻¹
N : ℕ
hN : ∀ (k : ℕ), k ≥ N → ↑k ^ n < exp ↑k / (exp 1 * C)
x : ℝ
hx : ↑N < x
hx₀ : 0 < x
⊢ exp (x + 1) / (exp 1 * C) = exp x / C
[PROOFSTEP]
rw [add_comm, exp_add, mul_div_mul_left _ _ (exp_pos _).ne']
[GOAL]
α : Type u_1
x✝ y z : ℝ
l : Filter α
n : ℕ
x : ℝ
⊢ ((fun r => r⁻¹) ∘ fun x => exp x / x ^ n) x = x ^ n * exp (-x)
[PROOFSTEP]
rw [comp_apply, inv_eq_one_div, div_div_eq_mul_div, one_mul, div_eq_mul_inv, exp_neg]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 < b
⊢ Tendsto (fun x => (b * exp x + c) / x ^ n) atTop atTop
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn)
[GOAL]
case inl
α : Type u_1
x y z : ℝ
l : Filter α
b c : ℝ
hb : 0 < b
⊢ Tendsto (fun x => (b * exp x + c) / x ^ 0) atTop atTop
[PROOFSTEP]
simp only [pow_zero, div_one]
[GOAL]
case inl
α : Type u_1
x y z : ℝ
l : Filter α
b c : ℝ
hb : 0 < b
⊢ Tendsto (fun x => b * exp x + c) atTop atTop
[PROOFSTEP]
exact (tendsto_exp_atTop.const_mul_atTop hb).atTop_add tendsto_const_nhds
[GOAL]
case inr
α : Type u_1
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 < b
hn : n ≠ 0
⊢ Tendsto (fun x => (b * exp x + c) / x ^ n) atTop atTop
[PROOFSTEP]
simp only [add_div, mul_div_assoc]
[GOAL]
case inr
α : Type u_1
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 < b
hn : n ≠ 0
⊢ Tendsto (fun x => b * (exp x / x ^ n) + c / x ^ n) atTop atTop
[PROOFSTEP]
exact ((tendsto_exp_div_pow_atTop n).const_mul_atTop hb).atTop_add (tendsto_const_nhds.div_atTop (tendsto_pow_atTop hn))
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
⊢ Tendsto (fun x => x ^ n / (b * exp x + c)) atTop (𝓝 0)
[PROOFSTEP]
have H : ∀ d e, 0 < d → Tendsto (fun x : ℝ => x ^ n / (d * exp x + e)) atTop (𝓝 0) :=
  by
  intro b' c' h
  convert (tendsto_mul_exp_add_div_pow_atTop b' c' n h).inv_tendsto_atTop using 1
  ext x
  simp
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
⊢ ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * exp x + e)) atTop (𝓝 0)
[PROOFSTEP]
intro b' c' h
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
b' c' : ℝ
h : 0 < b'
⊢ Tendsto (fun x => x ^ n / (b' * exp x + c')) atTop (𝓝 0)
[PROOFSTEP]
convert (tendsto_mul_exp_add_div_pow_atTop b' c' n h).inv_tendsto_atTop using 1
[GOAL]
case h.e'_3
α : Type u_1
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
b' c' : ℝ
h : 0 < b'
⊢ (fun x => x ^ n / (b' * exp x + c')) = (fun x => (b' * exp x + c') / x ^ n)⁻¹
[PROOFSTEP]
ext x
[GOAL]
case h.e'_3.h
α : Type u_1
x✝ y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
b' c' : ℝ
h : 0 < b'
x : ℝ
⊢ x ^ n / (b' * exp x + c') = (fun x => (b' * exp x + c') / x ^ n)⁻¹ x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * exp x + e)) atTop (𝓝 0)
⊢ Tendsto (fun x => x ^ n / (b * exp x + c)) atTop (𝓝 0)
[PROOFSTEP]
cases' lt_or_gt_of_ne hb with h h
[GOAL]
case inl
α : Type u_1
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * exp x + e)) atTop (𝓝 0)
h : 0 < b
⊢ Tendsto (fun x => x ^ n / (b * exp x + c)) atTop (𝓝 0)
[PROOFSTEP]
exact H b c h
[GOAL]
case inr
α : Type u_1
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * exp x + e)) atTop (𝓝 0)
h : 0 > b
⊢ Tendsto (fun x => x ^ n / (b * exp x + c)) atTop (𝓝 0)
[PROOFSTEP]
convert (H (-b) (-c) (neg_pos.mpr h)).neg using 1
[GOAL]
case h.e'_3
α : Type u_1
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * exp x + e)) atTop (𝓝 0)
h : 0 > b
⊢ (fun x => x ^ n / (b * exp x + c)) = fun x => -(x ^ n / (-b * exp x + -c))
[PROOFSTEP]
ext x
[GOAL]
case h.e'_3.h
α : Type u_1
x✝ y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * exp x + e)) atTop (𝓝 0)
h : 0 > b
x : ℝ
⊢ x ^ n / (b * exp x + c) = -(x ^ n / (-b * exp x + -c))
[PROOFSTEP]
field_simp
[GOAL]
case h.e'_3.h
α : Type u_1
x✝ y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * exp x + e)) atTop (𝓝 0)
h : 0 > b
x : ℝ
⊢ x ^ n / (b * exp x + c) = -x ^ n / (-(b * exp x) + -c)
[PROOFSTEP]
rw [← neg_add (b * exp x) c, neg_div_neg_eq]
[GOAL]
case h.e'_5
α : Type u_1
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * exp x + e)) atTop (𝓝 0)
h : 0 > b
⊢ 𝓝 0 = 𝓝 (-0)
[PROOFSTEP]
rw [neg_zero]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
⊢ Tendsto (fun x => { val := exp x, property := (_ : 0 < exp x) }) atTop atTop
[PROOFSTEP]
simp only [tendsto_Ioi_atTop, Subtype.coe_mk, tendsto_exp_atTop]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
⊢ Tendsto (fun x => { val := exp x, property := (_ : 0 < exp x) }) atBot atBot
[PROOFSTEP]
simp [tendsto_exp_atBot_nhdsWithin]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
⊢ Set.range exp = Set.Ioi 0
[PROOFSTEP]
rw [← coe_comp_expOrderIso, range_comp, expOrderIso.range_eq, image_univ, Subtype.range_coe]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
⊢ Filter.map exp atTop = atTop
[PROOFSTEP]
rw [← coe_comp_expOrderIso, ← Filter.map_map, OrderIso.map_atTop, map_val_Ioi_atTop]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
⊢ comap exp atTop = atTop
[PROOFSTEP]
rw [← map_exp_atTop, comap_map exp_injective, map_exp_atTop]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
f : α → ℝ
⊢ Tendsto (fun x => exp (f x)) l atTop ↔ Tendsto f l atTop
[PROOFSTEP]
simp_rw [← comp_apply (f := exp), ← tendsto_comap_iff, comap_exp_atTop]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
f : ℝ → α
⊢ Tendsto (fun x => f (exp x)) atTop l ↔ Tendsto f atTop l
[PROOFSTEP]
simp_rw [← comp_apply (g := exp), ← tendsto_map'_iff, map_exp_atTop]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
⊢ Filter.map exp atBot = 𝓝[Set.Ioi 0] 0
[PROOFSTEP]
rw [← coe_comp_expOrderIso, ← Filter.map_map, expOrderIso.map_atBot, ← map_coe_Ioi_atBot]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
⊢ comap exp (𝓝[Set.Ioi 0] 0) = atBot
[PROOFSTEP]
rw [← map_exp_atBot, comap_map exp_injective]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
f : ℝ → α
⊢ Tendsto (fun x => f (exp x)) atBot l ↔ Tendsto f (𝓝[Set.Ioi 0] 0) l
[PROOFSTEP]
rw [← map_exp_atBot, tendsto_map'_iff]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
f : ℝ → α
⊢ Tendsto (fun x => f (exp x)) atBot l ↔ Tendsto (f ∘ exp) atBot l
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
⊢ comap exp (𝓝[Set.range exp] 0) = atBot
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
f : α → ℝ
⊢ Tendsto (fun x => exp (f x)) l (𝓝 0) ↔ Tendsto f l atBot
[PROOFSTEP]
simp_rw [← comp_apply (f := exp), ← tendsto_comap_iff, comap_exp_nhds_zero]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
n : ℕ
⊢ (fun x => x ^ n) =o[atTop] exp
[PROOFSTEP]
simpa [isLittleO_iff_tendsto fun x hx => ((exp_pos x).ne' hx).elim] using
  tendsto_div_pow_mul_exp_add_atTop 1 0 n zero_ne_one
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
f g : α → ℝ
⊢ (IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => ‖exp (f x)‖ / ‖exp (g x)‖) ↔
    IsBoundedUnder (fun x x_1 => x ≤ x_1) l (f - g)
[PROOFSTEP]
simp only [norm_eq_abs, abs_exp, ← exp_sub, isBoundedUnder_le_exp_comp, Pi.sub_def]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
f g : α → ℝ
⊢ ((fun x => exp (f x)) =Θ[l] fun x => exp (g x)) ↔ IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => |f x - g x|
[PROOFSTEP]
simp only [isBoundedUnder_le_abs, ← isBoundedUnder_le_neg, neg_sub, IsTheta, isBigO_exp_comp_exp_comp, Pi.sub_def]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
f g : α → ℝ
⊢ ((fun x => exp (f x)) =o[l] fun x => exp (g x)) ↔ Tendsto (fun x => g x - f x) l atTop
[PROOFSTEP]
simp only [isLittleO_iff_tendsto, exp_ne_zero, ← exp_sub, ← tendsto_neg_atTop_iff, false_imp_iff, imp_true_iff,
  tendsto_exp_comp_nhds_zero, neg_sub]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
f : α → ℝ
⊢ ((fun x => 1) =o[l] fun x => exp (f x)) ↔ Tendsto f l atTop
[PROOFSTEP]
simp only [← exp_zero, isLittleO_exp_comp_exp_comp, sub_zero]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
f : α → ℝ
⊢ ((fun x => 1) =O[l] fun x => exp (f x)) ↔ IsBoundedUnder (fun x x_1 => x ≥ x_1) l f
[PROOFSTEP]
simp only [← exp_zero, isBigO_exp_comp_exp_comp, Pi.sub_def, zero_sub, isBoundedUnder_le_neg]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
f : α → ℝ
⊢ ((fun x => exp (f x)) =O[l] fun x => 1) ↔ IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
[PROOFSTEP]
simp only [isBigO_one_iff, norm_eq_abs, abs_exp, isBoundedUnder_le_exp_comp]
[GOAL]
α : Type u_1
x y z : ℝ
l : Filter α
f : α → ℝ
⊢ ((fun x => exp (f x)) =Θ[l] fun x => 1) ↔ IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => |f x|
[PROOFSTEP]
simp only [← exp_zero, isTheta_exp_comp_exp_comp, sub_zero]
[GOAL]
⊢ comap exp (comap (↑abs) atTop) = comap re (comap Real.exp atTop)
[PROOFSTEP]
simp only [comap_comap, (· ∘ ·), abs_exp]
[GOAL]
⊢ comap re (comap Real.exp atTop) = comap re atTop
[PROOFSTEP]
rw [Real.comap_exp_atTop]
[GOAL]
⊢ comap exp (𝓝 0) = comap re (comap Real.exp (𝓝 0))
[PROOFSTEP]
simp only [comap_comap, ← comap_abs_nhds_zero, (· ∘ ·), abs_exp]
[GOAL]
⊢ comap re (comap Real.exp (𝓝 0)) = comap re atBot
[PROOFSTEP]
rw [Real.comap_exp_nhds_zero]
[GOAL]
⊢ comap exp (𝓝[{0}ᶜ] 0) = comap re atBot
[PROOFSTEP]
have : (exp ⁻¹' {0})ᶜ = Set.univ := eq_univ_of_forall exp_ne_zero
[GOAL]
this : (exp ⁻¹' {0})ᶜ = Set.univ
⊢ comap exp (𝓝[{0}ᶜ] 0) = comap re atBot
[PROOFSTEP]
simp [nhdsWithin, comap_exp_nhds_zero, this]
[GOAL]
α : Type u_1
l : Filter α
f : α → ℂ
⊢ Tendsto (fun x => exp (f x)) l (𝓝 0) ↔ Tendsto (fun x => (f x).re) l atBot
[PROOFSTEP]
simp_rw [← comp_apply (f := exp), ← tendsto_comap_iff, comap_exp_nhds_zero, tendsto_comap_iff]
[GOAL]
α : Type u_1
l : Filter α
f : α → ℂ
⊢ Tendsto (re ∘ f) l atBot ↔ Tendsto (fun x => (f x).re) l atBot
[PROOFSTEP]
rfl