internlm/Lean-Github huggingface dataset:
Theorem: volume_ball_le_same
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
hn : ∀ (n : ℕ), volume.real (ball x (2 ^ n * r)) ≤ A ^ n * volume.real (ball x r)
haux : s * r ≤ 2 ^ ⌈s.log / Real.log 2⌉₊ * r
⊢ ball x r' ⊆ ball x (s * r)
Tactic:
apply ball_subset_ball hs
Proof state after:
no goals
Theorem: volume_ball_le_same
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
hn : ∀ (n : ℕ), volume.real (ball x (2 ^ n * r)) ≤ A ^ n * volume.real (ball x r)
haux : s * r ≤ 2 ^ ⌈s.log / Real.log 2⌉₊ * r
⊢ ball x (s * r) ⊆ ball x (2 ^ ⌈s.log / Real.log 2⌉₊ * r)
Tactic:
apply ball_subset_ball haux
Proof state after:
no goals
Theorem: volume_ball_le_same
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
hn : ∀ (n : ℕ), volume.real (ball x (2 ^ n * r)) ≤ A ^ n * volume.real (ball x r)
haux : s * r ≤ 2 ^ ⌈s.log / Real.log 2⌉₊ * r
h1 : ball x r' ⊆ ball x (2 ^ ⌈s.log / Real.log 2⌉₊ * r)
⊢ volume.real (ball x r') ≤ volume.real (ball x (2 ^ ⌈s.log / Real.log 2⌉₊ * r))
Tactic:
gcongr
Proof state after:
case h₂
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
hn : ∀ (n : ℕ), volume.real (ball x (2 ^ n * r)) ≤ A ^ n * volume.real (ball x r)
haux : s * r ≤ 2 ^ ⌈s.log / Real.log 2⌉₊ * r
h1 : ball x r' ⊆ ball x (2 ^ ⌈s.log / Real.log 2⌉₊ * r)
⊢ autoParam (volume (ball x (2 ^ ⌈s.log / Real.log 2⌉₊ * r)) ≠ ⊤) _auto✝
Theorem: volume_ball_le_same
Proof state before:
case h₂
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
hn : ∀ (n : ℕ), volume.real (ball x (2 ^ n * r)) ≤ A ^ n * volume.real (ball x r)
haux : s * r ≤ 2 ^ ⌈s.log / Real.log 2⌉₊ * r
h1 : ball x r' ⊆ ball x (2 ^ ⌈s.log / Real.log 2⌉₊ * r)
⊢ autoParam (volume (ball x (2 ^ ⌈s.log / Real.log 2⌉₊ * r)) ≠ ⊤) _auto✝
Tactic:
finiteness
Proof state after:
no goals
Theorem: volume_ball_le_same
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r s r' : ℝ
hsp : s > 0
hs : r' ≤ s * r
hn : ∀ (n : ℕ), volume.real (ball x (2 ^ n * r)) ≤ A ^ n * volume.real (ball x r)
haux : s * r ≤ 2 ^ ⌈s.log / Real.log 2⌉₊ * r
h1 : ball x r' ⊆ ball x (2 ^ ⌈s.log / Real.log 2⌉₊ * r)
⊢ volume.real (ball x (2 ^ ⌈s.log / Real.log 2⌉₊ * r)) ≤ A ^ ⌈s.log / Real.log 2⌉₊ * volume.real (ball x r)
Tactic:
apply hn
Proof state after:
no goals
Theorem: ball_subset_ball_of_le
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x x' : X
r r' : ℝ
hr : dist x x' + r' ≤ r
⊢ ball x' r' ⊆ ball x r
Tactic:
intro y h
Proof state after:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x x' : X
r r' : ℝ
hr : dist x x' + r' ≤ r
y : X
h : y ∈ ball x' r'
⊢ y ∈ ball x r
Theorem: ball_subset_ball_of_le
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x x' : X
r r' : ℝ
hr : dist x x' + r' ≤ r
y : X
h : y ∈ ball x' r'
⊢ y ∈ ball x r
Tactic:
have h1 : dist x y < r := by
  calc dist x y ≤ dist x x' + dist x' y := by apply dist_triangle
      _ < dist x x' + r' := by gcongr; apply mem_ball'.mp h
      _ ≤ r := by apply hr
Proof state after:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x x' : X
r r' : ℝ
hr : dist x x' + r' ≤ r
y : X
h : y ∈ ball x' r'
h1 : dist x y < r
⊢ y ∈ ball x r
Theorem: ball_subset_ball_of_le
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x x' : X
r r' : ℝ
hr : dist x x' + r' ≤ r
y : X
h : y ∈ ball x' r'
h1 : dist x y < r
⊢ y ∈ ball x r
Tactic:
exact mem_ball'.mpr h1
Proof state after:
no goals
Theorem: ball_subset_ball_of_le
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x x' : X
r r' : ℝ
hr : dist x x' + r' ≤ r
y : X
h : y ∈ ball x' r'
⊢ dist x y < r
Tactic:
calc dist x y ≤ dist x x' + dist x' y := by apply dist_triangle
    _ < dist x x' + r' := by gcongr; apply mem_ball'.mp h
    _ ≤ r := by apply hr
Proof state after:
no goals
Theorem: ball_subset_ball_of_le
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x x' : X
r r' : ℝ
hr : dist x x' + r' ≤ r
y : X
h : y ∈ ball x' r'
⊢ dist x y ≤ dist x x' + dist x' y
Tactic:
apply dist_triangle
Proof state after:
no goals
Theorem: ball_subset_ball_of_le
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x x' : X
r r' : ℝ
hr : dist x x' + r' ≤ r
y : X
h : y ∈ ball x' r'
⊢ dist x x' + dist x' y < dist x x' + r'
Tactic:
gcongr
Proof state after:
case bc
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x x' : X
r r' : ℝ
hr : dist x x' + r' ≤ r
y : X
h : y ∈ ball x' r'
⊢ dist x' y < r'
Theorem: ball_subset_ball_of_le
Proof state before:
case bc
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x x' : X
r r' : ℝ
hr : dist x x' + r' ≤ r
y : X
h : y ∈ ball x' r'
⊢ dist x' y < r'
Tactic:
apply mem_ball'.mp h
Proof state after:
no goals
Theorem: ball_subset_ball_of_le
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x x' : X
r r' : ℝ
hr : dist x x' + r' ≤ r
y : X
h : y ∈ ball x' r'
⊢ dist x x' + r' ≤ r
Tactic:
apply hr
Proof state after:
no goals
Theorem: volume_ball_le_of_dist_le
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x x' : X
r r' s d : ℝ
hs : r' ≤ s * r
hd : dist x x' ≤ d * r
⊢ volume.real (ball x' r') ≤ Ad A s d * volume.real (ball x r)
Tactic:
sorry
Proof state after:
no goals
Theorem: volume_ball_le_of_subset
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x' x : X
r r' s : ℝ
hs : r' ≤ s * r
hr : ball x' r ⊆ ball x r'
⊢ volume.real (ball x (2 * r)) ≤ Ai A s * volume.real (ball x' r)
Tactic:
sorry
Proof state after:
no goals
Theorem: card_le_of_le_dist
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
x : X
r r' s : ℝ
P : Set X
hs : r' ≤ s * r
hP : P ⊆ ball x r'
h2P : ∀ (x y : X), x ∈ P → y ∈ P → x ≠ y → r ≤ dist x y
⊢ P.Finite ∧ Nat.card ↑P ≤ Np A s
Tactic:
sorry
Proof state after:
no goals
Theorem: ballsCoverBalls
Proof state before:
X : Type u_1
A : ℝ
hA : 1 ≤ A
inst✝¹ : PseudoMetricSpace X
inst✝ : IsSpaceOfHomogeneousType X A
r r' s : ℝ
hs : r' ≤ s * r
⊢ BallsCoverBalls X r' r (Np A s)
Tactic:
sorry
Proof state after:
no goals
Theorem: prop2_1
Proof state before:
X : Type u_1
A : ℝ
inst✝⁶ : MetricSpace X
inst✝⁵ : IsSpaceOfHomogeneousType X A
inst✝⁴ : Inhabited X
τ q q' D κ C₀ C : ℝ
Θ : Set C(X, ℂ)
inst✝³ : IsCompatible Θ
inst✝² : IsCancellative τ Θ
inst✝¹ : TileStructure Θ D κ C₀
F G : Set X
σ σ' : X → ℤ
Q' : X → C(X, ℂ)
K : X → X → ℂ
inst✝ : IsCZKernel τ K
ψ : ℝ → ℝ
hA : 1 < A
hτ : τ ∈ Ioo 0 1
hq : q ∈ Ioc 1 2
hqq' : q.IsConjExponent q'
hC₀ : 0 < C₀
hC : C2_1 A τ q C₀ < C
hD : D2_1 A τ q C₀ < D
hκ : κ ∈ Ioo 0 (κ2_1 A τ q C₀)
hF : MeasurableSet F
hG : MeasurableSet G
h2F : volume F ∈ Ioo 0 ⊤
h2G : volume G ∈ Ioo 0 ⊤
Q'_mem : ∀ (x : X), Q' x ∈ Θ
m_Q' : Measurable Q'
m_σ : Measurable σ
m_σ' : Measurable σ'
hT : NormBoundedBy (ANCZOperatorLp 2 K) 1
hψ : LipschitzWith (Cψ2_1 A τ q C₀) ψ
h2ψ : support ψ ⊆ Icc (4 * D)⁻¹ 2⁻¹
h3ψ : ∀ x > 0, ∑ᶠ (s : ℤ), ψ (D ^ s * x) = 1
⊢ ∃ G',
    volume G' ≤ volume G / 4 ∧
      ↑‖∫ (x : X) in G \ G', ∑' (p : 𝔓 X), T K Q' σ σ' ψ p F 1 x‖₊ ≤
        C * volume.real G ^ (1 / q') * volume.real F ^ (1 / q)
Tactic:
sorry
Proof state after:
no goals
Theorem: uniformContinuous_iff_bounded
Proof 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]
Proof 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) < ε
Theorem: uniformContinuous_iff_bounded
Proof 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
Proof 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) < ε
Theorem: uniformContinuous_iff_bounded
Proof 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)))
Proof 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) < ε
Theorem: uniformContinuous_iff_bounded
Proof 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 δ
Proof state after:
no goals
Theorem: uniformContinuous_iff_bounded
Proof 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
Proof 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) < ε
Theorem: uniformContinuous_iff_bounded
Proof 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
Proof 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) < ε
Theorem: uniformContinuous_iff_bounded
Proof 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)
Proof 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) < ε
Theorem: uniformContinuous_iff_bounded
Proof 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
Proof 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) < ε
Theorem: uniformContinuous_iff_bounded
Proof 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
Proof 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) < ε
Theorem: uniformContinuous_iff_bounded
Proof 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
Proof 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) < ε
Theorem: uniformContinuous_iff_bounded
Proof 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
Proof 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) < ε
Theorem: uniformContinuous_iff_bounded
Proof 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)))
Proof state after:
no goals
Theorem: uniformContinuous_iff_bounded
Proof 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
Proof state after:
no goals
Theorem: uniformContinuous_iff_bounded
Proof 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
Proof state after:
no goals
Theorem: uniformContinuous_iff_bounded
Proof 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
Proof 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
Theorem: uniformContinuous_iff_bounded
Proof 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
Proof state after:
no goals
Theorem: uniformContinuous_iff_bounded
Proof 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
Proof 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) < ε
Theorem: uniformContinuous_iff_bounded
Proof 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)))
Proof state after:
no goals
Theorem: uniformContinuous_iff_bounded
Proof 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
Proof 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) < ε
Theorem: uniformContinuous_iff_bounded
Proof 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
Proof 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) < ε
Theorem: uniformContinuous_iff_bounded
Proof 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 δ
Proof state after:
no goals
Theorem: closeSmoothApprox
Proof state before:
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
εpos : ε > 0
⊢ ∃ f₀, ContDiff ℝ ⊤ f₀ ∧ ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε
Tactic:
obtain ⟨δ, δpos, hδ⟩ := (Metric.uniformContinuous_iff.mp unicontf) ε εpos
Proof state after:
case intro.intro
f : ℝ → ℂ
unicontf : UniformContinuous f
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : δ > 0
hδ : ∀ {a b : ℝ}, dist a b < δ → dist (f a) (f b) < ε
⊢ ∃ f₀, ContDiff ℝ ⊤ f₀ ∧ ∀ (x : ℝ), Complex.abs (f x - f₀ x) ≤ ε