α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf✝ : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K (f^[n])
x : α := fixedPoint (f^[n]) hf
⊢ IsFixedPt f x
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf✝ : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K (f^[n])
⊢ IsFixedPt f (fixedPoint (f^[n]) hf)
set x := hf.fixedPoint (f^[n])
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf✝ : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K (f^[n])
x : α := fixedPoint (f^[n]) hf
hx : (f^[n]) x = x
⊢ IsFixedPt f x
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf✝ : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K (f^[n])
x : α := fixedPoint (f^[n]) hf
⊢ IsFixedPt f x
have hx : (f^[n]) x = x := hf.fixedPoint_isFixedPt
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf✝ : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K (f^[n])
x : α := fixedPoint (f^[n]) hf
hx : (f^[n]) x = x
this : dist ((f^[n]) x) ((f^[n]) (f x)) ≤ ↑K * dist x (f x)
⊢ IsFixedPt f x
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf✝ : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K (f^[n])
x : α := fixedPoint (f^[n]) hf
hx : (f^[n]) x = x
⊢ IsFixedPt f x
have := hf.toLipschitzWith.dist_le_mul x (f x)
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf✝ : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K (f^[n])
x : α := fixedPoint (f^[n]) hf
hx : (f^[n]) x = x
this : dist x (f x) ≤ ↑K * dist x (f x)
⊢ IsFixedPt f x
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf✝ : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K (f^[n])
x : α := fixedPoint (f^[n]) hf
hx : (f^[n]) x = x
this : dist ((f^[n]) x) ((f^[n]) (f x)) ≤ ↑K * dist x (f x)
⊢ IsFixedPt f x
rw [← iterate_succ_apply, iterate_succ_apply', hx] at this
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf✝ : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K (f^[n])
x : α := fixedPoint (f^[n]) hf
hx : (f^[n]) x = x
⊢ dist x (f x) ≤ ↑K * dist x (f x) → IsFixedPt f x
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf✝ : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K (f^[n])
x : α := fixedPoint (f^[n]) hf
hx : (f^[n]) x = x
this : dist x (f x) ≤ ↑K * dist x (f x)
⊢ IsFixedPt f x
revert this
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf✝ : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K (f^[n])
x : α := fixedPoint (f^[n]) hf
hx : (f^[n]) x = x
⊢ ¬IsFixedPt f (fixedPoint (f^[n]) hf) →
    ↑K * dist (fixedPoint (f^[n]) hf) (f (fixedPoint (f^[n]) hf)) <
      dist (fixedPoint (f^[n]) hf) (f (fixedPoint (f^[n]) hf))
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf✝ : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K (f^[n])
x : α := fixedPoint (f^[n]) hf
hx : (f^[n]) x = x
⊢ dist x (f x) ≤ ↑K * dist x (f x) → IsFixedPt f x
contrapose!
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf✝ : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K (f^[n])
x : α := fixedPoint (f^[n]) hf
hx : (f^[n]) x = x
this : ¬IsFixedPt f (fixedPoint (f^[n]) hf)
⊢ ↑K * dist (fixedPoint (f^[n]) hf) (f (fixedPoint (f^[n]) hf)) <
    dist (fixedPoint (f^[n]) hf) (f (fixedPoint (f^[n]) hf))
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf✝ : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K (f^[n])
x : α := fixedPoint (f^[n]) hf
hx : (f^[n]) x = x
⊢ ¬IsFixedPt f (fixedPoint (f^[n]) hf) →
    ↑K * dist (fixedPoint (f^[n]) hf) (f (fixedPoint (f^[n]) hf)) <
      dist (fixedPoint (f^[n]) hf) (f (fixedPoint (f^[n]) hf))
intro this
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf✝ : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K (f^[n])
x : α := fixedPoint (f^[n]) hf
hx : (f^[n]) x = x
this✝ : ¬IsFixedPt f (fixedPoint (f^[n]) hf)
this : 0 < dist (fixedPoint (f^[n]) hf) (f (fixedPoint (f^[n]) hf))
⊢ ↑K * dist (fixedPoint (f^[n]) hf) (f (fixedPoint (f^[n]) hf)) <
    dist (fixedPoint (f^[n]) hf) (f (fixedPoint (f^[n]) hf))
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf✝ : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K (f^[n])
x : α := fixedPoint (f^[n]) hf
hx : (f^[n]) x = x
this : ¬IsFixedPt f (fixedPoint (f^[n]) hf)
⊢ ↑K * dist (fixedPoint (f^[n]) hf) (f (fixedPoint (f^[n]) hf)) <
    dist (fixedPoint (f^[n]) hf) (f (fixedPoint (f^[n]) hf))
have := dist_pos.2 (Ne.symm this)
no goals
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf✝ : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
n : ℕ
hf : ContractingWith K (f^[n])
x : α := fixedPoint (f^[n]) hf
hx : (f^[n]) x = x
this✝ : ¬IsFixedPt f (fixedPoint (f^[n]) hf)
this : 0 < dist (fixedPoint (f^[n]) hf) (f (fixedPoint (f^[n]) hf))
⊢ ↑K * dist (fixedPoint (f^[n]) hf) (f (fixedPoint (f^[n]) hf)) <
    dist (fixedPoint (f^[n]) hf) (f (fixedPoint (f^[n]) hf))
simpa only [NNReal.coe_one, one_mul, NNReal.val_eq_coe] using (mul_lt_mul_right this).mpr hf.left