[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
