[GOAL]
α : Type u_1
E : Type u_2
inst✝ : SeminormedAddCommGroup E
s t : Set α
f✝ : α → E
a✝ : α
h : s ⊆ t
f : α → E
a : α
⊢ ‖indicator s f a‖ ≤ ‖indicator t f a‖
[PROOFSTEP]
simp only [norm_indicator_eq_indicator_norm]
[GOAL]
α : Type u_1
E : Type u_2
inst✝ : SeminormedAddCommGroup E
s t : Set α
f✝ : α → E
a✝ : α
h : s ⊆ t
f : α → E
a : α
⊢ indicator s (fun a => ‖f a‖) a ≤ indicator t (fun a => ‖f a‖) a
[PROOFSTEP]
exact indicator_le_indicator_of_subset ‹_› (fun _ => norm_nonneg _) _
[GOAL]
α : Type u_1
E : Type u_2
inst✝ : SeminormedAddCommGroup E
s t : Set α
f : α → E
a : α
⊢ ‖indicator s f a‖ ≤ ‖f a‖
[PROOFSTEP]
rw [norm_indicator_eq_indicator_norm]
[GOAL]
α : Type u_1
E : Type u_2
inst✝ : SeminormedAddCommGroup E
s t : Set α
f : α → E
a : α
⊢ indicator s (fun a => ‖f a‖) a ≤ ‖f a‖
[PROOFSTEP]
apply indicator_norm_le_norm_self


[GOAL]
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
G' : Type u_5
inst✝⁴ : NormedAddCommGroup G'
inst✝³ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
φ : (i : ι) → E → F' i
φ' : (i : ι) → E →L[𝕜] F' i
Φ : E → (i : ι) → F' i
Φ' : E →L[𝕜] (i : ι) → F' i
⊢ HasStrictFDerivAt Φ Φ' x ↔ ∀ (i : ι), HasStrictFDerivAt (fun x => Φ x i) (comp (proj i) Φ') x
[PROOFSTEP]
simp only [HasStrictFDerivAt, ContinuousLinearMap.coe_pi]
[GOAL]
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
G' : Type u_5
inst✝⁴ : NormedAddCommGroup G'
inst✝³ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
φ : (i : ι) → E → F' i
φ' : (i : ι) → E →L[𝕜] F' i
Φ : E → (i : ι) → F' i
Φ' : E →L[𝕜] (i : ι) → F' i
⊢ ((fun p => Φ p.fst - Φ p.snd - ↑Φ' (p.fst - p.snd)) =o[𝓝 (x, x)] fun p => p.fst - p.snd) ↔
    ∀ (i : ι),
      (fun p => Φ p.fst i - Φ p.snd i - ↑(comp (proj i) Φ') (p.fst - p.snd)) =o[𝓝 (x, x)] fun p => p.fst - p.snd
[PROOFSTEP]
exact isLittleO_pi
[GOAL]
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
G' : Type u_5
inst✝⁴ : NormedAddCommGroup G'
inst✝³ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
φ : (i : ι) → E → F' i
φ' : (i : ι) → E →L[𝕜] F' i
Φ : E → (i : ι) → F' i
Φ' : E →L[𝕜] (i : ι) → F' i
⊢ HasFDerivAtFilter Φ Φ' x L ↔ ∀ (i : ι), HasFDerivAtFilter (fun x => Φ x i) (comp (proj i) Φ') x L
[PROOFSTEP]
simp only [HasFDerivAtFilter, ContinuousLinearMap.coe_pi]
[GOAL]
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
G' : Type u_5
inst✝⁴ : NormedAddCommGroup G'
inst✝³ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
φ : (i : ι) → E → F' i
φ' : (i : ι) → E →L[𝕜] F' i
Φ : E → (i : ι) → F' i
Φ' : E →L[𝕜] (i : ι) → F' i
⊢ ((fun x' => Φ x' - Φ x - ↑Φ' (x' - x)) =o[L] fun x' => x' - x) ↔
    ∀ (i : ι), (fun x' => Φ x' i - Φ x i - ↑(comp (proj i) Φ') (x' - x)) =o[L] fun x' => x' - x
[PROOFSTEP]
exact isLittleO_pi


[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
C : ℝ
⊢ Tendsto (fun n => C / ↑n) atTop (𝓝 0)
[PROOFSTEP]
simpa only [mul_zero] using tendsto_const_nhds.mul tendsto_inverse_atTop_nhds_0_nat
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
⊢ Tendsto (fun n => (↑n)⁻¹) atTop (𝓝 0)
[PROOFSTEP]
rw [← NNReal.tendsto_coe]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
⊢ Tendsto (fun a => ↑(↑a)⁻¹) atTop (𝓝 ↑0)
[PROOFSTEP]
exact _root_.tendsto_inverse_atTop_nhds_0_nat
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
C : ℝ≥0
⊢ Tendsto (fun n => C / ↑n) atTop (𝓝 0)
[PROOFSTEP]
simpa using tendsto_const_nhds.mul NNReal.tendsto_inverse_atTop_nhds_0_nat
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
this : Tendsto (fun n => 1 / ↑(n + 1)) atTop (𝓝 0)
⊢ Tendsto (fun n => 1 / (↑n + 1)) atTop (𝓝 0)
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝⁴ : Semiring 𝕜
inst✝³ : Algebra ℝ≥0 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : TopologicalSemiring 𝕜
inst✝ : ContinuousSMul ℝ≥0 𝕜
⊢ Tendsto (↑(algebraMap ℝ≥0 𝕜) ∘ fun n => (↑n)⁻¹) atTop (𝓝 0)
[PROOFSTEP]
convert (continuous_algebraMap ℝ≥0 𝕜).continuousAt.tendsto.comp tendsto_inverse_atTop_nhds_0_nat
[GOAL]
case h.e'_5.h.e'_3
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝⁴ : Semiring 𝕜
inst✝³ : Algebra ℝ≥0 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : TopologicalSemiring 𝕜
inst✝ : ContinuousSMul ℝ≥0 𝕜
⊢ 0 = ↑(algebraMap ℝ≥0 𝕜) 0
[PROOFSTEP]
rw [map_zero]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
⊢ Tendsto (fun n => ↑n / (↑n + x)) atTop (𝓝 1)
[PROOFSTEP]
refine' Tendsto.congr' ((eventually_ne_atTop 0).mp (eventually_of_forall fun n hn => _)) _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
⊢ ℕ → 𝕜
[PROOFSTEP]
exact fun n : ℕ => 1 / (1 + x / n)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
n : ℕ
hn : n ≠ 0
⊢ 1 / (1 + x / ↑n) = (fun n => ↑n / (↑n + x)) n
[PROOFSTEP]
field_simp [Nat.cast_ne_zero.mpr hn]
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
⊢ Tendsto (fun n => 1 / (1 + x / ↑n)) atTop (𝓝 1)
[PROOFSTEP]
have : 𝓝 (1 : 𝕜) = 𝓝 (1 / (1 + x * (0 : 𝕜))) := by rw [mul_zero, add_zero, div_one]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
⊢ 𝓝 1 = 𝓝 (1 / (1 + x * 0))
[PROOFSTEP]
rw [mul_zero, add_zero, div_one]
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
⊢ Tendsto (fun n => 1 / (1 + x / ↑n)) atTop (𝓝 1)
[PROOFSTEP]
rw [this]
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
⊢ Tendsto (fun n => 1 / (1 + x / ↑n)) atTop (𝓝 (1 / (1 + x * 0)))
[PROOFSTEP]
refine' tendsto_const_nhds.div (tendsto_const_nhds.add _) (by simp)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
⊢ 1 + x * 0 ≠ 0
[PROOFSTEP]
simp
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
⊢ Tendsto (fun n => x / ↑n) atTop (𝓝 (x * 0))
[PROOFSTEP]
simp_rw [div_eq_mul_inv]
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
⊢ Tendsto (fun n => x * (↑n)⁻¹) atTop (𝓝 (x * 0))
[PROOFSTEP]
refine' tendsto_const_nhds.mul _
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
⊢ Tendsto (fun n => (↑n)⁻¹) atTop (𝓝 0)
[PROOFSTEP]
have := ((continuous_algebraMap ℝ 𝕜).tendsto _).comp tendsto_inverse_atTop_nhds_0_nat
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this✝ : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
this : Tendsto (↑(algebraMap ℝ 𝕜) ∘ fun n => (↑n)⁻¹) atTop (𝓝 (↑(algebraMap ℝ 𝕜) 0))
⊢ Tendsto (fun n => (↑n)⁻¹) atTop (𝓝 0)
[PROOFSTEP]
rw [map_zero, Filter.tendsto_atTop'] at this
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this✝ : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
this : ∀ (s : Set 𝕜), s ∈ 𝓝 0 → ∃ a, ∀ (b : ℕ), b ≥ a → (↑(algebraMap ℝ 𝕜) ∘ fun n => (↑n)⁻¹) b ∈ s
⊢ Tendsto (fun n => (↑n)⁻¹) atTop (𝓝 0)
[PROOFSTEP]
refine' Iff.mpr tendsto_atTop' _
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this✝ : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
this : ∀ (s : Set 𝕜), s ∈ 𝓝 0 → ∃ a, ∀ (b : ℕ), b ≥ a → (↑(algebraMap ℝ 𝕜) ∘ fun n => (↑n)⁻¹) b ∈ s
⊢ ∀ (s : Set 𝕜), s ∈ 𝓝 0 → ∃ a, ∀ (b : ℕ), b ≥ a → (↑b)⁻¹ ∈ s
[PROOFSTEP]
intros
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝⁵ : DivisionRing 𝕜
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : CharZero 𝕜
inst✝² : Algebra ℝ 𝕜
inst✝¹ : ContinuousSMul ℝ 𝕜
inst✝ : TopologicalDivisionRing 𝕜
x : 𝕜
this✝ : 𝓝 1 = 𝓝 (1 / (1 + x * 0))
this : ∀ (s : Set 𝕜), s ∈ 𝓝 0 → ∃ a, ∀ (b : ℕ), b ≥ a → (↑(algebraMap ℝ 𝕜) ∘ fun n => (↑n)⁻¹) b ∈ s
s✝ : Set 𝕜
a✝ : s✝ ∈ 𝓝 0
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → (↑b)⁻¹ ∈ s✝
[PROOFSTEP]
simp_all only [comp_apply, map_inv₀, map_natCast]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h₁ : 0 ≤ r
h₂ : r < 1
hr : 0 = r
⊢ Tendsto (fun n => r ^ (n + 1)) atTop (𝓝 0)
[PROOFSTEP]
simp [_root_.pow_succ, ← hr, tendsto_const_nhds]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h₁ : 0 ≤ r
h₂ : r < 1
hr : 0 < r
this : Tendsto (fun n => r⁻¹ ^ n) atTop atTop
n : ℕ
⊢ ((fun r => r⁻¹) ∘ fun n => r⁻¹ ^ n) n = r ^ n
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
⊢ Tendsto (fun n => r ^ n) atTop (𝓝 0) ↔ |r| < 1
[PROOFSTEP]
rw [tendsto_zero_iff_abs_tendsto_zero]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
⊢ Tendsto (abs ∘ fun n => r ^ n) atTop (𝓝 0) ↔ |r| < 1
[PROOFSTEP]
refine ⟨fun h ↦ by_contra (fun hr_le ↦ ?_), fun h ↦ ?_⟩
[GOAL]
case refine_1
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n => r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
⊢ False
[PROOFSTEP]
by_cases hr : 1 = |r|
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n => r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : 1 = |r|
⊢ False
[PROOFSTEP]
replace h : Tendsto (fun n : ℕ ↦ |r| ^ n) atTop (𝓝 0) := by simpa only [← abs_pow, h]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n => r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : 1 = |r|
⊢ Tendsto (fun n => |r| ^ n) atTop (𝓝 0)
[PROOFSTEP]
simpa only [← abs_pow, h]
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
hr_le : ¬|r| < 1
hr : 1 = |r|
h : Tendsto (fun n => |r| ^ n) atTop (𝓝 0)
⊢ False
[PROOFSTEP]
simp only [hr.symm, one_pow] at h
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
hr_le : ¬|r| < 1
hr : 1 = |r|
h : Tendsto (fun n => 1) atTop (𝓝 0)
⊢ False
[PROOFSTEP]
exact zero_ne_one <| tendsto_nhds_unique h tendsto_const_nhds
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n => r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : ¬1 = |r|
⊢ False
[PROOFSTEP]
apply @not_tendsto_nhds_of_tendsto_atTop 𝕜 ℕ _ _ _ _ atTop _ (fun n ↦ |r| ^ n) _ 0 _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n => r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : ¬1 = |r|
⊢ Tendsto (fun n => |r| ^ n) atTop atTop
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n => r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : ¬1 = |r|
⊢ Tendsto (fun n => |r| ^ n) atTop (𝓝 0)
[PROOFSTEP]
refine (pow_strictMono_right $ lt_of_le_of_ne (le_of_not_lt hr_le) hr).monotone.tendsto_atTop_atTop (fun b ↦ ?_)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n => r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : ¬1 = |r|
b : 𝕜
⊢ ∃ a, b ≤ |r| ^ a
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n => r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : ¬1 = |r|
⊢ Tendsto (fun n => |r| ^ n) atTop (𝓝 0)
[PROOFSTEP]
obtain ⟨n, hn⟩ := (pow_unbounded_of_one_lt b (lt_of_le_of_ne (le_of_not_lt hr_le) hr))
[GOAL]
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n => r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : ¬1 = |r|
b : 𝕜
n : ℕ
hn : b < |r| ^ n
⊢ ∃ a, b ≤ |r| ^ a
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n => r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : ¬1 = |r|
⊢ Tendsto (fun n => |r| ^ n) atTop (𝓝 0)
[PROOFSTEP]
exacts [⟨n, le_of_lt hn⟩, by simpa only [← abs_pow]]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : Tendsto (abs ∘ fun n => r ^ n) atTop (𝓝 0)
hr_le : ¬|r| < 1
hr : ¬1 = |r|
⊢ Tendsto (fun n => |r| ^ n) atTop (𝓝 0)
[PROOFSTEP]
simpa only [← abs_pow]
[GOAL]
case refine_2
α : Type u_1
β : Type u_2
ι : Type u_3
𝕜 : Type u_4
inst✝³ : LinearOrderedField 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
r : 𝕜
h : |r| < 1
⊢ Tendsto (abs ∘ fun n => r ^ n) atTop (𝓝 0)
[PROOFSTEP]
simpa only [← abs_pow] using (tendsto_pow_atTop_nhds_0_of_lt_1 (abs_nonneg r)) h
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ (k : ℕ), k < n → c * u k < u (k + 1)
⊢ c ^ n * u 0 < u n
[PROOFSTEP]
apply (monotone_mul_left_of_nonneg hc).seq_pos_lt_seq_of_le_of_lt hn _ _ h
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ (k : ℕ), k < n → c * u k < u (k + 1)
⊢ c ^ 0 * u 0 ≤ u 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ (k : ℕ), k < n → c * u k < u (k + 1)
⊢ ∀ (k : ℕ), k < n → c ^ (k + 1) * u 0 ≤ c * (c ^ k * u 0)
[PROOFSTEP]
simp [_root_.pow_succ, mul_assoc, le_refl]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ (k : ℕ), k < n → c * u k ≤ u (k + 1)
⊢ c ^ n * u 0 ≤ u n
[PROOFSTEP]
apply (monotone_mul_left_of_nonneg hc).seq_le_seq n _ _ h
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ (k : ℕ), k < n → c * u k ≤ u (k + 1)
⊢ c ^ 0 * u 0 ≤ u 0
[PROOFSTEP]
simp [_root_.pow_succ, mul_assoc, le_refl]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ (k : ℕ), k < n → c * u k ≤ u (k + 1)
⊢ ∀ (k : ℕ), k < n → c ^ (k + 1) * u 0 ≤ c * (c ^ k * u 0)
[PROOFSTEP]
simp [_root_.pow_succ, mul_assoc, le_refl]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ (k : ℕ), k < n → u (k + 1) < c * u k
⊢ u n < c ^ n * u 0
[PROOFSTEP]
apply (monotone_mul_left_of_nonneg hc).seq_pos_lt_seq_of_lt_of_le hn _ h _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ (k : ℕ), k < n → u (k + 1) < c * u k
⊢ u 0 ≤ c ^ 0 * u 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
hn : 0 < n
h : ∀ (k : ℕ), k < n → u (k + 1) < c * u k
⊢ ∀ (k : ℕ), k < n → c * (c ^ k * u 0) ≤ c ^ (k + 1) * u 0
[PROOFSTEP]
simp [_root_.pow_succ, mul_assoc, le_refl]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ (k : ℕ), k < n → u (k + 1) ≤ c * u k
⊢ u n ≤ c ^ n * u 0
[PROOFSTEP]
apply (monotone_mul_left_of_nonneg hc).seq_le_seq n _ h _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ (k : ℕ), k < n → u (k + 1) ≤ c * u k
⊢ u 0 ≤ c ^ 0 * u 0
[PROOFSTEP]
simp [_root_.pow_succ, mul_assoc, le_refl]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
u : ℕ → ℝ
c : ℝ
hc : 0 ≤ c
n : ℕ
h : ∀ (k : ℕ), k < n → u (k + 1) ≤ c * u k
⊢ ∀ (k : ℕ), k < n → c * (c ^ k * u 0) ≤ c ^ (k + 1) * u 0
[PROOFSTEP]
simp [_root_.pow_succ, mul_assoc, le_refl]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
r : ℝ≥0
hr : r < 1
⊢ Tendsto (fun a => ↑(r ^ a)) atTop (𝓝 ↑0)
[PROOFSTEP]
simp only [NNReal.coe_pow, NNReal.coe_zero, _root_.tendsto_pow_atTop_nhds_0_of_lt_1 r.coe_nonneg hr]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
r : ℝ≥0∞
hr : r < 1
⊢ Tendsto (fun n => r ^ n) atTop (𝓝 0)
[PROOFSTEP]
rcases ENNReal.lt_iff_exists_coe.1 hr with ⟨r, rfl, hr'⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
r : ℝ≥0
hr' : ↑r < 1
hr : ↑r < 1
⊢ Tendsto (fun n => ↑r ^ n) atTop (𝓝 0)
[PROOFSTEP]
rw [← ENNReal.coe_zero]
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
r : ℝ≥0
hr' : ↑r < 1
hr : ↑r < 1
⊢ Tendsto (fun n => ↑r ^ n) atTop (𝓝 ↑0)
[PROOFSTEP]
norm_cast at *
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
r : ℝ≥0
hr' hr : r < 1
⊢ Tendsto (fun a => r ^ a) atTop (𝓝 0)
[PROOFSTEP]
apply NNReal.tendsto_pow_atTop_nhds_0_of_lt_1 hr
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
r : ℝ
h₁ : 0 ≤ r
h₂ : r < 1
this✝ : r ≠ 1
this : Tendsto (fun n => (r ^ n - 1) * (r - 1)⁻¹) atTop (𝓝 ((0 - 1) * (r - 1)⁻¹))
⊢ Tendsto (fun n => ∑ i in Finset.range n, r ^ i) atTop (𝓝 (1 - r)⁻¹)
[PROOFSTEP]
simp_all [neg_inv, geom_sum_eq, div_eq_mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
⊢ HasSum (fun n => (1 / 2) ^ n) 2
[PROOFSTEP]
convert hasSum_geometric_of_lt_1 _ _
[GOAL]
case h.e'_6
α : Type u_1
β : Type u_2
ι : Type u_3
⊢ 2 = (1 - 1 / 2)⁻¹
[PROOFSTEP]
norm_num
[GOAL]
case convert_2
α : Type u_1
β : Type u_2
ι : Type u_3
⊢ 0 ≤ 1 / 2
[PROOFSTEP]
norm_num
[GOAL]
case convert_3
α : Type u_1
β : Type u_2
ι : Type u_3
⊢ 1 / 2 < 1
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
n : ℕ
⊢ ∑ i in Finset.range n, (1 / 2) ^ i ≤ 2
[PROOFSTEP]
have : ∀ i, 0 ≤ (1 / (2 : ℝ)) ^ i := by
  intro i
  apply pow_nonneg
  norm_num
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
n : ℕ
⊢ ∀ (i : ℕ), 0 ≤ (1 / 2) ^ i
[PROOFSTEP]
intro i
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
n i : ℕ
⊢ 0 ≤ (1 / 2) ^ i
[PROOFSTEP]
apply pow_nonneg
[GOAL]
case H
α : Type u_1
β : Type u_2
ι : Type u_3
n i : ℕ
⊢ 0 ≤ 1 / 2
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
n : ℕ
this : ∀ (i : ℕ), 0 ≤ (1 / 2) ^ i
⊢ ∑ i in Finset.range n, (1 / 2) ^ i ≤ 2
[PROOFSTEP]
convert sum_le_tsum (range n) (fun i _ => this i) summable_geometric_two
[GOAL]
case h.e'_4
α : Type u_1
β : Type u_2
ι : Type u_3
n : ℕ
this : ∀ (i : ℕ), 0 ≤ (1 / 2) ^ i
⊢ 2 = ∑' (i : ℕ), (1 / 2) ^ i
[PROOFSTEP]
exact tsum_geometric_two.symm
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
n : ℕ
⊢ (∑' (i : ℕ), if n ≤ i then 2⁻¹ ^ i else 0) = 2 * 2⁻¹ ^ n
[PROOFSTEP]
have A : Summable fun i : ℕ => ite (n ≤ i) ((2⁻¹ : ℝ) ^ i) 0 := by
  apply summable_of_nonneg_of_le _ _ summable_geometric_two <;>
    · intro i
      by_cases hi : n ≤ i <;> simp [hi]; apply pow_nonneg; exact zero_le_two
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
n : ℕ
⊢ Summable fun i => if n ≤ i then 2⁻¹ ^ i else 0
[PROOFSTEP]
apply summable_of_nonneg_of_le _ _ summable_geometric_two
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
n : ℕ
⊢ ∀ (b : ℕ), 0 ≤ if n ≤ b then 2⁻¹ ^ b else 0
[PROOFSTEP]
intro i
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
n i : ℕ
⊢ 0 ≤ if n ≤ i then 2⁻¹ ^ i else 0
[PROOFSTEP]
by_cases hi : n ≤ i
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
n i : ℕ
hi : n ≤ i
⊢ 0 ≤ if n ≤ i then 2⁻¹ ^ i else 0
[PROOFSTEP]
simp [hi]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
n i : ℕ
hi : ¬n ≤ i
⊢ 0 ≤ if n ≤ i then 2⁻¹ ^ i else 0
[PROOFSTEP]
simp [hi]
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
n i : ℕ
hi : n ≤ i
⊢ 0 ≤ 2 ^ i
[PROOFSTEP]
apply pow_nonneg
[GOAL]
case pos.H
α : Type u_1
β : Type u_2
ι : Type u_3
n i : ℕ
hi : n ≤ i
⊢ 0 ≤ 2
[PROOFSTEP]
exact zero_le_two
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
n : ℕ
⊢ ∀ (b : ℕ), (if n ≤ b then 2⁻¹ ^ b else 0) ≤ (1 / 2) ^ b
[PROOFSTEP]
intro i
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
n i : ℕ
⊢ (if n ≤ i then 2⁻¹ ^ i else 0) ≤ (1 / 2) ^ i
[PROOFSTEP]
by_cases hi : n ≤ i
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
n i : ℕ
hi : n ≤ i
⊢ (if n ≤ i then 2⁻¹ ^ i else 0) ≤ (1 / 2) ^ i
[PROOFSTEP]
simp [hi]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
n i : ℕ
hi : ¬n ≤ i
⊢ (if n ≤ i then 2⁻¹ ^ i else 0) ≤ (1 / 2) ^ i
[PROOFSTEP]
simp [hi]
[GOAL]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
n i : ℕ
hi : ¬n ≤ i
⊢ 0 ≤ 2 ^ i
[PROOFSTEP]
apply pow_nonneg
[GOAL]
case neg.H
α : Type u_1
β : Type u_2
ι : Type u_3
n i : ℕ
hi : ¬n ≤ i
⊢ 0 ≤ 2
[PROOFSTEP]
exact zero_le_two
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
n : ℕ
A : Summable fun i => if n ≤ i then 2⁻¹ ^ i else 0
⊢ (∑' (i : ℕ), if n ≤ i then 2⁻¹ ^ i else 0) = 2 * 2⁻¹ ^ n
[PROOFSTEP]
have B : ((Finset.range n).sum fun i : ℕ => ite (n ≤ i) ((2⁻¹ : ℝ) ^ i) 0) = 0 :=
  Finset.sum_eq_zero fun i hi => ite_eq_right_iff.2 fun h => (lt_irrefl _ ((Finset.mem_range.1 hi).trans_le h)).elim
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
n : ℕ
A : Summable fun i => if n ≤ i then 2⁻¹ ^ i else 0
B : (∑ i in Finset.range n, if n ≤ i then 2⁻¹ ^ i else 0) = 0
⊢ (∑' (i : ℕ), if n ≤ i then 2⁻¹ ^ i else 0) = 2 * 2⁻¹ ^ n
[PROOFSTEP]
simp only [← _root_.sum_add_tsum_nat_add n A, B, if_true, zero_add, zero_le', le_add_iff_nonneg_left, pow_add,
  _root_.tsum_mul_right, tsum_geometric_inv_two]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
a : ℝ
⊢ HasSum (fun n => a / 2 / 2 ^ n) a
[PROOFSTEP]
convert HasSum.mul_left (a / 2) (hasSum_geometric_of_lt_1 (le_of_lt one_half_pos) one_half_lt_one) using 1
[GOAL]
case h.e'_5
α : Type u_1
β : Type u_2
ι : Type u_3
a : ℝ
⊢ (fun n => a / 2 / 2 ^ n) = fun i => a / 2 * (1 / 2) ^ i
[PROOFSTEP]
funext n
[GOAL]
case h.e'_5.h
α : Type u_1
β : Type u_2
ι : Type u_3
a : ℝ
n : ℕ
⊢ a / 2 / 2 ^ n = a / 2 * (1 / 2) ^ n
[PROOFSTEP]
simp
[GOAL]
case h.e'_5.h
α : Type u_1
β : Type u_2
ι : Type u_3
a : ℝ
n : ℕ
⊢ a / 2 / 2 ^ n = a / 2 * (2 ^ n)⁻¹
[PROOFSTEP]
rfl
[GOAL]
case h.e'_6
α : Type u_1
β : Type u_2
ι : Type u_3
a : ℝ
⊢ a = a / 2 * (1 - 1 / 2)⁻¹
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
r : ℝ≥0
hr : r < 1
⊢ HasSum (fun n => r ^ n) (1 - r)⁻¹
[PROOFSTEP]
apply NNReal.hasSum_coe.1
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
r : ℝ≥0
hr : r < 1
⊢ HasSum (fun a => ↑(r ^ a)) ↑(1 - r)⁻¹
[PROOFSTEP]
push_cast
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
r : ℝ≥0
hr : r < 1
⊢ HasSum (fun a => ↑r ^ a) (↑(1 - r))⁻¹
[PROOFSTEP]
rw [NNReal.coe_sub (le_of_lt hr)]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
r : ℝ≥0
hr : r < 1
⊢ HasSum (fun a => ↑r ^ a) (↑1 - ↑r)⁻¹
[PROOFSTEP]
exact hasSum_geometric_of_lt_1 r.coe_nonneg hr
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
r : ℝ≥0∞
⊢ ∑' (n : ℕ), r ^ n = (1 - r)⁻¹
[PROOFSTEP]
cases' lt_or_le r 1 with hr hr
[GOAL]
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
r : ℝ≥0∞
hr : r < 1
⊢ ∑' (n : ℕ), r ^ n = (1 - r)⁻¹
[PROOFSTEP]
rcases ENNReal.lt_iff_exists_coe.1 hr with ⟨r, rfl, hr'⟩
[GOAL]
case inl.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
r : ℝ≥0
hr' : ↑r < 1
hr : ↑r < 1
⊢ ∑' (n : ℕ), ↑r ^ n = (1 - ↑r)⁻¹
[PROOFSTEP]
norm_cast at *
[GOAL]
case inl.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
r : ℝ≥0
hr' hr : r < 1
⊢ ∑' (n : ℕ), ↑(r ^ n) = (1 - ↑r)⁻¹
[PROOFSTEP]
convert ENNReal.tsum_coe_eq (NNReal.hasSum_geometric hr)
[GOAL]
case h.e'_3
α : Type u_1
β : Type u_2
ι : Type u_3
r : ℝ≥0
hr' hr : r < 1
⊢ (1 - ↑r)⁻¹ = ↑(1 - r)⁻¹
[PROOFSTEP]
rw [ENNReal.coe_inv <| ne_of_gt <| tsub_pos_iff_lt.2 hr, coe_sub, coe_one]
[GOAL]
case inr
α : Type u_1
β : Type u_2
ι : Type u_3
r : ℝ≥0∞
hr : 1 ≤ r
⊢ ∑' (n : ℕ), r ^ n = (1 - r)⁻¹
[PROOFSTEP]
rw [tsub_eq_zero_iff_le.mpr hr, ENNReal.inv_zero, ENNReal.tsum_eq_iSup_nat, iSup_eq_top]
[GOAL]
case inr
α : Type u_1
β : Type u_2
ι : Type u_3
r : ℝ≥0∞
hr : 1 ≤ r
⊢ ∀ (b : ℝ≥0∞), b < ⊤ → ∃ i, b < ∑ a in Finset.range i, r ^ a
[PROOFSTEP]
refine' fun a ha => (ENNReal.exists_nat_gt (lt_top_iff_ne_top.1 ha)).imp fun n hn => lt_of_lt_of_le hn _
[GOAL]
case inr
α : Type u_1
β : Type u_2
ι : Type u_3
r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ⊤
n : ℕ
hn : a < ↑n
⊢ ↑n ≤ ∑ a in Finset.range n, r ^ a
[PROOFSTEP]
calc
  (n : ℝ≥0∞) = ∑ i in range n, 1 := by rw [sum_const, nsmul_one, card_range]
  _ ≤ ∑ i in range n, r ^ i := by gcongr; apply one_le_pow_of_one_le' hr
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ⊤
n : ℕ
hn : a < ↑n
⊢ ↑n = ∑ i in Finset.range n, 1
[PROOFSTEP]
rw [sum_const, nsmul_one, card_range]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ⊤
n : ℕ
hn : a < ↑n
⊢ ∑ i in Finset.range n, 1 ≤ ∑ i in Finset.range n, r ^ i
[PROOFSTEP]
gcongr
[GOAL]
case h
α : Type u_1
β : Type u_2
ι : Type u_3
r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ⊤
n : ℕ
hn : a < ↑n
i✝ : ℕ
a✝ : i✝ ∈ Finset.range n
⊢ 1 ≤ r ^ i✝
[PROOFSTEP]
apply one_le_pow_of_one_le' hr
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
hr : r < 1
hC : C ≠ ⊤
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
⊢ CauchySeq f
[PROOFSTEP]
refine' cauchySeq_of_edist_le_of_tsum_ne_top _ hu _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
hr : r < 1
hC : C ≠ ⊤
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
⊢ ∑' (n : ℕ), C * r ^ n ≠ ⊤
[PROOFSTEP]
rw [ENNReal.tsum_mul_left, ENNReal.tsum_geometric]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
hr : r < 1
hC : C ≠ ⊤
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
⊢ C * (1 - r)⁻¹ ≠ ⊤
[PROOFSTEP]
refine' ENNReal.mul_ne_top hC (ENNReal.inv_ne_top.2 _)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
hr : r < 1
hC : C ≠ ⊤
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
⊢ 1 - r ≠ 0
[PROOFSTEP]
exact (tsub_pos_iff_lt.2 hr).ne'
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
hr : r < 1
hC : C ≠ ⊤
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ edist (f n) a ≤ C * r ^ n / (1 - r)
[PROOFSTEP]
convert edist_le_tsum_of_edist_le_of_tendsto _ hu ha _
[GOAL]
case h.e'_4
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
hr : r < 1
hC : C ≠ ⊤
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ C * r ^ n / (1 - r) = ∑' (m : ℕ), C * r ^ (n + m)
[PROOFSTEP]
simp only [pow_add, ENNReal.tsum_mul_left, ENNReal.tsum_geometric, div_eq_mul_inv, mul_assoc]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
hr : r < 1
hC : C ≠ ⊤
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
⊢ edist (f 0) a ≤ C / (1 - r)
[PROOFSTEP]
simpa only [_root_.pow_zero, mul_one] using edist_le_of_edist_le_geometric_of_tendsto r C hu ha 0
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
hC : C ≠ ⊤
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C / 2 ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
⊢ CauchySeq f
[PROOFSTEP]
simp only [div_eq_mul_inv, ENNReal.inv_pow] at hu
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
hC : C ≠ ⊤
f : ℕ → α
a : α
ha : Tendsto f atTop (𝓝 a)
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n
⊢ CauchySeq f
[PROOFSTEP]
refine' cauchySeq_of_edist_le_geometric 2⁻¹ C _ hC hu
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
hC : C ≠ ⊤
f : ℕ → α
a : α
ha : Tendsto f atTop (𝓝 a)
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n
⊢ 2⁻¹ < 1
[PROOFSTEP]
simp [ENNReal.one_lt_two]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
hC : C ≠ ⊤
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C / 2 ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ edist (f n) a ≤ 2 * C / 2 ^ n
[PROOFSTEP]
simp only [div_eq_mul_inv, ENNReal.inv_pow] at *
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
hC : C ≠ ⊤
f : ℕ → α
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n
⊢ edist (f n) a ≤ 2 * C * 2⁻¹ ^ n
[PROOFSTEP]
rw [mul_assoc, mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
hC : C ≠ ⊤
f : ℕ → α
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n
⊢ edist (f n) a ≤ C * 2⁻¹ ^ n * 2
[PROOFSTEP]
convert edist_le_of_edist_le_geometric_of_tendsto 2⁻¹ C hu ha n using 1
[GOAL]
case h.e'_4
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
hC : C ≠ ⊤
f : ℕ → α
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * 2⁻¹ ^ n
⊢ C * 2⁻¹ ^ n * 2 = C * 2⁻¹ ^ n / (1 - 2⁻¹)
[PROOFSTEP]
rw [ENNReal.one_sub_inv_two, div_eq_mul_inv, inv_inv]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : PseudoEMetricSpace α
C : ℝ≥0∞
hC : C ≠ ⊤
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C / 2 ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
⊢ edist (f 0) a ≤ 2 * C
[PROOFSTEP]
simpa only [_root_.pow_zero, div_eq_mul_inv, inv_one, mul_one] using
  edist_le_of_edist_le_geometric_two_of_tendsto C hu ha 0
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : PseudoMetricSpace α
r C : ℝ
hr : r < 1
f : ℕ → α
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
⊢ HasSum (fun n => C * r ^ n) (C / (1 - r))
[PROOFSTEP]
rcases sign_cases_of_C_mul_pow_nonneg fun n => dist_nonneg.trans (hu n) with (rfl | ⟨_, r₀⟩)
[GOAL]
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : PseudoMetricSpace α
r : ℝ
hr : r < 1
f : ℕ → α
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ 0 * r ^ n
⊢ HasSum (fun n => 0 * r ^ n) (0 / (1 - r))
[PROOFSTEP]
simp [hasSum_zero]
[GOAL]
case inr.intro
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : PseudoMetricSpace α
r C : ℝ
hr : r < 1
f : ℕ → α
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
left✝ : 0 < C
r₀ : 0 ≤ r
⊢ HasSum (fun n => C * r ^ n) (C / (1 - r))
[PROOFSTEP]
refine' HasSum.mul_left C _
[GOAL]
case inr.intro
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : PseudoMetricSpace α
r C : ℝ
hr : r < 1
f : ℕ → α
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
left✝ : 0 < C
r₀ : 0 ≤ r
⊢ HasSum (fun n => r ^ n) (1 - r)⁻¹
[PROOFSTEP]
simpa using hasSum_geometric_of_lt_1 r₀ hr
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : PseudoMetricSpace α
r C : ℝ
hr : r < 1
f : ℕ → α
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ dist (f n) a ≤ C * r ^ n / (1 - r)
[PROOFSTEP]
have := aux_hasSum_of_le_geometric hr hu
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : PseudoMetricSpace α
r C : ℝ
hr : r < 1
f : ℕ → α
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
this : HasSum (fun n => C * r ^ n) (C / (1 - r))
⊢ dist (f n) a ≤ C * r ^ n / (1 - r)
[PROOFSTEP]
convert dist_le_tsum_of_dist_le_of_tendsto _ hu ⟨_, this⟩ ha n
[GOAL]
case h.e'_4
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : PseudoMetricSpace α
r C : ℝ
hr : r < 1
f : ℕ → α
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
this : HasSum (fun n => C * r ^ n) (C / (1 - r))
⊢ C * r ^ n / (1 - r) = ∑' (m : ℕ), C * r ^ (n + m)
[PROOFSTEP]
simp only [pow_add, mul_left_comm C, mul_div_right_comm]
[GOAL]
case h.e'_4
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : PseudoMetricSpace α
r C : ℝ
hr : r < 1
f : ℕ → α
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
this : HasSum (fun n => C * r ^ n) (C / (1 - r))
⊢ C / (1 - r) * r ^ n = ∑' (m : ℕ), r ^ n * (C * r ^ m)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
case h.e'_4
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : PseudoMetricSpace α
r C : ℝ
hr : r < 1
f : ℕ → α
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
this : HasSum (fun n => C * r ^ n) (C / (1 - r))
⊢ r ^ n * (C / (1 - r)) = ∑' (m : ℕ), r ^ n * (C * r ^ m)
[PROOFSTEP]
exact (this.mul_left _).tsum_eq.symm
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : PseudoMetricSpace α
r C : ℝ
hr : r < 1
f : ℕ → α
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
hu₂ : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ dist (f n) a ≤ C / 2 ^ n
[PROOFSTEP]
convert dist_le_tsum_of_dist_le_of_tendsto _ hu₂ (summable_geometric_two' C) ha n
[GOAL]
case h.e'_4
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : PseudoMetricSpace α
r C : ℝ
hr : r < 1
f : ℕ → α
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
hu₂ : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ C / 2 ^ n = ∑' (m : ℕ), C / 2 / 2 ^ (n + m)
[PROOFSTEP]
simp only [add_comm n, pow_add, ← div_div]
[GOAL]
case h.e'_4
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : PseudoMetricSpace α
r C : ℝ
hr : r < 1
f : ℕ → α
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
hu₂ : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ C / 2 ^ n = ∑' (m : ℕ), C / 2 / 2 ^ m / 2 ^ n
[PROOFSTEP]
symm
[GOAL]
case h.e'_4
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : PseudoMetricSpace α
r C : ℝ
hr : r < 1
f : ℕ → α
hu : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n
hu₂ : ∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ ∑' (m : ℕ), C / 2 / 2 ^ m / 2 ^ n = C / 2 ^ n
[PROOFSTEP]
exact ((hasSum_geometric_two' C).div_const _).tsum_eq
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
⊢ Summable fun i => 1 / m ^ f i
[PROOFSTEP]
refine'
  summable_of_nonneg_of_le (fun a => one_div_nonneg.mpr (pow_nonneg (zero_le_one.trans hm.le) _)) (fun a => _)
    (summable_geometric_of_lt_1 (one_div_nonneg.mpr (zero_le_one.trans hm.le))
      ((one_div_lt (zero_lt_one.trans hm) zero_lt_one).mpr (one_div_one.le.trans_lt hm)))
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 1 / m ^ f a ≤ (1 / m) ^ a
[PROOFSTEP]
rw [div_pow, one_pow]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 1 / m ^ f a ≤ 1 / m ^ a
[PROOFSTEP]
refine' (one_div_le_one_div _ _).mpr (pow_le_pow hm.le (fi a))
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 0 < m ^ f a
[PROOFSTEP]
exact pow_pos (zero_lt_one.trans hm) _
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
a : ℕ
⊢ 0 < m ^ a
[PROOFSTEP]
exact pow_pos (zero_lt_one.trans hm) _
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type ?u.561991
inst✝ : Encodable ι
⊢ { ε' // (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c ≤ ε }
[PROOFSTEP]
let f n := ε / 2 / 2 ^ n
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type ?u.561991
inst✝ : Encodable ι
f : ℕ → ℝ := fun n => ε / 2 / 2 ^ n
⊢ { ε' // (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c ≤ ε }
[PROOFSTEP]
have hf : HasSum f ε := hasSum_geometric_two' _
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type ?u.561991
inst✝ : Encodable ι
f : ℕ → ℝ := fun n => ε / 2 / 2 ^ n
hf : HasSum f ε
⊢ { ε' // (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c ≤ ε }
[PROOFSTEP]
have f0 : ∀ n, 0 < f n := fun n => div_pos (half_pos hε) (pow_pos zero_lt_two _)
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type ?u.561991
inst✝ : Encodable ι
f : ℕ → ℝ := fun n => ε / 2 / 2 ^ n
hf : HasSum f ε
f0 : ∀ (n : ℕ), 0 < f n
⊢ { ε' // (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c ≤ ε }
[PROOFSTEP]
refine' ⟨f ∘ Encodable.encode, fun i => f0 _, _⟩
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type ?u.561991
inst✝ : Encodable ι
f : ℕ → ℝ := fun n => ε / 2 / 2 ^ n
hf : HasSum f ε
f0 : ∀ (n : ℕ), 0 < f n
⊢ ∃ c, HasSum (f ∘ Encodable.encode) c ∧ c ≤ ε
[PROOFSTEP]
rcases hf.summable.comp_injective (@Encodable.encode_injective ι _) with ⟨c, hg⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type ?u.561991
inst✝ : Encodable ι
f : ℕ → ℝ := fun n => ε / 2 / 2 ^ n
hf : HasSum f ε
f0 : ∀ (n : ℕ), 0 < f n
c : ℝ
hg : HasSum (f ∘ Encodable.encode) c
⊢ ∃ c, HasSum (f ∘ Encodable.encode) c ∧ c ≤ ε
[PROOFSTEP]
refine' ⟨c, hg, hasSum_le_inj _ (@Encodable.encode_injective ι _) _ _ hg hf⟩
[GOAL]
case intro.refine'_1
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type ?u.561991
inst✝ : Encodable ι
f : ℕ → ℝ := fun n => ε / 2 / 2 ^ n
hf : HasSum f ε
f0 : ∀ (n : ℕ), 0 < f n
c : ℝ
hg : HasSum (f ∘ Encodable.encode) c
⊢ ∀ (c : ℕ), ¬c ∈ Set.range Encodable.encode → 0 ≤ f c
[PROOFSTEP]
intro i _
[GOAL]
case intro.refine'_1
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type ?u.561991
inst✝ : Encodable ι
f : ℕ → ℝ := fun n => ε / 2 / 2 ^ n
hf : HasSum f ε
f0 : ∀ (n : ℕ), 0 < f n
c : ℝ
hg : HasSum (f ∘ Encodable.encode) c
i : ℕ
a✝ : ¬i ∈ Set.range Encodable.encode
⊢ 0 ≤ f i
[PROOFSTEP]
exact le_of_lt (f0 _)
[GOAL]
case intro.refine'_2
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type ?u.561991
inst✝ : Encodable ι
f : ℕ → ℝ := fun n => ε / 2 / 2 ^ n
hf : HasSum f ε
f0 : ∀ (n : ℕ), 0 < f n
c : ℝ
hg : HasSum (f ∘ Encodable.encode) c
⊢ ∀ (i : ι), (f ∘ Encodable.encode) i ≤ f (Encodable.encode i)
[PROOFSTEP]
intro n
[GOAL]
case intro.refine'_2
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ
hε : 0 < ε
ι : Type ?u.561991
inst✝ : Encodable ι
f : ℕ → ℝ := fun n => ε / 2 / 2 ^ n
hf : HasSum f ε
f0 : ∀ (n : ℕ), 0 < f n
c : ℝ
hg : HasSum (f ∘ Encodable.encode) c
n : ι
⊢ (f ∘ Encodable.encode) n ≤ f (Encodable.encode n)
[PROOFSTEP]
exact le_rfl
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ι : Type u_4
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum (fun i => ε' ↑i) c ∧ c ≤ ε
[PROOFSTEP]
haveI := hs.toEncodable
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ι : Type u_4
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum (fun i => ε' ↑i) c ∧ c ≤ ε
[PROOFSTEP]
rcases posSumOfEncodable hε s with ⟨f, hf0, ⟨c, hfc, hcε⟩⟩
[GOAL]
case mk.intro.intro.intro
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ι : Type u_4
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum (fun i => ε' ↑i) c ∧ c ≤ ε
[PROOFSTEP]
refine' ⟨fun i => if h : i ∈ s then f ⟨i, h⟩ else 1, fun i => _, ⟨c, _, hcε⟩⟩
[GOAL]
case mk.intro.intro.intro.refine'_1
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ι : Type u_4
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
i : ι
⊢ 0 < (fun i => if h : i ∈ s then f { val := i, property := h } else 1) i
[PROOFSTEP]
conv_rhs => simp
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ι : Type u_4
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
i : ι
| (fun i => if h : i ∈ s then f { val := i, property := h } else 1) i
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ι : Type u_4
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
i : ι
| (fun i => if h : i ∈ s then f { val := i, property := h } else 1) i
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ι : Type u_4
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
i : ι
| (fun i => if h : i ∈ s then f { val := i, property := h } else 1) i
[PROOFSTEP]
simp
[GOAL]
case mk.intro.intro.intro.refine'_1
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ι : Type u_4
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
i : ι
⊢ 0 < if h : i ∈ s then f { val := i, property := h } else 1
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ι : Type u_4
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
i : ι
h✝ : i ∈ s
⊢ 0 < f { val := i, property := h✝ }
case neg
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ι : Type u_4
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
i : ι
h✝ : ¬i ∈ s
⊢ 0 < 1
[PROOFSTEP]
exacts [hf0 _, zero_lt_one]
[GOAL]
case mk.intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ι : Type u_4
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
this : Encodable ↑s
f : ↑s → ℝ
hf0 : ∀ (i : ↑s), 0 < f i
c : ℝ
hfc : HasSum f c
hcε : c ≤ ε
⊢ HasSum (fun i => (fun i => if h : i ∈ s then f { val := i, property := h } else 1) ↑i) c
[PROOFSTEP]
simpa only [Subtype.coe_prop, dif_pos, Subtype.coe_eta]
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ι : Type u_4
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∀ (t : Finset ι), ↑t ⊆ s → ∑ i in t, ε' i ≤ ε
[PROOFSTEP]
rcases hs.exists_pos_hasSum_le hε with ⟨ε', hpos, c, hε'c, hcε⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ι : Type u_4
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
ε' : ι → ℝ
hpos : ∀ (i : ι), 0 < ε' i
c : ℝ
hε'c : HasSum (fun i => ε' ↑i) c
hcε : c ≤ ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∀ (t : Finset ι), ↑t ⊆ s → ∑ i in t, ε' i ≤ ε
[PROOFSTEP]
refine' ⟨ε', hpos, fun t ht => _⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ι : Type u_4
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
ε' : ι → ℝ
hpos : ∀ (i : ι), 0 < ε' i
c : ℝ
hε'c : HasSum (fun i => ε' ↑i) c
hcε : c ≤ ε
t : Finset ι
ht : ↑t ⊆ s
⊢ ∑ i in t, ε' i ≤ ε
[PROOFSTEP]
rw [← sum_subtype_of_mem _ ht]
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ι : Type u_4
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
ε' : ι → ℝ
hpos : ∀ (i : ι), 0 < ε' i
c : ℝ
hε'c : HasSum (fun i => ε' ↑i) c
hcε : c ≤ ε
t : Finset ι
ht : ↑t ⊆ s
⊢ ∑ x in Finset.subtype (fun x => x ∈ s) t, ε' ↑x ≤ ε
[PROOFSTEP]
refine' (sum_le_hasSum _ _ hε'c).trans hcε
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ι : Type u_4
s : Set ι
hs : Set.Countable s
ε : ℝ
hε : 0 < ε
ε' : ι → ℝ
hpos : ∀ (i : ι), 0 < ε' i
c : ℝ
hε'c : HasSum (fun i => ε' ↑i) c
hcε : c ≤ ε
t : Finset ι
ht : ↑t ⊆ s
⊢ ∀ (i : ↑s), ¬i ∈ Finset.subtype (fun x => x ∈ s) t → 0 ≤ ε' ↑i
[PROOFSTEP]
exact fun _ _ => (hpos _).le
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε
[PROOFSTEP]
cases nonempty_encodable ι
[GOAL]
case intro
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
val✝ : Encodable ι
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε
[PROOFSTEP]
obtain ⟨a, a0, aε⟩ := exists_between (pos_iff_ne_zero.2 hε)
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
val✝ : Encodable ι
a : ℝ≥0
a0 : 0 < a
aε : a < ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε
[PROOFSTEP]
obtain ⟨ε', hε', c, hc, hcε⟩ := posSumOfEncodable a0 ι
[GOAL]
case intro.intro.intro.mk.intro.intro.intro
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
val✝ : Encodable ι
a : ℝ≥0
a0 : 0 < a
aε : a < ε
ε' : ι → ℝ
hε' : ∀ (i : ι), 0 < ε' i
c : ℝ
hc : HasSum ε' c
hcε : c ≤ (fun a => ↑a) a
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c < ε
[PROOFSTEP]
exact
  ⟨fun i => ⟨ε' i, (hε' i).le⟩, fun i => NNReal.coe_lt_coe.1 <| hε' i,
    ⟨c, hasSum_le (fun i => (hε' i).le) hasSum_zero hc⟩, NNReal.hasSum_coe.1 hc,
    aε.trans_le' <| NNReal.coe_le_coe.1 hcε⟩
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), ↑(ε' i) < ε
[PROOFSTEP]
rcases exists_between (pos_iff_ne_zero.2 hε) with ⟨r, h0r, hrε⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
r : ℝ≥0∞
h0r : 0 < r
hrε : r < ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), ↑(ε' i) < ε
[PROOFSTEP]
rcases lt_iff_exists_coe.1 hrε with ⟨x, rfl, _⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
x : ℝ≥0
right✝ : ↑x < ε
h0r : 0 < ↑x
hrε : ↑x < ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), ↑(ε' i) < ε
[PROOFSTEP]
rcases NNReal.exists_pos_sum_of_countable (coe_pos.1 h0r).ne' ι with ⟨ε', hp, c, hc, hcr⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
x : ℝ≥0
right✝ : ↑x < ε
h0r : 0 < ↑x
hrε : ↑x < ε
ε' : ι → ℝ≥0
hp : ∀ (i : ι), 0 < ε' i
c : ℝ≥0
hc : HasSum ε' c
hcr : c < x
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), ↑(ε' i) < ε
[PROOFSTEP]
exact ⟨ε', hp, (ENNReal.tsum_coe_eq hc).symm ▸ lt_trans (coe_lt_coe.2 hcr) hrε⟩
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w : ι → ℝ≥0∞
hw : ∀ (i : ι), w i ≠ ⊤
⊢ ∃ δ, (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), w i * ↑(δ i) < ε
[PROOFSTEP]
lift w to ι → ℝ≥0 using hw
[GOAL]
case intro
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w : ι → ℝ≥0
⊢ ∃ δ, (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), (fun i => ↑(w i)) i * ↑(δ i) < ε
[PROOFSTEP]
rcases exists_pos_sum_of_countable hε ι with ⟨δ', Hpos, Hsum⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), ↑(δ' i) < ε
⊢ ∃ δ, (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), (fun i => ↑(w i)) i * ↑(δ i) < ε
[PROOFSTEP]
have : ∀ i, 0 < max 1 (w i) := fun i => zero_lt_one.trans_le (le_max_left _ _)
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), ↑(δ' i) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
⊢ ∃ δ, (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), (fun i => ↑(w i)) i * ↑(δ i) < ε
[PROOFSTEP]
refine' ⟨fun i => δ' i / max 1 (w i), fun i => div_pos (Hpos _) (this i), _⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), ↑(δ' i) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
⊢ ∑' (i : ι), (fun i => ↑(w i)) i * ↑((fun i => δ' i / max 1 (w i)) i) < ε
[PROOFSTEP]
refine' lt_of_le_of_lt (ENNReal.tsum_le_tsum fun i => _) Hsum
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), ↑(δ' i) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
i : ι
⊢ (fun i => ↑(w i)) i * ↑((fun i => δ' i / max 1 (w i)) i) ≤ ↑(δ' i)
[PROOFSTEP]
rw [coe_div (this i).ne']
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), ↑(δ' i) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
i : ι
⊢ (fun i => ↑(w i)) i * (↑(δ' i) / ↑(max 1 (w i))) ≤ ↑(δ' i)
[PROOFSTEP]
refine' mul_le_of_le_div' (mul_le_mul_left' (ENNReal.inv_le_inv.2 _) _)
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
ι✝ : Type u_3
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), ↑(δ' i) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
i : ι
⊢ (fun i => ↑(w i)) i ≤ ↑(max 1 (w i))
[PROOFSTEP]
exact coe_le_coe.2 (le_max_right _ _)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
n : ℕ
⊢ 0 ≤ ↑n !
[PROOFSTEP]
exact_mod_cast n.factorial_pos.le
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
n : ℕ
⊢ 0 ≤ ↑n
[PROOFSTEP]
exact_mod_cast n.zero_le
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
⊢ ∀ᶠ (b : ℕ) in atTop, ↑b ! / ↑b ^ b ≤ 1 / ↑b
[PROOFSTEP]
refine' (eventually_gt_atTop 0).mono fun n hn => _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
n : ℕ
hn : 0 < n
⊢ ↑n ! / ↑n ^ n ≤ 1 / ↑n
[PROOFSTEP]
rcases Nat.exists_eq_succ_of_ne_zero hn.ne.symm with ⟨k, rfl⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
k : ℕ
hn : 0 < succ k
⊢ ↑(succ k)! / ↑(succ k) ^ succ k ≤ 1 / ↑(succ k)
[PROOFSTEP]
rw [← prod_range_add_one_eq_factorial, pow_eq_prod_const, div_eq_mul_inv, ← inv_eq_one_div, prod_natCast, Nat.cast_succ,
  ← prod_inv_distrib, ← prod_mul_distrib, Finset.prod_range_succ']
[GOAL]
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
k : ℕ
hn : 0 < succ k
⊢ (∏ k_1 in Finset.range k, ↑(k_1 + 1 + 1) * (↑k + 1)⁻¹) * (↑(0 + 1) * (↑k + 1)⁻¹) ≤ (↑k + 1)⁻¹
[PROOFSTEP]
simp only [prod_range_succ', one_mul, Nat.cast_add, zero_add, Nat.cast_one]
[GOAL]
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
k : ℕ
hn : 0 < succ k
⊢ (∏ x in Finset.range k, (↑x + 1 + 1) * (↑k + 1)⁻¹) * (↑k + 1)⁻¹ ≤ (↑k + 1)⁻¹
[PROOFSTEP]
refine' mul_le_of_le_one_left (inv_nonneg.mpr <| by exact_mod_cast hn.le) (prod_le_one _ _)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
k : ℕ
hn : 0 < succ k
⊢ 0 ≤ ↑k + 1
[PROOFSTEP]
exact_mod_cast hn.le
[GOAL]
case intro.refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
k : ℕ
hn : 0 < succ k
⊢ ∀ (i : ℕ), i ∈ Finset.range k → 0 ≤ (↑i + 1 + 1) * (↑k + 1)⁻¹
[PROOFSTEP]
intro x hx
[GOAL]
case intro.refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
k : ℕ
hn : 0 < succ k
⊢ ∀ (i : ℕ), i ∈ Finset.range k → (↑i + 1 + 1) * (↑k + 1)⁻¹ ≤ 1
[PROOFSTEP]
intro x hx
[GOAL]
case intro.refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
k : ℕ
hn : 0 < succ k
x : ℕ
hx : x ∈ Finset.range k
⊢ 0 ≤ (↑x + 1 + 1) * (↑k + 1)⁻¹
[PROOFSTEP]
rw [Finset.mem_range] at hx
[GOAL]
case intro.refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
k : ℕ
hn : 0 < succ k
x : ℕ
hx : x ∈ Finset.range k
⊢ (↑x + 1 + 1) * (↑k + 1)⁻¹ ≤ 1
[PROOFSTEP]
rw [Finset.mem_range] at hx
[GOAL]
case intro.refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
k : ℕ
hn : 0 < succ k
x : ℕ
hx : x < k
⊢ 0 ≤ (↑x + 1 + 1) * (↑k + 1)⁻¹
[PROOFSTEP]
refine' mul_nonneg _ (inv_nonneg.mpr _)
[GOAL]
case intro.refine'_1.refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
k : ℕ
hn : 0 < succ k
x : ℕ
hx : x < k
⊢ 0 ≤ ↑x + 1 + 1
[PROOFSTEP]
norm_cast
[GOAL]
case intro.refine'_1.refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
k : ℕ
hn : 0 < succ k
x : ℕ
hx : x < k
⊢ 0 ≤ ↑k + 1
[PROOFSTEP]
norm_cast
[GOAL]
case intro.refine'_1.refine'_1
α : Type u_1
β : Type u_2
ι : Type u_3
k : ℕ
hn : 0 < succ k
x : ℕ
hx : x < k
⊢ 0 ≤ x + 1 + 1
[PROOFSTEP]
linarith
[GOAL]
case intro.refine'_1.refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
k : ℕ
hn : 0 < succ k
x : ℕ
hx : x < k
⊢ 0 ≤ k + 1
[PROOFSTEP]
linarith
[GOAL]
case intro.refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
k : ℕ
hn : 0 < succ k
x : ℕ
hx : x < k
⊢ (↑x + 1 + 1) * (↑k + 1)⁻¹ ≤ 1
[PROOFSTEP]
refine' (div_le_one <| by exact_mod_cast hn).mpr _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
k : ℕ
hn : 0 < succ k
x : ℕ
hx : x < k
⊢ 0 < ↑k + 1
[PROOFSTEP]
exact_mod_cast hn
[GOAL]
case intro.refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
k : ℕ
hn : 0 < succ k
x : ℕ
hx : x < k
⊢ ↑x + 1 + 1 ≤ ↑k + 1
[PROOFSTEP]
norm_cast
[GOAL]
case intro.refine'_2
α : Type u_1
β : Type u_2
ι : Type u_3
k : ℕ
hn : 0 < succ k
x : ℕ
hx : x < k
⊢ x + 1 + 1 ≤ k + 1
[PROOFSTEP]
linarith
[GOAL]
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : Type u_4
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
x : ℕ
⊢ x ≤ ⌊max 0 (↑x + 1)⌋₊
[PROOFSTEP]
simp [Nat.le_floor_iff]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
⊢ Tendsto (fun x => ↑⌊a * x⌋₊ / x) atTop (𝓝 a)
[PROOFSTEP]
have A : Tendsto (fun x : R => a - x⁻¹) atTop (𝓝 (a - 0)) := tendsto_const_nhds.sub tendsto_inv_atTop_zero
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a - x⁻¹) atTop (𝓝 (a - 0))
⊢ Tendsto (fun x => ↑⌊a * x⌋₊ / x) atTop (𝓝 a)
[PROOFSTEP]
rw [sub_zero] at A
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a - x⁻¹) atTop (𝓝 a)
⊢ Tendsto (fun x => ↑⌊a * x⌋₊ / x) atTop (𝓝 a)
[PROOFSTEP]
apply tendsto_of_tendsto_of_tendsto_of_le_of_le' A tendsto_const_nhds
[GOAL]
case hgf
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a - x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, a - b⁻¹ ≤ ↑⌊a * b⌋₊ / b
[PROOFSTEP]
refine' eventually_atTop.2 ⟨1, fun x hx => _⟩
[GOAL]
case hgf
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a - x⁻¹) atTop (𝓝 a)
x : R
hx : x ≥ 1
⊢ a - x⁻¹ ≤ ↑⌊a * x⌋₊ / x
[PROOFSTEP]
simp only [le_div_iff (zero_lt_one.trans_le hx), _root_.sub_mul, inv_mul_cancel (zero_lt_one.trans_le hx).ne']
[GOAL]
case hgf
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a - x⁻¹) atTop (𝓝 a)
x : R
hx : x ≥ 1
⊢ a * x - 1 ≤ ↑⌊a * x⌋₊
[PROOFSTEP]
have := Nat.lt_floor_add_one (a * x)
[GOAL]
case hgf
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a - x⁻¹) atTop (𝓝 a)
x : R
hx : x ≥ 1
this : a * x < ↑⌊a * x⌋₊ + 1
⊢ a * x - 1 ≤ ↑⌊a * x⌋₊
[PROOFSTEP]
linarith
[GOAL]
case hfh
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a - x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, ↑⌊a * b⌋₊ / b ≤ a
[PROOFSTEP]
refine' eventually_atTop.2 ⟨1, fun x hx => _⟩
[GOAL]
case hfh
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a - x⁻¹) atTop (𝓝 a)
x : R
hx : x ≥ 1
⊢ ↑⌊a * x⌋₊ / x ≤ a
[PROOFSTEP]
rw [div_le_iff (zero_lt_one.trans_le hx)]
[GOAL]
case hfh
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a - x⁻¹) atTop (𝓝 a)
x : R
hx : x ≥ 1
⊢ ↑⌊a * x⌋₊ ≤ a * x
[PROOFSTEP]
simp [Nat.floor_le (mul_nonneg ha (zero_le_one.trans hx))]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
⊢ Tendsto (fun x => ↑⌊x⌋₊ / x) atTop (𝓝 1)
[PROOFSTEP]
simpa using tendsto_nat_floor_mul_div_atTop (zero_le_one' R)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
⊢ Tendsto (fun x => ↑⌈a * x⌉₊ / x) atTop (𝓝 a)
[PROOFSTEP]
have A : Tendsto (fun x : R => a + x⁻¹) atTop (𝓝 (a + 0)) := tendsto_const_nhds.add tendsto_inv_atTop_zero
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a + x⁻¹) atTop (𝓝 (a + 0))
⊢ Tendsto (fun x => ↑⌈a * x⌉₊ / x) atTop (𝓝 a)
[PROOFSTEP]
rw [add_zero] at A
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a + x⁻¹) atTop (𝓝 a)
⊢ Tendsto (fun x => ↑⌈a * x⌉₊ / x) atTop (𝓝 a)
[PROOFSTEP]
apply tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds A
[GOAL]
case hgf
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a + x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, a ≤ ↑⌈a * b⌉₊ / b
[PROOFSTEP]
refine' eventually_atTop.2 ⟨1, fun x hx => _⟩
[GOAL]
case hgf
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a + x⁻¹) atTop (𝓝 a)
x : R
hx : x ≥ 1
⊢ a ≤ ↑⌈a * x⌉₊ / x
[PROOFSTEP]
rw [le_div_iff (zero_lt_one.trans_le hx)]
[GOAL]
case hgf
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a + x⁻¹) atTop (𝓝 a)
x : R
hx : x ≥ 1
⊢ a * x ≤ ↑⌈a * x⌉₊
[PROOFSTEP]
exact Nat.le_ceil _
[GOAL]
case hfh
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a + x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, ↑⌈a * b⌉₊ / b ≤ a + b⁻¹
[PROOFSTEP]
refine' eventually_atTop.2 ⟨1, fun x hx => _⟩
[GOAL]
case hfh
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a + x⁻¹) atTop (𝓝 a)
x : R
hx : x ≥ 1
⊢ ↑⌈a * x⌉₊ / x ≤ a + x⁻¹
[PROOFSTEP]
simp [div_le_iff (zero_lt_one.trans_le hx), inv_mul_cancel (zero_lt_one.trans_le hx).ne',
  (Nat.ceil_lt_add_one (mul_nonneg ha (zero_le_one.trans hx))).le, add_mul]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
⊢ Tendsto (fun x => ↑⌈x⌉₊ / x) atTop (𝓝 1)
[PROOFSTEP]
simpa using tendsto_nat_ceil_mul_div_atTop (zero_le_one' R)