[GOAL]
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a b : α
⊢ (fun n => dist a (x n) - dist (x 0) (x n)) ∈ lp (fun i => ℝ) ⊤
[PROOFSTEP]
apply memℓp_infty
[GOAL]
case hf
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a b : α
⊢ BddAbove (range fun i => ‖(fun n => dist a (x n) - dist (x 0) (x n)) i‖)
[PROOFSTEP]
use dist a (x 0)
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a b : α
⊢ dist a (x 0) ∈ upperBounds (range fun i => ‖(fun n => dist a (x n) - dist (x 0) (x n)) i‖)
[PROOFSTEP]
rintro - ⟨n, rfl⟩
[GOAL]
case h.intro
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n✝ : ℕ
C : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a b : α
n : ℕ
⊢ (fun i => ‖(fun n => dist a (x n) - dist (x 0) (x n)) i‖) n ≤ dist a (x 0)
[PROOFSTEP]
exact abs_dist_sub_le _ _ _
[GOAL]
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ a b : α
⊢ dist (embeddingOfSubset x a) (embeddingOfSubset x b) ≤ dist a b
[PROOFSTEP]
refine' lp.norm_le_of_forall_le dist_nonneg fun n => _
[GOAL]
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n✝ : ℕ
C : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ a b : α
n : ℕ
⊢ ‖↑(embeddingOfSubset x a - embeddingOfSubset x b) n‖ ≤ dist a b
[PROOFSTEP]
simp only [lp.coeFn_sub, Pi.sub_apply, embeddingOfSubset_coe, Real.dist_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n✝ : ℕ
C : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ a b : α
n : ℕ
⊢ ‖dist a (x n) - dist (x 0) (x n) - (dist b (x n) - dist (x 0) (x n))‖ ≤ dist a b
[PROOFSTEP]
convert abs_dist_sub_le a b (x n) using 2
[GOAL]
case h.e'_3.h.e'_1
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n✝ : ℕ
C : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ a b : α
n : ℕ
⊢ dist a (x n) - dist (x 0) (x n) - (dist b (x n) - dist (x 0) (x n)) = dist a (x n) - dist b (x n)
[PROOFSTEP]
ring
[GOAL]
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a b : α
H : DenseRange x
⊢ Isometry (embeddingOfSubset x)
[PROOFSTEP]
refine' Isometry.of_dist_eq fun a b => _
[GOAL]
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
⊢ dist (embeddingOfSubset x a) (embeddingOfSubset x b) = dist a b
[PROOFSTEP]
refine'
  (embeddingOfSubset_dist_le x a b).antisymm
    (le_of_forall_pos_le_add fun e epos => _)
      -- First step: find n with dist a (x n) < e
[GOAL]
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
⊢ dist a b ≤ dist (embeddingOfSubset x a) (embeddingOfSubset x b) + e
[PROOFSTEP]
rcases Metric.mem_closure_range_iff.1 (H a) (e / 2) (half_pos epos) with
  ⟨n, hn⟩
    -- Second step: use the norm control at index n to conclude
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n✝ : ℕ
C : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
⊢ dist a b ≤ dist (embeddingOfSubset x a) (embeddingOfSubset x b) + e
[PROOFSTEP]
have C : dist b (x n) - dist a (x n) = embeddingOfSubset x b n - embeddingOfSubset x a n := by
  simp only [embeddingOfSubset_coe, sub_sub_sub_cancel_right]
[GOAL]
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n✝ : ℕ
C : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
⊢ dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
[PROOFSTEP]
simp only [embeddingOfSubset_coe, sub_sub_sub_cancel_right]
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ dist a b ≤ dist (embeddingOfSubset x a) (embeddingOfSubset x b) + e
[PROOFSTEP]
have :=
  calc
    dist a b ≤ dist a (x n) + dist (x n) b := dist_triangle _ _ _
    _ = 2 * dist a (x n) + (dist b (x n) - dist a (x n)) := by simp [dist_comm]; ring
    _ ≤ 2 * dist a (x n) + |dist b (x n) - dist a (x n)| := by apply_rules [add_le_add_left, le_abs_self]
    _ ≤ 2 * (e / 2) + |embeddingOfSubset x b n - embeddingOfSubset x a n| :=
      by
      rw [C]
      apply_rules [add_le_add, mul_le_mul_of_nonneg_left, hn.le, le_refl]
      norm_num
    _ ≤ 2 * (e / 2) + dist (embeddingOfSubset x b) (embeddingOfSubset x a) :=
      by
      have :
        |embeddingOfSubset x b n - embeddingOfSubset x a n| ≤ dist (embeddingOfSubset x b) (embeddingOfSubset x a) :=
        by
        simp only [dist_eq_norm]
        exact lp.norm_apply_le_norm ENNReal.top_ne_zero (embeddingOfSubset x b - embeddingOfSubset x a) n
      nlinarith
    _ = dist (embeddingOfSubset x b) (embeddingOfSubset x a) + e := by ring
[GOAL]
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ dist a (x n) + dist (x n) b = 2 * dist a (x n) + (dist b (x n) - dist a (x n))
[PROOFSTEP]
simp [dist_comm]
[GOAL]
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ dist a (x n) + dist b (x n) = 2 * dist a (x n) + (dist b (x n) - dist a (x n))
[PROOFSTEP]
ring
[GOAL]
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ 2 * dist a (x n) + (dist b (x n) - dist a (x n)) ≤ 2 * dist a (x n) + |dist b (x n) - dist a (x n)|
[PROOFSTEP]
apply_rules [add_le_add_left, le_abs_self]
[GOAL]
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ 2 * dist a (x n) + |dist b (x n) - dist a (x n)| ≤
    2 * (e / 2) + |↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n|
[PROOFSTEP]
rw [C]
[GOAL]
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ 2 * dist a (x n) + |↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n| ≤
    2 * (e / 2) + |↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n|
[PROOFSTEP]
apply_rules [add_le_add, mul_le_mul_of_nonneg_left, hn.le, le_refl]
[GOAL]
case h₁.a0
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
C_symm : ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n = dist b (x n) - dist a (x n)
⊢ 0 ≤ 2
[PROOFSTEP]
norm_num
[GOAL]
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ 2 * (e / 2) + |↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n| ≤
    2 * (e / 2) + dist (embeddingOfSubset x b) (embeddingOfSubset x a)
[PROOFSTEP]
have : |embeddingOfSubset x b n - embeddingOfSubset x a n| ≤ dist (embeddingOfSubset x b) (embeddingOfSubset x a) :=
  by
  simp only [dist_eq_norm]
  exact lp.norm_apply_le_norm ENNReal.top_ne_zero (embeddingOfSubset x b - embeddingOfSubset x a) n
[GOAL]
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ |↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n| ≤ dist (embeddingOfSubset x b) (embeddingOfSubset x a)
[PROOFSTEP]
simp only [dist_eq_norm]
[GOAL]
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ |↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n| ≤ ‖embeddingOfSubset x b - embeddingOfSubset x a‖
[PROOFSTEP]
exact lp.norm_apply_le_norm ENNReal.top_ne_zero (embeddingOfSubset x b - embeddingOfSubset x a) n
[GOAL]
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
this : |↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n| ≤ dist (embeddingOfSubset x b) (embeddingOfSubset x a)
⊢ 2 * (e / 2) + |↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n| ≤
    2 * (e / 2) + dist (embeddingOfSubset x b) (embeddingOfSubset x a)
[PROOFSTEP]
nlinarith
[GOAL]
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ 2 * (e / 2) + dist (embeddingOfSubset x b) (embeddingOfSubset x a) =
    dist (embeddingOfSubset x b) (embeddingOfSubset x a) + e
[PROOFSTEP]
ring
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
this : dist a b ≤ dist (embeddingOfSubset x b) (embeddingOfSubset x a) + e
⊢ dist a b ≤ dist (embeddingOfSubset x a) (embeddingOfSubset x b) + e
[PROOFSTEP]
simpa [dist_comm] using this
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝² : MetricSpace α✝
x : ℕ → α✝
a b : α✝
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
⊢ ∃ f, Isometry f
[PROOFSTEP]
cases' (univ : Set α).eq_empty_or_nonempty with h h
[GOAL]
case inl
α✝ : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝² : MetricSpace α✝
x : ℕ → α✝
a b : α✝
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
h : univ = ∅
⊢ ∃ f, Isometry f
[PROOFSTEP]
use fun _ => 0
[GOAL]
case h
α✝ : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝² : MetricSpace α✝
x : ℕ → α✝
a b : α✝
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
h : univ = ∅
⊢ Isometry fun x => 0
[PROOFSTEP]
intro x
[GOAL]
case h
α✝ : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝² : MetricSpace α✝
x✝ : ℕ → α✝
a b : α✝
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
h : univ = ∅
x : α
⊢ ∀ (x2 : α), edist ((fun x => 0) x) ((fun x => 0) x2) = edist x x2
[PROOFSTEP]
exact absurd h (Nonempty.ne_empty ⟨x, mem_univ x⟩)
[GOAL]
case inr
α✝ : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝² : MetricSpace α✝
x : ℕ → α✝
a b : α✝
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
h : Set.Nonempty univ
⊢ ∃ f, Isometry f
[PROOFSTEP]
rcases h with ⟨basepoint⟩
[GOAL]
case inr.intro
α✝ : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝² : MetricSpace α✝
x : ℕ → α✝
a b : α✝
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
basepoint : α
h✝ : basepoint ∈ univ
⊢ ∃ f, Isometry f
[PROOFSTEP]
haveI : Inhabited α := ⟨basepoint⟩
[GOAL]
case inr.intro
α✝ : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝² : MetricSpace α✝
x : ℕ → α✝
a b : α✝
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
basepoint : α
h✝ : basepoint ∈ univ
this : Inhabited α
⊢ ∃ f, Isometry f
[PROOFSTEP]
have : ∃ s : Set α, s.Countable ∧ Dense s := exists_countable_dense α
[GOAL]
case inr.intro
α✝ : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝² : MetricSpace α✝
x : ℕ → α✝
a b : α✝
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
basepoint : α
h✝ : basepoint ∈ univ
this✝ : Inhabited α
this : ∃ s, Set.Countable s ∧ Dense s
⊢ ∃ f, Isometry f
[PROOFSTEP]
rcases this with ⟨S, ⟨S_countable, S_dense⟩⟩
[GOAL]
case inr.intro.intro.intro
α✝ : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝² : MetricSpace α✝
x : ℕ → α✝
a b : α✝
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
basepoint : α
h✝ : basepoint ∈ univ
this : Inhabited α
S : Set α
S_countable : Set.Countable S
S_dense : Dense S
⊢ ∃ f, Isometry f
[PROOFSTEP]
rcases Set.countable_iff_exists_subset_range.1 S_countable with
  ⟨x, x_range⟩
    -- Use embeddingOfSubset to construct the desired isometry
[GOAL]
case inr.intro.intro.intro.intro
α✝ : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun i => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝² : MetricSpace α✝
x✝ : ℕ → α✝
a b : α✝
α : Type u
inst✝¹ : MetricSpace α
inst✝ : SeparableSpace α
basepoint : α
h✝ : basepoint ∈ univ
this : Inhabited α
S : Set α
S_countable : Set.Countable S
S_dense : Dense S
x : ℕ → α
x_range : S ⊆ range x
⊢ ∃ f, Isometry f
[PROOFSTEP]
exact ⟨embeddingOfSubset x, embeddingOfSubset_isometry x (S_dense.mono x_range)⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
f : α → { x // x ∈ lp (fun i => ℝ) ⊤ }
K : ℝ≥0
hfl : LipschitzOnWith K f s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s
[PROOFSTEP]
rw [LipschitzOnWith.coordinate] at hfl
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
f : α → { x // x ∈ lp (fun i => ℝ) ⊤ }
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s
[PROOFSTEP]
have : ∀ i : ι, ∃ g : α → ℝ, LipschitzWith K g ∧ EqOn (fun x => f x i) g s
[GOAL]
case this
α : Type u
β : Type v
γ : Type w
ι : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
f : α → { x // x ∈ lp (fun i => ℝ) ⊤ }
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
⊢ ∀ (i : ι), ∃ g, LipschitzWith K g ∧ EqOn (fun x => ↑(f x) i) g s
[PROOFSTEP]
intro i
[GOAL]
case this
α : Type u
β : Type v
γ : Type w
ι : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
f : α → { x // x ∈ lp (fun i => ℝ) ⊤ }
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
i : ι
⊢ ∃ g, LipschitzWith K g ∧ EqOn (fun x => ↑(f x) i) g s
[PROOFSTEP]
exact
  LipschitzOnWith.extend_real
    (hfl i)
      -- use the nonlinear Hahn-Banach theorem here!
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
f : α → { x // x ∈ lp (fun i => ℝ) ⊤ }
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
this : ∀ (i : ι), ∃ g, LipschitzWith K g ∧ EqOn (fun x => ↑(f x) i) g s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s
[PROOFSTEP]
choose g hgl hgeq using this
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
f : α → { x // x ∈ lp (fun i => ℝ) ⊤ }
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x => ↑(f x) i) (g i) s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s
[PROOFSTEP]
rcases s.eq_empty_or_nonempty with rfl | ⟨a₀, ha₀_in_s⟩
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
ι : Type u_1
inst✝ : PseudoMetricSpace α
f : α → { x // x ∈ lp (fun i => ℝ) ⊤ }
K : ℝ≥0
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) ∅
hgeq : ∀ (i : ι), EqOn (fun x => ↑(f x) i) (g i) ∅
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g ∅
[PROOFSTEP]
exact ⟨0, LipschitzWith.const' 0, by simp⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type u_1
inst✝ : PseudoMetricSpace α
f : α → { x // x ∈ lp (fun i => ℝ) ⊤ }
K : ℝ≥0
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) ∅
hgeq : ∀ (i : ι), EqOn (fun x => ↑(f x) i) (g i) ∅
⊢ EqOn f 0 ∅
[PROOFSTEP]
simp
[GOAL]
case inr.intro
α : Type u
β : Type v
γ : Type w
ι : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
f : α → { x // x ∈ lp (fun i => ℝ) ⊤ }
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x => ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s
[PROOFSTEP]
have hf_extb : ∀ a : α, Memℓp (swap g a) ∞
[GOAL]
case hf_extb
α : Type u
β : Type v
γ : Type w
ι : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
f : α → { x // x ∈ lp (fun i => ℝ) ⊤ }
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x => ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
⊢ ∀ (a : α), Memℓp (swap g a) ⊤
[PROOFSTEP]
apply LipschitzWith.uniformly_bounded (swap g) hgl a₀
[GOAL]
case hf_extb
α : Type u
β : Type v
γ : Type w
ι : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
f : α → { x // x ∈ lp (fun i => ℝ) ⊤ }
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x => ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
⊢ Memℓp (swap g a₀) ⊤
[PROOFSTEP]
use‖f a₀‖
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
ι : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
f : α → { x // x ∈ lp (fun i => ℝ) ⊤ }
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x => ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
⊢ ‖f a₀‖ ∈ upperBounds (range fun i => ‖swap g a₀ i‖)
[PROOFSTEP]
rintro - ⟨i, rfl⟩
[GOAL]
case h.intro
α : Type u
β : Type v
γ : Type w
ι : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
f : α → { x // x ∈ lp (fun i => ℝ) ⊤ }
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x => ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
i : ι
⊢ (fun i => ‖swap g a₀ i‖) i ≤ ‖f a₀‖
[PROOFSTEP]
simp_rw [← hgeq i ha₀_in_s]
[GOAL]
case h.intro
α : Type u
β : Type v
γ : Type w
ι : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
f : α → { x // x ∈ lp (fun i => ℝ) ⊤ }
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x => ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
i : ι
⊢ ‖↑(f a₀) i‖ ≤ ‖f a₀‖
[PROOFSTEP]
exact lp.norm_apply_le_norm top_ne_zero (f a₀) i
[GOAL]
case inr.intro
α : Type u
β : Type v
γ : Type w
ι : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
f : α → { x // x ∈ lp (fun i => ℝ) ⊤ }
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x => ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (swap g a) ⊤
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s
[PROOFSTEP]
let f_ext' : α → ℓ^∞(ι) := fun i ↦ ⟨swap g i, hf_extb i⟩
[GOAL]
case inr.intro
α : Type u
β : Type v
γ : Type w
ι : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
f : α → { x // x ∈ lp (fun i => ℝ) ⊤ }
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x => ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (swap g a) ⊤
f_ext' : α → { x // x ∈ lp (fun i => ℝ) ⊤ } := fun i => { val := swap g i, property := (_ : Memℓp (swap g i) ⊤) }
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s
[PROOFSTEP]
refine ⟨f_ext', ?_, ?_⟩
[GOAL]
case inr.intro.refine_1
α : Type u
β : Type v
γ : Type w
ι : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
f : α → { x // x ∈ lp (fun i => ℝ) ⊤ }
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x => ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (swap g a) ⊤
f_ext' : α → { x // x ∈ lp (fun i => ℝ) ⊤ } := fun i => { val := swap g i, property := (_ : Memℓp (swap g i) ⊤) }
⊢ LipschitzWith K f_ext'
[PROOFSTEP]
rw [LipschitzWith.coordinate]
[GOAL]
case inr.intro.refine_1
α : Type u
β : Type v
γ : Type w
ι : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
f : α → { x // x ∈ lp (fun i => ℝ) ⊤ }
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x => ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (swap g a) ⊤
f_ext' : α → { x // x ∈ lp (fun i => ℝ) ⊤ } := fun i => { val := swap g i, property := (_ : Memℓp (swap g i) ⊤) }
⊢ ∀ (i : ι), LipschitzWith K fun a => ↑(f_ext' a) i
[PROOFSTEP]
exact hgl
[GOAL]
case inr.intro.refine_2
α : Type u
β : Type v
γ : Type w
ι : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
f : α → { x // x ∈ lp (fun i => ℝ) ⊤ }
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x => ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (swap g a) ⊤
f_ext' : α → { x // x ∈ lp (fun i => ℝ) ⊤ } := fun i => { val := swap g i, property := (_ : Memℓp (swap g i) ⊤) }
⊢ EqOn f f_ext' s
[PROOFSTEP]
intro a hyp
[GOAL]
case inr.intro.refine_2
α : Type u
β : Type v
γ : Type w
ι : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
f : α → { x // x ∈ lp (fun i => ℝ) ⊤ }
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x => ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (swap g a) ⊤
f_ext' : α → { x // x ∈ lp (fun i => ℝ) ⊤ } := fun i => { val := swap g i, property := (_ : Memℓp (swap g i) ⊤) }
a : α
hyp : a ∈ s
⊢ f a = f_ext' a
[PROOFSTEP]
ext i
[GOAL]
case inr.intro.refine_2.h.h
α : Type u
β : Type v
γ : Type w
ι : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
f : α → { x // x ∈ lp (fun i => ℝ) ⊤ }
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a => ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x => ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (swap g a) ⊤
f_ext' : α → { x // x ∈ lp (fun i => ℝ) ⊤ } := fun i => { val := swap g i, property := (_ : Memℓp (swap g i) ⊤) }
a : α
hyp : a ∈ s
i : ι
⊢ ↑(f a) i = ↑(f_ext' a) i
[PROOFSTEP]
exact (hgeq i) hyp


[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


[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
⊢ ∀ (p q : β × β), dist (p.fst * p.snd) (q.fst * q.snd) ≤ ↑(LipschitzMul.C β) * dist p q
[PROOFSTEP]
rw [← lipschitzWith_iff_dist_le_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
⊢ LipschitzWith (LipschitzMul.C β) fun p => p.fst * p.snd
[PROOFSTEP]
exact lipschitzWith_lipschitz_const_mul_edist
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
s : Submonoid β
⊢ LipschitzWith (LipschitzMul.C β) fun p => p.fst * p.snd
[PROOFSTEP]
rintro ⟨x₁, x₂⟩ ⟨y₁, y₂⟩
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
s : Submonoid β
x₁ x₂ y₁ y₂ : { x // x ∈ s }
⊢ edist ((fun p => p.fst * p.snd) (x₁, x₂)) ((fun p => p.fst * p.snd) (y₁, y₂)) ≤
    ↑(LipschitzMul.C β) * edist (x₁, x₂) (y₁, y₂)
[PROOFSTEP]
convert lipschitzWith_lipschitz_const_mul_edist ⟨(x₁ : β), x₂⟩ ⟨y₁, y₂⟩ using 1
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
p q : ℝ × ℝ
⊢ dist (p.fst + p.snd) (q.fst + q.snd) ≤ ↑2 * dist p q
[PROOFSTEP]
simp only [Real.dist_eq, Prod.dist_eq, Prod.fst_sub, Prod.snd_sub, NNReal.coe_ofNat, add_sub_add_comm, two_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
p q : ℝ × ℝ
⊢ |p.fst - q.fst + (p.snd - q.snd)| ≤ max |p.fst - q.fst| |p.snd - q.snd| + max |p.fst - q.fst| |p.snd - q.snd|
[PROOFSTEP]
refine le_trans (abs_add (p.1 - q.1) (p.2 - q.2)) ?_
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
p q : ℝ × ℝ
⊢ |p.fst - q.fst| + |p.snd - q.snd| ≤ max |p.fst - q.fst| |p.snd - q.snd| + max |p.fst - q.fst| |p.snd - q.snd|
[PROOFSTEP]
exact add_le_add (le_max_left _ _) (le_max_right _ _)
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
⊢ LipschitzWith (LipschitzAdd.C ℝ) fun p => p.fst + p.snd
[PROOFSTEP]
rintro ⟨x₁, x₂⟩ ⟨y₁, y₂⟩
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
x₁ x₂ y₁ y₂ : ℝ≥0
⊢ edist ((fun p => p.fst + p.snd) (x₁, x₂)) ((fun p => p.fst + p.snd) (y₁, y₂)) ≤
    ↑(LipschitzAdd.C ℝ) * edist (x₁, x₂) (y₁, y₂)
[PROOFSTEP]
exact lipschitzWith_lipschitz_const_add_edist ⟨(x₁ : ℝ), x₂⟩ ⟨y₁, y₂⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
⊢ Continuous fun p => p.fst • p.snd
[PROOFSTEP]
rw [Metric.continuous_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
⊢ ∀ (b : α × β) (ε : ℝ), ε > 0 → ∃ δ, δ > 0 ∧ ∀ (a : α × β), dist a b < δ → dist (a.fst • a.snd) (b.fst • b.snd) < ε
[PROOFSTEP]
rintro ⟨a, b⟩ ε ε0
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
a : α
b : β
ε : ℝ
ε0 : ε > 0
⊢ ∃ δ, δ > 0 ∧ ∀ (a_1 : α × β), dist a_1 (a, b) < δ → dist (a_1.fst • a_1.snd) ((a, b).fst • (a, b).snd) < ε
[PROOFSTEP]
obtain ⟨δ, δ0, hδε⟩ : ∃ δ > 0, δ * (δ + dist b 0) + dist a 0 * δ < ε
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
a : α
b : β
ε : ℝ
ε0 : ε > 0
⊢ ∃ δ, δ > 0 ∧ δ * (δ + dist b 0) + dist a 0 * δ < ε
[PROOFSTEP]
have : Continuous fun δ ↦ δ * (δ + dist b 0) + dist a 0 * δ := by continuity
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
a : α
b : β
ε : ℝ
ε0 : ε > 0
⊢ Continuous fun δ => δ * (δ + dist b 0) + dist a 0 * δ
[PROOFSTEP]
continuity
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
a : α
b : β
ε : ℝ
ε0 : ε > 0
this : Continuous fun δ => δ * (δ + dist b 0) + dist a 0 * δ
⊢ ∃ δ, δ > 0 ∧ δ * (δ + dist b 0) + dist a 0 * δ < ε
[PROOFSTEP]
refine ((this.tendsto' _ _ ?_).eventually (gt_mem_nhds ε0)).exists_gt
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
a : α
b : β
ε : ℝ
ε0 : ε > 0
this : Continuous fun δ => δ * (δ + dist b 0) + dist a 0 * δ
⊢ 0 * (0 + dist b 0) + dist a 0 * 0 = 0
[PROOFSTEP]
simp
[GOAL]
case mk.intro.intro
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
a : α
b : β
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδε : δ * (δ + dist b 0) + dist a 0 * δ < ε
⊢ ∃ δ, δ > 0 ∧ ∀ (a_1 : α × β), dist a_1 (a, b) < δ → dist (a_1.fst • a_1.snd) ((a, b).fst • (a, b).snd) < ε
[PROOFSTEP]
refine ⟨δ, δ0, fun (a', b') hab' => ?_⟩
[GOAL]
case mk.intro.intro
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
a : α
b : β
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδε : δ * (δ + dist b 0) + dist a 0 * δ < ε
x✝ : α × β
a' : α
b' : β
hab' : dist (a', b') (a, b) < δ
⊢ dist ((a', b').fst • (a', b').snd) ((a, b).fst • (a, b).snd) < ε
[PROOFSTEP]
obtain ⟨ha, hb⟩ := max_lt_iff.1 hab'
[GOAL]
case mk.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
a : α
b : β
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδε : δ * (δ + dist b 0) + dist a 0 * δ < ε
x✝ : α × β
a' : α
b' : β
hab' : dist (a', b') (a, b) < δ
ha : dist (a', b').fst (a, b).fst < δ
hb : dist (a', b').snd (a, b).snd < δ
⊢ dist ((a', b').fst • (a', b').snd) ((a, b).fst • (a, b).snd) < ε
[PROOFSTEP]
calc
  dist (a' • b') (a • b) ≤ dist (a' • b') (a • b') + dist (a • b') (a • b) := dist_triangle ..
  _ ≤ dist a' a * dist b' 0 + dist a 0 * dist b' b := (add_le_add (dist_pair_smul _ _ _) (dist_smul_pair _ _ _))
  _ ≤ δ * (δ + dist b 0) + dist a 0 * δ :=
    by
    have : dist b' 0 ≤ δ + dist b 0 := (dist_triangle _ _ _).trans <| add_le_add_right hb.le _
    mono* <;> apply_rules [dist_nonneg, le_of_lt]
  _ < ε := hδε
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
a : α
b : β
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδε : δ * (δ + dist b 0) + dist a 0 * δ < ε
x✝ : α × β
a' : α
b' : β
hab' : dist (a', b') (a, b) < δ
ha : dist (a', b').fst (a, b).fst < δ
hb : dist (a', b').snd (a, b).snd < δ
⊢ dist a' a * dist b' 0 + dist a 0 * dist b' b ≤ δ * (δ + dist b 0) + dist a 0 * δ
[PROOFSTEP]
have : dist b' 0 ≤ δ + dist b 0 := (dist_triangle _ _ _).trans <| add_le_add_right hb.le _
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
a : α
b : β
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδε : δ * (δ + dist b 0) + dist a 0 * δ < ε
x✝ : α × β
a' : α
b' : β
hab' : dist (a', b') (a, b) < δ
ha : dist (a', b').fst (a, b).fst < δ
hb : dist (a', b').snd (a, b).snd < δ
this : dist b' 0 ≤ δ + dist b 0
⊢ dist a' a * dist b' 0 + dist a 0 * dist b' b ≤ δ * (δ + dist b 0) + dist a 0 * δ
[PROOFSTEP]
mono*
[GOAL]
case h₁.h₁
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
a : α
b : β
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδε : δ * (δ + dist b 0) + dist a 0 * δ < ε
x✝ : α × β
a' : α
b' : β
hab' : dist (a', b') (a, b) < δ
ha : dist (a', b').fst (a, b).fst < δ
hb : dist (a', b').snd (a, b).snd < δ
this : dist b' 0 ≤ δ + dist b 0
⊢ dist a' a ≤ δ
[PROOFSTEP]
apply_rules [dist_nonneg, le_of_lt]
[GOAL]
case h₁.c0
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
a : α
b : β
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδε : δ * (δ + dist b 0) + dist a 0 * δ < ε
x✝ : α × β
a' : α
b' : β
hab' : dist (a', b') (a, b) < δ
ha : dist (a', b').fst (a, b).fst < δ
hb : dist (a', b').snd (a, b).snd < δ
this : dist b' 0 ≤ δ + dist b 0
⊢ 0 ≤ dist b' 0
[PROOFSTEP]
apply_rules [dist_nonneg, le_of_lt]
[GOAL]
case h₁.b0
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
a : α
b : β
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδε : δ * (δ + dist b 0) + dist a 0 * δ < ε
x✝ : α × β
a' : α
b' : β
hab' : dist (a', b') (a, b) < δ
ha : dist (a', b').fst (a, b).fst < δ
hb : dist (a', b').snd (a, b).snd < δ
this : dist b' 0 ≤ δ + dist b 0
⊢ 0 ≤ δ
[PROOFSTEP]
apply_rules [dist_nonneg, le_of_lt]
[GOAL]
case h₂.h₂
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
a : α
b : β
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδε : δ * (δ + dist b 0) + dist a 0 * δ < ε
x✝ : α × β
a' : α
b' : β
hab' : dist (a', b') (a, b) < δ
ha : dist (a', b').fst (a, b).fst < δ
hb : dist (a', b').snd (a, b).snd < δ
this : dist b' 0 ≤ δ + dist b 0
⊢ dist b' b ≤ δ
[PROOFSTEP]
apply_rules [dist_nonneg, le_of_lt]
[GOAL]
case h₂.c0
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
a : α
b : β
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδε : δ * (δ + dist b 0) + dist a 0 * δ < ε
x✝ : α × β
a' : α
b' : β
hab' : dist (a', b') (a, b) < δ
ha : dist (a', b').fst (a, b).fst < δ
hb : dist (a', b').snd (a, b).snd < δ
this : dist b' 0 ≤ δ + dist b 0
⊢ 0 ≤ dist b' b
[PROOFSTEP]
apply_rules [dist_nonneg, le_of_lt]
[GOAL]
case h₂.b0
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
a : α
b : β
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδε : δ * (δ + dist b 0) + dist a 0 * δ < ε
x✝ : α × β
a' : α
b' : β
hab' : dist (a', b') (a, b) < δ
ha : dist (a', b').fst (a, b).fst < δ
hb : dist (a', b').snd (a, b).snd < δ
this : dist b' 0 ≤ δ + dist b 0
⊢ 0 ≤ dist a 0
[PROOFSTEP]
apply_rules [dist_nonneg, le_of_lt]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
x y₁ y₂ : ℝ
⊢ dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂
[PROOFSTEP]
simpa [Real.dist_eq, mul_sub] using (abs_mul x (y₁ - y₂)).le
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
x₁ x₂ y : ℝ
⊢ dist (x₁ • y) (x₂ • y) ≤ dist x₁ x₂ * dist y 0
[PROOFSTEP]
simpa [Real.dist_eq, sub_mul] using (abs_mul (x₁ - x₂) y).le
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
x y₁ y₂ : ℝ≥0
⊢ dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂
[PROOFSTEP]
convert dist_smul_pair (x : ℝ) (y₁ : ℝ) y₂ using 1
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : SMul α β
inst✝ : BoundedSMul α β
x₁ x₂ y : ℝ≥0
⊢ dist (x₁ • y) (x₂ • y) ≤ dist x₁ x₂ * dist y 0
[PROOFSTEP]
convert dist_pair_smul (x₁ : ℝ) x₂ (y : ℝ) using 1
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁷ : PseudoMetricSpace α
inst✝⁶ : PseudoMetricSpace β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMul α β
inst✝² : BoundedSMul α β
inst✝¹ : SMul αᵐᵒᵖ β
inst✝ : IsCentralScalar α β
x : α
y₁ y₂ : β
⊢ dist (MulOpposite.op x • y₁) (MulOpposite.op x • y₂) ≤ dist (MulOpposite.op x) 0 * dist y₁ y₂
[PROOFSTEP]
simpa only [op_smul_eq_smul] using dist_smul_pair x y₁ y₂
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁷ : PseudoMetricSpace α
inst✝⁶ : PseudoMetricSpace β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMul α β
inst✝² : BoundedSMul α β
inst✝¹ : SMul αᵐᵒᵖ β
inst✝ : IsCentralScalar α β
x₁ x₂ : α
y : β
⊢ dist (MulOpposite.op x₁ • y) (MulOpposite.op x₂ • y) ≤ dist (MulOpposite.op x₁) (MulOpposite.op x₂) * dist y 0
[PROOFSTEP]
simpa only [op_smul_eq_smul] using dist_pair_smul x₁ x₂ y


[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
⊢ EquicontinuousAt F x₀ ↔
    ∀ (ε : ℝ), ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ U → ∀ (x' : β), x' ∈ U → ∀ (i : ι), dist (F i x) (F i x') < ε
[PROOFSTEP]
rw [equicontinuousAt_iff_pair]
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
⊢ (∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ V, V ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ V → ∀ (y : β), y ∈ V → ∀ (i : ι), (F i x, F i y) ∈ U) ↔
    ∀ (ε : ℝ), ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ U → ∀ (x' : β), x' ∈ U → ∀ (i : ι), dist (F i x) (F i x') < ε
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
ι✝ : Type u_3
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
⊢ (∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ V, V ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ V → ∀ (y : β), y ∈ V → ∀ (i : ι), (F i x, F i y) ∈ U) →
    ∀ (ε : ℝ), ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ U → ∀ (x' : β), x' ∈ U → ∀ (i : ι), dist (F i x) (F i x') < ε
[PROOFSTEP]
intro H
[GOAL]
case mpr
α : Type u_1
β : Type u_2
ι✝ : Type u_3
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
⊢ (∀ (ε : ℝ), ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ U → ∀ (x' : β), x' ∈ U → ∀ (i : ι), dist (F i x) (F i x') < ε) →
    ∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ V, V ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ V → ∀ (y : β), y ∈ V → ∀ (i : ι), (F i x, F i y) ∈ U
[PROOFSTEP]
intro H
[GOAL]
case mp
α : Type u_1
β : Type u_2
ι✝ : Type u_3
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
H : ∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ V, V ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ V → ∀ (y : β), y ∈ V → ∀ (i : ι), (F i x, F i y) ∈ U
⊢ ∀ (ε : ℝ), ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ U → ∀ (x' : β), x' ∈ U → ∀ (i : ι), dist (F i x) (F i x') < ε
[PROOFSTEP]
intro ε hε
[GOAL]
case mp
α : Type u_1
β : Type u_2
ι✝ : Type u_3
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
H : ∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ V, V ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ V → ∀ (y : β), y ∈ V → ∀ (i : ι), (F i x, F i y) ∈ U
ε : ℝ
hε : ε > 0
⊢ ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ U → ∀ (x' : β), x' ∈ U → ∀ (i : ι), dist (F i x) (F i x') < ε
[PROOFSTEP]
exact H _ (dist_mem_uniformity hε)
[GOAL]
case mpr
α : Type u_1
β : Type u_2
ι✝ : Type u_3
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
H : ∀ (ε : ℝ), ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ U → ∀ (x' : β), x' ∈ U → ∀ (i : ι), dist (F i x) (F i x') < ε
⊢ ∀ (U : Set (α × α)), U ∈ 𝓤 α → ∃ V, V ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ V → ∀ (y : β), y ∈ V → ∀ (i : ι), (F i x, F i y) ∈ U
[PROOFSTEP]
intro U hU
[GOAL]
case mpr
α : Type u_1
β : Type u_2
ι✝ : Type u_3
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
H : ∀ (ε : ℝ), ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ U → ∀ (x' : β), x' ∈ U → ∀ (i : ι), dist (F i x) (F i x') < ε
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∃ V, V ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ V → ∀ (y : β), y ∈ V → ∀ (i : ι), (F i x, F i y) ∈ U
[PROOFSTEP]
rcases mem_uniformity_dist.mp hU with ⟨ε, hε, hεU⟩
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
ι✝ : Type u_3
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
H : ∀ (ε : ℝ), ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ U → ∀ (x' : β), x' ∈ U → ∀ (i : ι), dist (F i x) (F i x') < ε
U : Set (α × α)
hU : U ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hεU : ∀ {a b : α}, dist a b < ε → (a, b) ∈ U
⊢ ∃ V, V ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ V → ∀ (y : β), y ∈ V → ∀ (i : ι), (F i x, F i y) ∈ U
[PROOFSTEP]
refine' Exists.imp (fun V => And.imp_right fun h => _) (H _ hε)
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
ι✝ : Type u_3
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : TopologicalSpace β
F : ι → β → α
x₀ : β
H : ∀ (ε : ℝ), ε > 0 → ∃ U, U ∈ 𝓝 x₀ ∧ ∀ (x : β), x ∈ U → ∀ (x' : β), x' ∈ U → ∀ (i : ι), dist (F i x) (F i x') < ε
U : Set (α × α)
hU : U ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hεU : ∀ {a b : α}, dist a b < ε → (a, b) ∈ U
V : Set β
h : ∀ (x : β), x ∈ V → ∀ (x' : β), x' ∈ V → ∀ (i : ι), dist (F i x) (F i x') < ε
⊢ ∀ (x : β), x ∈ V → ∀ (y : β), y ∈ V → ∀ (i : ι), (F i x, F i y) ∈ U
[PROOFSTEP]
exact fun x hx x' hx' i => hεU (h _ hx _ hx' i)
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : TopologicalSpace β
x₀ : β
b : β → ℝ
b_lim : Tendsto b (𝓝 x₀) (𝓝 0)
F : ι → β → α
H : ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) ≤ b x
⊢ EquicontinuousAt F x₀
[PROOFSTEP]
rw [Metric.equicontinuousAt_iff_right]
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : TopologicalSpace β
x₀ : β
b : β → ℝ
b_lim : Tendsto b (𝓝 x₀) (𝓝 0)
F : ι → β → α
H : ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) ≤ b x
⊢ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) < ε
[PROOFSTEP]
intro ε ε0
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : TopologicalSpace β
x₀ : β
b : β → ℝ
b_lim : Tendsto b (𝓝 x₀) (𝓝 0)
F : ι → β → α
H : ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) ≤ b x
ε : ℝ
ε0 : ε > 0
⊢ ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) < ε
[PROOFSTEP]
filter_upwards [Filter.mem_map.mp <| b_lim (Iio_mem_nhds ε0), H] using fun x hx₁ hx₂ i => (hx₂ i).trans_lt hx₁
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
⊢ UniformEquicontinuous F
[PROOFSTEP]
rw [Metric.uniformEquicontinuous_iff]
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
⊢ ∀ (ε : ℝ), ε > 0 → ∃ δ, δ > 0 ∧ ∀ (x y : β), dist x y < δ → ∀ (i : ι), dist (F i x) (F i y) < ε
[PROOFSTEP]
intro ε ε0
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
ε : ℝ
ε0 : ε > 0
⊢ ∃ δ, δ > 0 ∧ ∀ (x y : β), dist x y < δ → ∀ (i : ι), dist (F i x) (F i y) < ε
[PROOFSTEP]
rcases tendsto_nhds_nhds.1 b_lim ε ε0 with ⟨δ, δ0, hδ⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
ι✝ : Type u_3
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδ : ∀ {x : ℝ}, dist x 0 < δ → dist (b x) 0 < ε
⊢ ∃ δ, δ > 0 ∧ ∀ (x y : β), dist x y < δ → ∀ (i : ι), dist (F i x) (F i y) < ε
[PROOFSTEP]
refine' ⟨δ, δ0, fun x y hxy i => _⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
ι✝ : Type u_3
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδ : ∀ {x : ℝ}, dist x 0 < δ → dist (b x) 0 < ε
x y : β
hxy : dist x y < δ
i : ι
⊢ dist (F i x) (F i y) < ε
[PROOFSTEP]
calc
  dist (F i x) (F i y) ≤ b (dist x y) := H x y i
  _ ≤ |b (dist x y)| := (le_abs_self _)
  _ = dist (b (dist x y)) 0 := by simp [Real.dist_eq]
  _ < ε := hδ (by simpa only [Real.dist_eq, tsub_zero, abs_dist] using hxy)
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδ : ∀ {x : ℝ}, dist x 0 < δ → dist (b x) 0 < ε
x y : β
hxy : dist x y < δ
i : ι
⊢ |b (dist x y)| = dist (b (dist x y)) 0
[PROOFSTEP]
simp [Real.dist_eq]
[GOAL]
α : Type u_1
β : Type u_2
ι✝ : Type u_3
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδ : ∀ {x : ℝ}, dist x 0 < δ → dist (b x) 0 < ε
x y : β
hxy : dist x y < δ
i : ι
⊢ dist (dist x y) 0 < δ
[PROOFSTEP]
simpa only [Real.dist_eq, tsub_zero, abs_dist] using hxy