[GOAL]
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
⊢ 0 < 1 - ↑K
[PROOFSTEP]
simp [hf.1]
[GOAL]
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
⊢ 1 - ↑K ≠ ⊤
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
⊢ ¬1 - ↑K = ⊤
[PROOFSTEP]
exact ENNReal.coe_ne_top
[GOAL]
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
h : edist x y ≠ ⊤
⊢ edist x (f x) + edist (f x) (f y) + edist (f y) y = edist x (f x) + edist y (f y) + edist (f x) (f y)
[PROOFSTEP]
rw [edist_comm y, add_right_comm]
[GOAL]
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
h : edist x y ≠ ⊤
this : edist x y ≤ edist x (f x) + edist y (f y) + ↑K * edist x y
⊢ edist x y ≤ (edist x (f x) + edist y (f y)) / (1 - ↑K)
[PROOFSTEP]
rwa [ENNReal.le_div_iff_mul_le (Or.inl hf.one_sub_K_ne_zero) (Or.inl one_sub_K_ne_top), mul_comm,
  ENNReal.sub_mul fun _ _ ↦ h, one_mul, tsub_le_iff_right]
[GOAL]
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
h : edist x y ≠ ⊤
hy : IsFixedPt f y
⊢ edist x y ≤ edist x (f x) / (1 - ↑K)
[PROOFSTEP]
simpa only [hy.eq, edist_self, add_zero] using hf.edist_inequality h
[GOAL]
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
hx : IsFixedPt f x
hy : IsFixedPt f y
⊢ x = y ∨ edist x y = ⊤
[PROOFSTEP]
refine' or_iff_not_imp_right.2 fun h ↦ edist_le_zero.1 _
[GOAL]
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
hx : IsFixedPt f x
hy : IsFixedPt f y
h : ¬edist x y = ⊤
⊢ edist x y ≤ 0
[PROOFSTEP]
simpa only [hx.eq, edist_self, add_zero, ENNReal.zero_div] using hf.edist_le_of_fixedPoint h hy
[GOAL]
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
⊢ edist x (efixedPoint f hf x hx) ≤ edist x (f x) / (1 - ↑K)
[PROOFSTEP]
convert hf.apriori_edist_iterate_efixedPoint_le hx 0
[GOAL]
case h.e'_4.h.e'_5
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
⊢ edist x (f x) = edist x (f x) * ↑K ^ 0
[PROOFSTEP]
simp only [pow_zero, mul_one]
[GOAL]
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
y : α
hy : edist y (f y) ≠ ⊤
h : edist x y ≠ ⊤
⊢ efixedPoint f hf x hx = efixedPoint f hf y hy
[PROOFSTEP]
refine' (hf.eq_or_edist_eq_top_of_fixedPoints _ _).elim id fun h' ↦ False.elim (ne_of_lt _ h')
[GOAL]
case refine'_1
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
y : α
hy : edist y (f y) ≠ ⊤
h : edist x y ≠ ⊤
⊢ IsFixedPt f (efixedPoint f hf x hx)
[PROOFSTEP]
try apply efixedPoint_isFixedPt
[GOAL]
case refine'_1
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
y : α
hy : edist y (f y) ≠ ⊤
h : edist x y ≠ ⊤
⊢ IsFixedPt f (efixedPoint f hf x hx)
[PROOFSTEP]
apply efixedPoint_isFixedPt
[GOAL]
case refine'_2
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
y : α
hy : edist y (f y) ≠ ⊤
h : edist x y ≠ ⊤
⊢ IsFixedPt f (efixedPoint f hf y hy)
[PROOFSTEP]
try apply efixedPoint_isFixedPt
[GOAL]
case refine'_2
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
y : α
hy : edist y (f y) ≠ ⊤
h : edist x y ≠ ⊤
⊢ IsFixedPt f (efixedPoint f hf y hy)
[PROOFSTEP]
apply efixedPoint_isFixedPt
[GOAL]
case refine'_3
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
y : α
hy : edist y (f y) ≠ ⊤
h : edist x y ≠ ⊤
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ⊤
⊢ edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) < ⊤
[PROOFSTEP]
try apply efixedPoint_isFixedPt
[GOAL]
case refine'_3
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
y : α
hy : edist y (f y) ≠ ⊤
h : edist x y ≠ ⊤
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ⊤
⊢ edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) < ⊤
[PROOFSTEP]
apply efixedPoint_isFixedPt
[GOAL]
case refine'_3
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
y : α
hy : edist y (f y) ≠ ⊤
h : edist x y ≠ ⊤
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ⊤
⊢ edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) < ⊤
[PROOFSTEP]
change edistLtTopSetoid.Rel _ _
[GOAL]
case refine'_3
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
y : α
hy : edist y (f y) ≠ ⊤
h : edist x y ≠ ⊤
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ⊤
⊢ Setoid.Rel edistLtTopSetoid (efixedPoint f hf x hx) (efixedPoint f hf y hy)
[PROOFSTEP]
trans x
[GOAL]
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
y : α
hy : edist y (f y) ≠ ⊤
h : edist x y ≠ ⊤
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ⊤
⊢ Setoid.Rel edistLtTopSetoid (efixedPoint f hf x hx) x
[PROOFSTEP]
apply Setoid.symm'
[GOAL]
case a
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
y : α
hy : edist y (f y) ≠ ⊤
h : edist x y ≠ ⊤
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ⊤
⊢ Setoid.Rel edistLtTopSetoid x (efixedPoint f hf x hx)
[PROOFSTEP]
exact hf.edist_efixedPoint_lt_top hx
[GOAL]
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
y : α
hy : edist y (f y) ≠ ⊤
h : edist x y ≠ ⊤
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ⊤
⊢ Setoid.Rel edistLtTopSetoid x (efixedPoint f hf y hy)
[PROOFSTEP]
trans y
[GOAL]
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
y : α
hy : edist y (f y) ≠ ⊤
h : edist x y ≠ ⊤
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ⊤
⊢ Setoid.Rel edistLtTopSetoid x y
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ⊤
y : α
hy : edist y (f y) ≠ ⊤
h : edist x y ≠ ⊤
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ⊤
⊢ Setoid.Rel edistLtTopSetoid y (efixedPoint f hf y hy)
[PROOFSTEP]
exacts [lt_top_iff_ne_top.2 h, hf.edist_efixedPoint_lt_top hy]
[GOAL]
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
⊢ ∃ y,
    y ∈ s ∧
      IsFixedPt f y ∧
        Tendsto (fun n => f^[n] x) atTop (𝓝 y) ∧ ∀ (n : ℕ), edist (f^[n] x) y ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)
[PROOFSTEP]
haveI := hsc.completeSpace_coe
[GOAL]
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
this : CompleteSpace ↑s
⊢ ∃ y,
    y ∈ s ∧
      IsFixedPt f y ∧
        Tendsto (fun n => f^[n] x) atTop (𝓝 y) ∧ ∀ (n : ℕ), edist (f^[n] x) y ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)
[PROOFSTEP]
rcases hf.exists_fixedPoint ⟨x, hxs⟩ hx with ⟨y, hfy, h_tendsto, hle⟩
[GOAL]
case intro.intro.intro
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
this : CompleteSpace ↑s
y : ↑s
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto : Tendsto (fun n => (MapsTo.restrict f s s hsf)^[n] { val := x, property := hxs }) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf)^[n] { val := x, property := hxs }) y ≤
      edist { val := x, property := hxs } (MapsTo.restrict f s s hsf { val := x, property := hxs }) * ↑K ^ n / (1 - ↑K)
⊢ ∃ y,
    y ∈ s ∧
      IsFixedPt f y ∧
        Tendsto (fun n => f^[n] x) atTop (𝓝 y) ∧ ∀ (n : ℕ), edist (f^[n] x) y ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)
[PROOFSTEP]
refine' ⟨y, y.2, Subtype.ext_iff_val.1 hfy, _, fun n ↦ _⟩
[GOAL]
case intro.intro.intro.refine'_1
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
this : CompleteSpace ↑s
y : ↑s
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto : Tendsto (fun n => (MapsTo.restrict f s s hsf)^[n] { val := x, property := hxs }) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf)^[n] { val := x, property := hxs }) y ≤
      edist { val := x, property := hxs } (MapsTo.restrict f s s hsf { val := x, property := hxs }) * ↑K ^ n / (1 - ↑K)
⊢ Tendsto (fun n => f^[n] x) atTop (𝓝 ↑y)
[PROOFSTEP]
convert (continuous_subtype_val.tendsto _).comp h_tendsto
[GOAL]
case h.e'_3.h
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
this : CompleteSpace ↑s
y : ↑s
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto : Tendsto (fun n => (MapsTo.restrict f s s hsf)^[n] { val := x, property := hxs }) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf)^[n] { val := x, property := hxs }) y ≤
      edist { val := x, property := hxs } (MapsTo.restrict f s s hsf { val := x, property := hxs }) * ↑K ^ n / (1 - ↑K)
x✝ : ℕ
⊢ f^[x✝] x = (Subtype.val ∘ fun n => (MapsTo.restrict f s s hsf)^[n] { val := x, property := hxs }) x✝
[PROOFSTEP]
simp only [(· ∘ ·), MapsTo.iterate_restrict, MapsTo.val_restrict_apply]
[GOAL]
case intro.intro.intro.refine'_2
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
this : CompleteSpace ↑s
y : ↑s
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto : Tendsto (fun n => (MapsTo.restrict f s s hsf)^[n] { val := x, property := hxs }) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf)^[n] { val := x, property := hxs }) y ≤
      edist { val := x, property := hxs } (MapsTo.restrict f s s hsf { val := x, property := hxs }) * ↑K ^ n / (1 - ↑K)
n : ℕ
⊢ edist (f^[n] x) ↑y ≤ edist x (f x) * ↑K ^ n / (1 - ↑K)
[PROOFSTEP]
convert hle n
[GOAL]
case h.e'_3
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
this : CompleteSpace ↑s
y : ↑s
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto : Tendsto (fun n => (MapsTo.restrict f s s hsf)^[n] { val := x, property := hxs }) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf)^[n] { val := x, property := hxs }) y ≤
      edist { val := x, property := hxs } (MapsTo.restrict f s s hsf { val := x, property := hxs }) * ↑K ^ n / (1 - ↑K)
n : ℕ
⊢ edist (f^[n] x) ↑y = edist ((MapsTo.restrict f s s hsf)^[n] { val := x, property := hxs }) y
[PROOFSTEP]
rw [MapsTo.iterate_restrict]
[GOAL]
case h.e'_3
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
this : CompleteSpace ↑s
y : ↑s
hfy : IsFixedPt (MapsTo.restrict f s s hsf) y
h_tendsto : Tendsto (fun n => (MapsTo.restrict f s s hsf)^[n] { val := x, property := hxs }) atTop (𝓝 y)
hle :
  ∀ (n : ℕ),
    edist ((MapsTo.restrict f s s hsf)^[n] { val := x, property := hxs }) y ≤
      edist { val := x, property := hxs } (MapsTo.restrict f s s hsf { val := x, property := hxs }) * ↑K ^ n / (1 - ↑K)
n : ℕ
⊢ edist (f^[n] x) ↑y = edist (MapsTo.restrict f^[n] s s (_ : MapsTo f^[n] s s) { val := x, property := hxs }) y
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
⊢ edist x (efixedPoint' f hsc hsf hf x hxs hx) ≤ edist x (f x) / (1 - ↑K)
[PROOFSTEP]
convert hf.apriori_edist_iterate_efixedPoint_le' hsc hsf hxs hx 0
[GOAL]
case h.e'_4.h.e'_5
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
⊢ edist x (f x) = edist x (f x) * ↑K ^ 0
[PROOFSTEP]
rw [pow_zero, mul_one]
[GOAL]
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
⊢ efixedPoint' f hsc hsf hfs x hxs hx = efixedPoint' f htc htf hft y hyt hy
[PROOFSTEP]
refine' (hf.eq_or_edist_eq_top_of_fixedPoints _ _).elim id fun h' ↦ False.elim (ne_of_lt _ h')
[GOAL]
case refine'_1
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
⊢ IsFixedPt f (efixedPoint' f hsc hsf hfs x hxs hx)
[PROOFSTEP]
try apply efixedPoint_isFixedPt'
[GOAL]
case refine'_1
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
⊢ IsFixedPt f (efixedPoint' f hsc hsf hfs x hxs hx)
[PROOFSTEP]
apply efixedPoint_isFixedPt'
[GOAL]
case refine'_2
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
⊢ IsFixedPt f (efixedPoint' f htc htf hft y hyt hy)
[PROOFSTEP]
try apply efixedPoint_isFixedPt'
[GOAL]
case refine'_2
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
⊢ IsFixedPt f (efixedPoint' f htc htf hft y hyt hy)
[PROOFSTEP]
apply efixedPoint_isFixedPt'
[GOAL]
case refine'_3
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤
⊢ edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) < ⊤
[PROOFSTEP]
try apply efixedPoint_isFixedPt'
[GOAL]
case refine'_3
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤
⊢ edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) < ⊤
[PROOFSTEP]
apply efixedPoint_isFixedPt'
[GOAL]
case refine'_3
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤
⊢ edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) < ⊤
[PROOFSTEP]
change edistLtTopSetoid.Rel _ _
[GOAL]
case refine'_3
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤
⊢ Setoid.Rel edistLtTopSetoid (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy)
[PROOFSTEP]
trans x
[GOAL]
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤
⊢ Setoid.Rel edistLtTopSetoid (efixedPoint' f hsc hsf hfs x hxs hx) x
[PROOFSTEP]
apply Setoid.symm'
[GOAL]
case a
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤
⊢ Setoid.Rel edistLtTopSetoid x (efixedPoint' f hsc hsf hfs x hxs hx)
[PROOFSTEP]
apply edist_efixedPoint_lt_top'
[GOAL]
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤
⊢ Setoid.Rel edistLtTopSetoid x (efixedPoint' f htc htf hft y hyt hy)
[PROOFSTEP]
trans y
[GOAL]
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤
⊢ Setoid.Rel edistLtTopSetoid x y
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤
⊢ Setoid.Rel edistLtTopSetoid y (efixedPoint' f htc htf hft y hyt hy)
[PROOFSTEP]
exact lt_top_iff_ne_top.2 hxy
[GOAL]
α : Type u_1
inst✝ : EMetricSpace α
cs : CompleteSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤
⊢ Setoid.Rel edistLtTopSetoid y (efixedPoint' f htc htf hft y hyt hy)
[PROOFSTEP]
apply edist_efixedPoint_lt_top'
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
this : dist x y ≤ dist x (f x) + dist y (f y) + ↑K * dist x y
⊢ dist x y ≤ (dist x (f x) + dist y (f y)) / (1 - ↑K)
[PROOFSTEP]
rwa [le_div_iff hf.one_sub_K_pos, mul_comm, _root_.sub_mul, one_mul, sub_le_iff_le_add]
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
hy : IsFixedPt f y
⊢ dist x y ≤ dist x (f x) / (1 - ↑K)
[PROOFSTEP]
simpa only [hy.eq, dist_self, add_zero] using hf.dist_inequality x y
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
g : α → α
x y : α
hx : IsFixedPt f x
hy : IsFixedPt g y
C : ℝ
hfg : ∀ (z : α), dist (f z) (g z) ≤ C
⊢ dist y (f y) / (1 - ↑K) = dist (f y) (g y) / (1 - ↑K)
[PROOFSTEP]
rw [hy.eq, dist_comm]
[GOAL]
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
n : ℕ
⊢ dist (f^[n] x) (fixedPoint f hf) ≤ dist (f^[n] x) (f^[n + 1] x) / (1 - ↑K)
[PROOFSTEP]
rw [iterate_succ']
[GOAL]
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
n : ℕ
⊢ dist (f^[n] x) (fixedPoint f hf) ≤ dist (f^[n] x) ((f ∘ f^[n]) x) / (1 - ↑K)
[PROOFSTEP]
apply hf.dist_fixedPoint_le
[GOAL]
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
⊢ Tendsto (fun n => f^[n] x) atTop (𝓝 (fixedPoint f hf))
[PROOFSTEP]
convert tendsto_iterate_efixedPoint hf (edist_ne_top x _)
[GOAL]
case h.e'_5.h.e'_3
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
⊢ fixedPoint f hf = efixedPoint f hf x (_ : edist x (f x) ≠ ⊤)
[PROOFSTEP]
refine' (fixedPoint_unique _ _).symm
[GOAL]
case h.e'_5.h.e'_3
α : Type u_1
inst✝² : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
inst✝¹ : Nonempty α
inst✝ : CompleteSpace α
x : α
⊢ IsFixedPt f (efixedPoint f hf x (_ : edist x (f x) ≠ ⊤))
[PROOFSTEP]
apply efixedPoint_isFixedPt
[GOAL]
α : 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)
[PROOFSTEP]
set x := hf.fixedPoint f^[n]
[GOAL]
α : 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
[PROOFSTEP]
have hx : f^[n] x = x := hf.fixedPoint_isFixedPt
[GOAL]
α : 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
[PROOFSTEP]
have := hf.toLipschitzWith.dist_le_mul x (f x)
[GOAL]
α : 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
[PROOFSTEP]
rw [← iterate_succ_apply, iterate_succ_apply', hx] at this 
[GOAL]
α : 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
[PROOFSTEP]
revert this
[GOAL]
α : 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
[PROOFSTEP]
contrapose!
[GOAL]
α : 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))
[PROOFSTEP]
intro this
[GOAL]
α : 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))
[PROOFSTEP]
have := dist_pos.2 (Ne.symm this)
[GOAL]
α : 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))
[PROOFSTEP]
simpa only [NNReal.coe_one, one_mul, NNReal.val_eq_coe] using (mul_lt_mul_right this).mpr hf.left
