Theorem: uniformContinuous_iff_bounded (Carleson/Theorem1_1/Approximation.lean)

State before:
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
⊢ UniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, δ < b ∧ ∀ {x y : α}, dist x y < δ → dist (f x) (f y) < ε
Tactic:
rw [Metric.uniformContinuous_iff]
State after:
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
⊢ (∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε) ↔
    ∀ ε > 0, ∃ δ > 0, δ < b ∧ ∀ {x y : α}, dist x y < δ → dist (f x) (f y) < ε

State before:
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
⊢ (∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε) ↔
    ∀ ε > 0, ∃ δ > 0, δ < b ∧ ∀ {x y : α}, dist x y < δ → dist (f x) (f y) < ε
Tactic:
constructor
State after:
case mp
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
⊢ (∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε) →
    ∀ ε > 0, ∃ δ > 0, δ < b ∧ ∀ {x y : α}, dist x y < δ → dist (f x) (f y) < ε

case mpr
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
⊢ (∀ ε > 0, ∃ δ > 0, δ < b ∧ ∀ {x y : α}, dist x y < δ → dist (f x) (f y) < ε) →
    ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε

State before:
case mp
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
⊢ (∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε) →
    ∀ ε > 0, ∃ δ > 0, δ < b ∧ ∀ {x y : α}, dist x y < δ → dist (f x) (f y) < ε

case mpr
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
⊢ (∀ ε > 0, ∃ δ > 0, δ < b ∧ ∀ {x y : α}, dist x y < δ → dist (f x) (f y) < ε) →
    ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε
Tactic:
. intro h ε εpos
  obtain ⟨δ', δ'pos, hδ'⟩ := h ε εpos
  use min δ' (b / 2)
  constructor
  . exact (lt_min δ'pos (by linarith)).gt
  constructor
  . apply min_lt_of_right_lt
    linarith
  . intro x y hxy
    exact hδ' (lt_of_lt_of_le hxy (min_le_left δ' (b / 2)))
State after:
case mpr
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
⊢ (∀ ε > 0, ∃ δ > 0, δ < b ∧ ∀ {x y : α}, dist x y < δ → dist (f x) (f y) < ε) →
    ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε

State before:
case mpr
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
⊢ (∀ ε > 0, ∃ δ > 0, δ < b ∧ ∀ {x y : α}, dist x y < δ → dist (f x) (f y) < ε) →
    ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε
Tactic:
. intro h ε εpos
  obtain ⟨δ, δpos, _, hδ⟩ := h ε εpos
  use δ
State after:
no goals

State before:
case mp
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
⊢ (∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε) →
    ∀ ε > 0, ∃ δ > 0, δ < b ∧ ∀ {x y : α}, dist x y < δ → dist (f x) (f y) < ε
Tactic:
intro h ε εpos
State after:
case mp
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
h : ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε
ε : ℝ
εpos : ε > 0
⊢ ∃ δ > 0, δ < b ∧ ∀ {x y : α}, dist x y < δ → dist (f x) (f y) < ε

State before:
case mp
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
h : ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε
ε : ℝ
εpos : ε > 0
⊢ ∃ δ > 0, δ < b ∧ ∀ {x y : α}, dist x y < δ → dist (f x) (f y) < ε
Tactic:
obtain ⟨δ', δ'pos, hδ'⟩ := h ε εpos
State after:
case mp.intro.intro
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
h : ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε
ε : ℝ
εpos : ε > 0
δ' : ℝ
δ'pos : δ' > 0
hδ' : ∀ {a b : α}, dist a b < δ' → dist (f a) (f b) < ε
⊢ ∃ δ > 0, δ < b ∧ ∀ {x y : α}, dist x y < δ → dist (f x) (f y) < ε

State before:
case mp.intro.intro
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
h : ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε
ε : ℝ
εpos : ε > 0
δ' : ℝ
δ'pos : δ' > 0
hδ' : ∀ {a b : α}, dist a b < δ' → dist (f a) (f b) < ε
⊢ ∃ δ > 0, δ < b ∧ ∀ {x y : α}, dist x y < δ → dist (f x) (f y) < ε
Tactic:
use min δ' (b / 2)
State after:
case h
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
h : ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε
ε : ℝ
εpos : ε > 0
δ' : ℝ
δ'pos : δ' > 0
hδ' : ∀ {a b : α}, dist a b < δ' → dist (f a) (f b) < ε
⊢ min δ' (b / 2) > 0 ∧ min δ' (b / 2) < b ∧ ∀ {x y : α}, dist x y < min δ' (b / 2) → dist (f x) (f y) < ε

State before:
case h
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
h : ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε
ε : ℝ
εpos : ε > 0
δ' : ℝ
δ'pos : δ' > 0
hδ' : ∀ {a b : α}, dist a b < δ' → dist (f a) (f b) < ε
⊢ min δ' (b / 2) > 0 ∧ min δ' (b / 2) < b ∧ ∀ {x y : α}, dist x y < min δ' (b / 2) → dist (f x) (f y) < ε
Tactic:
constructor
State after:
case h.left
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
h : ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε
ε : ℝ
εpos : ε > 0
δ' : ℝ
δ'pos : δ' > 0
hδ' : ∀ {a b : α}, dist a b < δ' → dist (f a) (f b) < ε
⊢ min δ' (b / 2) > 0

case h.right
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
h : ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε
ε : ℝ
εpos : ε > 0
δ' : ℝ
δ'pos : δ' > 0
hδ' : ∀ {a b : α}, dist a b < δ' → dist (f a) (f b) < ε
⊢ min δ' (b / 2) < b ∧ ∀ {x y : α}, dist x y < min δ' (b / 2) → dist (f x) (f y) < ε

State before:
case h.left
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
h : ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε
ε : ℝ
εpos : ε > 0
δ' : ℝ
δ'pos : δ' > 0
hδ' : ∀ {a b : α}, dist a b < δ' → dist (f a) (f b) < ε
⊢ min δ' (b / 2) > 0

case h.right
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
h : ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε
ε : ℝ
εpos : ε > 0
δ' : ℝ
δ'pos : δ' > 0
hδ' : ∀ {a b : α}, dist a b < δ' → dist (f a) (f b) < ε
⊢ min δ' (b / 2) < b ∧ ∀ {x y : α}, dist x y < min δ' (b / 2) → dist (f x) (f y) < ε
Tactic:
. exact (lt_min δ'pos (by linarith)).gt
State after:
case h.right
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
h : ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε
ε : ℝ
εpos : ε > 0
δ' : ℝ
δ'pos : δ' > 0
hδ' : ∀ {a b : α}, dist a b < δ' → dist (f a) (f b) < ε
⊢ min δ' (b / 2) < b ∧ ∀ {x y : α}, dist x y < min δ' (b / 2) → dist (f x) (f y) < ε

State before:
case h.right
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
h : ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε
ε : ℝ
εpos : ε > 0
δ' : ℝ
δ'pos : δ' > 0
hδ' : ∀ {a b : α}, dist a b < δ' → dist (f a) (f b) < ε
⊢ min δ' (b / 2) < b ∧ ∀ {x y : α}, dist x y < min δ' (b / 2) → dist (f x) (f y) < ε
Tactic:
constructor
State after:
case h.right.left
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
h : ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε
ε : ℝ
εpos : ε > 0
δ' : ℝ
δ'pos : δ' > 0
hδ' : ∀ {a b : α}, dist a b < δ' → dist (f a) (f b) < ε
⊢ min δ' (b / 2) < b

case h.right.right
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
h : ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε
ε : ℝ
εpos : ε > 0
δ' : ℝ
δ'pos : δ' > 0
hδ' : ∀ {a b : α}, dist a b < δ' → dist (f a) (f b) < ε
⊢ ∀ {x y : α}, dist x y < min δ' (b / 2) → dist (f x) (f y) < ε

State before:
case h.right.left
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
h : ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε
ε : ℝ
εpos : ε > 0
δ' : ℝ
δ'pos : δ' > 0
hδ' : ∀ {a b : α}, dist a b < δ' → dist (f a) (f b) < ε
⊢ min δ' (b / 2) < b

case h.right.right
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
h : ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε
ε : ℝ
εpos : ε > 0
δ' : ℝ
δ'pos : δ' > 0
hδ' : ∀ {a b : α}, dist a b < δ' → dist (f a) (f b) < ε
⊢ ∀ {x y : α}, dist x y < min δ' (b / 2) → dist (f x) (f y) < ε
Tactic:
. apply min_lt_of_right_lt
  linarith
State after:
case h.right.right
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
h : ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε
ε : ℝ
εpos : ε > 0
δ' : ℝ
δ'pos : δ' > 0
hδ' : ∀ {a b : α}, dist a b < δ' → dist (f a) (f b) < ε
⊢ ∀ {x y : α}, dist x y < min δ' (b / 2) → dist (f x) (f y) < ε

State before:
case h.right.right
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
h : ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε
ε : ℝ
εpos : ε > 0
δ' : ℝ
δ'pos : δ' > 0
hδ' : ∀ {a b : α}, dist a b < δ' → dist (f a) (f b) < ε
⊢ ∀ {x y : α}, dist x y < min δ' (b / 2) → dist (f x) (f y) < ε
Tactic:
. intro x y hxy
  exact hδ' (lt_of_lt_of_le hxy (min_le_left δ' (b / 2)))
State after:
no goals

State before:
case h.left
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
h : ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε
ε : ℝ
εpos : ε > 0
δ' : ℝ
δ'pos : δ' > 0
hδ' : ∀ {a b : α}, dist a b < δ' → dist (f a) (f b) < ε
⊢ min δ' (b / 2) > 0
Tactic:
exact (lt_min δ'pos (by linarith)).gt
State after:
no goals

State before:
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
h : ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε
ε : ℝ
εpos : ε > 0
δ' : ℝ
δ'pos : δ' > 0
hδ' : ∀ {a b : α}, dist a b < δ' → dist (f a) (f b) < ε
⊢ 0 < b / 2
Tactic:
linarith
State after:
no goals

State before:
case h.right.left
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
h : ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε
ε : ℝ
εpos : ε > 0
δ' : ℝ
δ'pos : δ' > 0
hδ' : ∀ {a b : α}, dist a b < δ' → dist (f a) (f b) < ε
⊢ min δ' (b / 2) < b
Tactic:
apply min_lt_of_right_lt
State after:
case h.right.left.h
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
h : ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε
ε : ℝ
εpos : ε > 0
δ' : ℝ
δ'pos : δ' > 0
hδ' : ∀ {a b : α}, dist a b < δ' → dist (f a) (f b) < ε
⊢ b / 2 < b

State before:
case h.right.left.h
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
h : ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε
ε : ℝ
εpos : ε > 0
δ' : ℝ
δ'pos : δ' > 0
hδ' : ∀ {a b : α}, dist a b < δ' → dist (f a) (f b) < ε
⊢ b / 2 < b
Tactic:
linarith
State after:
no goals

State before:
case h.right.right
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
h : ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε
ε : ℝ
εpos : ε > 0
δ' : ℝ
δ'pos : δ' > 0
hδ' : ∀ {a b : α}, dist a b < δ' → dist (f a) (f b) < ε
⊢ ∀ {x y : α}, dist x y < min δ' (b / 2) → dist (f x) (f y) < ε
Tactic:
intro x y hxy
State after:
case h.right.right
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
h : ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε
ε : ℝ
εpos : ε > 0
δ' : ℝ
δ'pos : δ' > 0
hδ' : ∀ {a b : α}, dist a b < δ' → dist (f a) (f b) < ε
x y : α
hxy : dist x y < min δ' (b / 2)
⊢ dist (f x) (f y) < ε

State before:
case h.right.right
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
h : ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε
ε : ℝ
εpos : ε > 0
δ' : ℝ
δ'pos : δ' > 0
hδ' : ∀ {a b : α}, dist a b < δ' → dist (f a) (f b) < ε
x y : α
hxy : dist x y < min δ' (b / 2)
⊢ dist (f x) (f y) < ε
Tactic:
exact hδ' (lt_of_lt_of_le hxy (min_le_left δ' (b / 2)))
State after:
no goals

State before:
case mpr
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
⊢ (∀ ε > 0, ∃ δ > 0, δ < b ∧ ∀ {x y : α}, dist x y < δ → dist (f x) (f y) < ε) →
    ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε
Tactic:
intro h ε εpos
State after:
case mpr
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
h : ∀ ε > 0, ∃ δ > 0, δ < b ∧ ∀ {x y : α}, dist x y < δ → dist (f x) (f y) < ε
ε : ℝ
εpos : ε > 0
⊢ ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε

State before:
case mpr
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
h : ∀ ε > 0, ∃ δ > 0, δ < b ∧ ∀ {x y : α}, dist x y < δ → dist (f x) (f y) < ε
ε : ℝ
εpos : ε > 0
⊢ ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε
Tactic:
obtain ⟨δ, δpos, _, hδ⟩ := h ε εpos
State after:
case mpr.intro.intro.intro
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
h : ∀ ε > 0, ∃ δ > 0, δ < b ∧ ∀ {x y : α}, dist x y < δ → dist (f x) (f y) < ε
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
left✝ : δ < b
hδ : ∀ {x y : α}, dist x y < δ → dist (f x) (f y) < ε
⊢ ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε

State before:
case mpr.intro.intro.intro
α β : Type
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
b : ℝ
bpos : b > 0
h : ∀ ε > 0, ∃ δ > 0, δ < b ∧ ∀ {x y : α}, dist x y < δ → dist (f x) (f y) < ε
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
left✝ : δ < b
hδ : ∀ {x y : α}, dist x y < δ → dist (f x) (f y) < ε
⊢ ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε
Tactic:
use δ
State after:
no goals