internlm/Lean-Github huggingface dataset:
Theorem: LipschitzOnWith.sum
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
Kf Kg : ℝ≥0
s : Set X
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
⊢ LipschitzOnWith (Kf + Kg) (f + g) s
Tactic:
intro y hy z hz
Proof state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
Kf Kg : ℝ≥0
s : Set X
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
y : X
hy : y ∈ s
z : X
hz : z ∈ s
⊢ edist ((f + g) y) ((f + g) z) ≤ ↑(Kf + Kg) * edist y z
Theorem: LipschitzOnWith.sum
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
Kf Kg : ℝ≥0
s : Set X
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
y : X
hy : y ∈ s
z : X
hz : z ∈ s
⊢ edist ((f + g) y) ((f + g) z) ≤ ↑(Kf + Kg) * edist y z
Tactic:
have translation: ∀ w w' w'' : Y, edist (w + w'') (w' + w'') = edist w w' := by
  intro w w' w''
  simp only [edist_add_right]
Proof state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
Kf Kg : ℝ≥0
s : Set X
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
y : X
hy : y ∈ s
z : X
hz : z ∈ s
translation : ∀ (w w' w'' : Y), edist (w + w'') (w' + w'') = edist w w'
⊢ edist ((f + g) y) ((f + g) z) ≤ ↑(Kf + Kg) * edist y z
Theorem: LipschitzOnWith.sum
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
Kf Kg : ℝ≥0
s : Set X
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
y : X
hy : y ∈ s
z : X
hz : z ∈ s
translation : ∀ (w w' w'' : Y), edist (w + w'') (w' + w'') = edist w w'
⊢ edist ((f + g) y) ((f + g) z) ≤ ↑(Kf + Kg) * edist y z
Tactic:
simp only [Pi.add_apply, ENNReal.coe_add]
Proof state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
Kf Kg : ℝ≥0
s : Set X
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
y : X
hy : y ∈ s
z : X
hz : z ∈ s
translation : ∀ (w w' w'' : Y), edist (w + w'') (w' + w'') = edist w w'
⊢ edist (f y + g y) (f z + g z) ≤ (↑Kf + ↑Kg) * edist y z
Theorem: LipschitzOnWith.sum
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
Kf Kg : ℝ≥0
s : Set X
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
y : X
hy : y ∈ s
z : X
hz : z ∈ s
translation : ∀ (w w' w'' : Y), edist (w + w'') (w' + w'') = edist w w'
⊢ edist (f y + g y) (f z + g z) ≤ (↑Kf + ↑Kg) * edist y z
Tactic:
calc edist (f y + g y) (f z + g z)
  _ ≤ edist (f y + g y) (g y + f z) + edist (g y + f z) (f z + g z) := by apply edist_triangle
  _ = edist (f y + g y) (f z + g y) + edist (g y + f z) (g z + f z) := by
      simp only [add_comm, edist_add_right, edist_add_left]
  _ ≤ edist (f y) (f z) + edist (g y) (g z) := by rw [translation, translation]
  _ ≤ Kf * edist y z + Kg * edist y z := add_le_add (hf hy hz) (hg hy hz)
  _ = (Kf + Kg) * edist y z := by ring
Proof state after:
no goals
Theorem: LipschitzOnWith.sum
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
Kf Kg : ℝ≥0
s : Set X
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
y : X
hy : y ∈ s
z : X
hz : z ∈ s
⊢ ∀ (w w' w'' : Y), edist (w + w'') (w' + w'') = edist w w'
Tactic:
intro w w' w''
Proof state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
Kf Kg : ℝ≥0
s : Set X
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
y : X
hy : y ∈ s
z : X
hz : z ∈ s
w w' w'' : Y
⊢ edist (w + w'') (w' + w'') = edist w w'
Theorem: LipschitzOnWith.sum
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
Kf Kg : ℝ≥0
s : Set X
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
y : X
hy : y ∈ s
z : X
hz : z ∈ s
w w' w'' : Y
⊢ edist (w + w'') (w' + w'') = edist w w'
Tactic:
simp only [edist_add_right]
Proof state after:
no goals
Theorem: LipschitzOnWith.sum
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
Kf Kg : ℝ≥0
s : Set X
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
y : X
hy : y ∈ s
z : X
hz : z ∈ s
translation : ∀ (w w' w'' : Y), edist (w + w'') (w' + w'') = edist w w'
⊢ edist (f y + g y) (f z + g z) ≤ edist (f y + g y) (g y + f z) + edist (g y + f z) (f z + g z)
Tactic:
apply edist_triangle
Proof state after:
no goals
Theorem: LipschitzOnWith.sum
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
Kf Kg : ℝ≥0
s : Set X
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
y : X
hy : y ∈ s
z : X
hz : z ∈ s
translation : ∀ (w w' w'' : Y), edist (w + w'') (w' + w'') = edist w w'
⊢ edist (f y + g y) (g y + f z) + edist (g y + f z) (f z + g z) =
    edist (f y + g y) (f z + g y) + edist (g y + f z) (g z + f z)
Tactic:
simp only [add_comm, edist_add_right, edist_add_left]
Proof state after:
no goals
Theorem: LipschitzOnWith.sum
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
Kf Kg : ℝ≥0
s : Set X
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
y : X
hy : y ∈ s
z : X
hz : z ∈ s
translation : ∀ (w w' w'' : Y), edist (w + w'') (w' + w'') = edist w w'
⊢ edist (f y + g y) (f z + g y) + edist (g y + f z) (g z + f z) ≤ edist (f y) (f z) + edist (g y) (g z)
Tactic:
rw [translation, translation]
Proof state after:
no goals
Theorem: LipschitzOnWith.sum
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
Kf Kg : ℝ≥0
s : Set X
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
y : X
hy : y ∈ s
z : X
hz : z ∈ s
translation : ∀ (w w' w'' : Y), edist (w + w'') (w' + w'') = edist w w'
⊢ ↑Kf * edist y z + ↑Kg * edist y z = (↑Kf + ↑Kg) * edist y z
Tactic:
ring
Proof state after:
no goals
Theorem: LocallyLipschitz.sum
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
hf : LocallyLipschitz f
hg : LocallyLipschitz g
⊢ LocallyLipschitz (f + g)
Tactic:
intro x
Proof state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : X
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (f + g) t
Theorem: LocallyLipschitz.sum
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : X
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (f + g) t
Tactic:
rcases hf x with ⟨Kf, t₁, h₁t, hfL⟩
Proof state after:
case intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : X
Kf : ℝ≥0
t₁ : Set X
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (f + g) t
Theorem: LocallyLipschitz.sum
Proof state before:
case intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : X
Kf : ℝ≥0
t₁ : Set X
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (f + g) t
Tactic:
rcases hg x with ⟨Kg, t₂, h₂t, hgL⟩
Proof state after:
case intro.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : X
Kf : ℝ≥0
t₁ : Set X
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
Kg : ℝ≥0
t₂ : Set X
h₂t : t₂ ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t₂
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (f + g) t
Theorem: LocallyLipschitz.sum
Proof state before:
case intro.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : X
Kf : ℝ≥0
t₁ : Set X
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
Kg : ℝ≥0
t₂ : Set X
h₂t : t₂ ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t₂
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (f + g) t
Tactic:
use Kf + Kg, t₁ ∩ t₂
Proof state after:
case h
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : X
Kf : ℝ≥0
t₁ : Set X
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
Kg : ℝ≥0
t₂ : Set X
h₂t : t₂ ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t₂
⊢ t₁ ∩ t₂ ∈ 𝓝 x ∧ LipschitzOnWith (Kf + Kg) (f + g) (t₁ ∩ t₂)
Theorem: LocallyLipschitz.sum
Proof state before:
case h
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : X
Kf : ℝ≥0
t₁ : Set X
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
Kg : ℝ≥0
t₂ : Set X
h₂t : t₂ ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t₂
⊢ t₁ ∩ t₂ ∈ 𝓝 x ∧ LipschitzOnWith (Kf + Kg) (f + g) (t₁ ∩ t₂)
Tactic:
have hf' : LipschitzOnWith Kf f (t₁ ∩ t₂) := hfL.mono (Set.inter_subset_left t₁ t₂)
Proof state after:
case h
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : X
Kf : ℝ≥0
t₁ : Set X
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
Kg : ℝ≥0
t₂ : Set X
h₂t : t₂ ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t₂
hf' : LipschitzOnWith Kf f (t₁ ∩ t₂)
⊢ t₁ ∩ t₂ ∈ 𝓝 x ∧ LipschitzOnWith (Kf + Kg) (f + g) (t₁ ∩ t₂)
Theorem: LocallyLipschitz.sum
Proof state before:
case h
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : X
Kf : ℝ≥0
t₁ : Set X
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
Kg : ℝ≥0
t₂ : Set X
h₂t : t₂ ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t₂
hf' : LipschitzOnWith Kf f (t₁ ∩ t₂)
⊢ t₁ ∩ t₂ ∈ 𝓝 x ∧ LipschitzOnWith (Kf + Kg) (f + g) (t₁ ∩ t₂)
Tactic:
have hg' : LipschitzOnWith Kg g (t₁ ∩ t₂) := hgL.mono (Set.inter_subset_right t₁ t₂)
Proof state after:
case h
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : X
Kf : ℝ≥0
t₁ : Set X
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
Kg : ℝ≥0
t₂ : Set X
h₂t : t₂ ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t₂
hf' : LipschitzOnWith Kf f (t₁ ∩ t₂)
hg' : LipschitzOnWith Kg g (t₁ ∩ t₂)
⊢ t₁ ∩ t₂ ∈ 𝓝 x ∧ LipschitzOnWith (Kf + Kg) (f + g) (t₁ ∩ t₂)
Theorem: LocallyLipschitz.sum
Proof state before:
case h
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : X
Kf : ℝ≥0
t₁ : Set X
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
Kg : ℝ≥0
t₂ : Set X
h₂t : t₂ ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t₂
hf' : LipschitzOnWith Kf f (t₁ ∩ t₂)
hg' : LipschitzOnWith Kg g (t₁ ∩ t₂)
⊢ t₁ ∩ t₂ ∈ 𝓝 x ∧ LipschitzOnWith (Kf + Kg) (f + g) (t₁ ∩ t₂)
Tactic:
exact ⟨Filter.inter_mem h₁t h₂t, hf'.sum hg'⟩
Proof state after:
no goals
Theorem: helper
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
a b : ℝ
⊢ ENNReal.ofReal (a * b) = ENNReal.ofReal a * ENNReal.ofReal b
Tactic:
sorry
Proof state after:
no goals
Theorem: last'
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
a K c : ℝ≥0
⊢ a * K * c = a * (K * c)
Tactic:
exact mul_assoc a K c
Proof state after:
no goals
Theorem: last''
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
a : ℝ
K c : ℝ≥0
⊢ ‖a‖.toNNReal * K * c = ‖a‖.toNNReal * (K * c)
Tactic:
exact mul_assoc _ K c
Proof state after:
no goals
Theorem: last
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
a : ℝ
K : ℝ≥0
c : ℝ≥0∞
⊢ ↑‖a‖.toNNReal * (↑K * c) = ↑(‖a‖.toNNReal * K) * c
Tactic:
have : c ≠ ∞ := by sorry
Proof state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
a : ℝ
K : ℝ≥0
c : ℝ≥0∞
this : c ≠ ⊤
⊢ ↑‖a‖.toNNReal * (↑K * c) = ↑(‖a‖.toNNReal * K) * c
Theorem: last
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
a : ℝ
K : ℝ≥0
c : ℝ≥0∞
this : c ≠ ⊤
⊢ ↑‖a‖.toNNReal * (↑K * c) = ↑(‖a‖.toNNReal * K) * c
Tactic:
lift c to ℝ≥0 using this
Proof state after:
case intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
a : ℝ
K c : ℝ≥0
⊢ ↑‖a‖.toNNReal * (↑K * ↑c) = ↑(‖a‖.toNNReal * K) * ↑c
Theorem: last
Proof state before:
case intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
a : ℝ
K c : ℝ≥0
⊢ ↑‖a‖.toNNReal * (↑K * ↑c) = ↑(‖a‖.toNNReal * K) * ↑c
Tactic:
sorry
Proof state after:
no goals
Theorem: last
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
a : ℝ
K : ℝ≥0
c : ℝ≥0∞
⊢ c ≠ ⊤
Tactic:
sorry
Proof state after:
no goals
Theorem: LipschitzOnWith.smul
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
K : ℝ≥0
s : Set X
hf : LipschitzOnWith K f s
a : ℝ
⊢ LipschitzOnWith ((ENNReal.ofReal ‖a‖).toNNReal * K) (fun x => a • f x) s
Tactic:
intro x hx y hy
Proof state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
K : ℝ≥0
s : Set X
hf : LipschitzOnWith K f s
a : ℝ
x : X
hx : x ∈ s
y : X
hy : y ∈ s
⊢ edist ((fun x => a • f x) x) ((fun x => a • f x) y) ≤ ↑((ENNReal.ofReal ‖a‖).toNNReal * K) * edist x y
Theorem: LipschitzOnWith.smul
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
K : ℝ≥0
s : Set X
hf : LipschitzOnWith K f s
a : ℝ
x : X
hx : x ∈ s
y : X
hy : y ∈ s
⊢ edist ((fun x => a • f x) x) ((fun x => a • f x) y) ≤ ↑((ENNReal.ofReal ‖a‖).toNNReal * K) * edist x y
Tactic:
have : dist (a • f x) (a • f y) = ‖a‖ * dist (f x) (f y) := by
    calc dist (a • f x) (a • f y)
      _ = ‖(a • (f x)) - (a • (f y))‖ := by apply dist_eq_norm
      _ = ‖a • ((f x) - (f y))‖ := by rw [smul_sub]
      _ = ‖a‖ * ‖(f x) - (f y)‖ := by rw [norm_smul]
      _ = ‖a‖ * dist (f x) (f y) := by rw [← dist_eq_norm]
      _ = ‖a‖ * dist (f x) (f y) := by rw [← dist_smul₀]
Proof state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
K : ℝ≥0
s : Set X
hf : LipschitzOnWith K f s
a : ℝ
x : X
hx : x ∈ s
y : X
hy : y ∈ s
this : dist (a • f x) (a • f y) = ‖a‖ * dist (f x) (f y)
⊢ edist ((fun x => a • f x) x) ((fun x => a • f x) y) ≤ ↑((ENNReal.ofReal ‖a‖).toNNReal * K) * edist x y
Theorem: LipschitzOnWith.smul
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
K : ℝ≥0
s : Set X
hf : LipschitzOnWith K f s
a : ℝ
x : X
hx : x ∈ s
y : X
hy : y ∈ s
this : dist (a • f x) (a • f y) = ‖a‖ * dist (f x) (f y)
⊢ edist ((fun x => a • f x) x) ((fun x => a • f x) y) ≤ ↑((ENNReal.ofReal ‖a‖).toNNReal * K) * edist x y
Tactic:
calc edist (a • f x) (a • f y)
    _ = ENNReal.ofReal (dist (a • f x) (a • f y)) := by rw [edist_dist]
    _ = ENNReal.ofReal (‖a‖ * dist (f x) (f y)) := by rw [this]
    _ = ENNReal.ofReal (‖a‖) * ENNReal.ofReal (dist (f x) (f y)) := by rw [← helper]
    _ = ENNReal.ofReal ‖a‖ * edist (f x) (f y) := by rw [edist_dist]
    _ ≤ Real.toNNReal ‖a‖ * (K * edist x y) := by exact mul_le_mul_left' (hf hx hy) _
    _ = ↑(Real.toNNReal ‖a‖ * K) * edist x y := by exact last a K (edist x y)
Proof state after:
no goals
Theorem: LipschitzOnWith.smul
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
K : ℝ≥0
s : Set X
hf : LipschitzOnWith K f s
a : ℝ
x : X
hx : x ∈ s
y : X
hy : y ∈ s
⊢ dist (a • f x) (a • f y) = ‖a‖ * dist (f x) (f y)
Tactic:
calc dist (a • f x) (a • f y)
  _ = ‖(a • (f x)) - (a • (f y))‖ := by apply dist_eq_norm
  _ = ‖a • ((f x) - (f y))‖ := by rw [smul_sub]
  _ = ‖a‖ * ‖(f x) - (f y)‖ := by rw [norm_smul]
  _ = ‖a‖ * dist (f x) (f y) := by rw [← dist_eq_norm]
  _ = ‖a‖ * dist (f x) (f y) := by rw [← dist_smul₀]
Proof state after:
no goals
Theorem: LipschitzOnWith.smul
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
K : ℝ≥0
s : Set X
hf : LipschitzOnWith K f s
a : ℝ
x : X
hx : x ∈ s
y : X
hy : y ∈ s
⊢ dist (a • f x) (a • f y) = ‖a • f x - a • f y‖
Tactic:
apply dist_eq_norm
Proof state after:
no goals
Theorem: LipschitzOnWith.smul
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
K : ℝ≥0
s : Set X
hf : LipschitzOnWith K f s
a : ℝ
x : X
hx : x ∈ s
y : X
hy : y ∈ s
⊢ ‖a • f x - a • f y‖ = ‖a • (f x - f y)‖
Tactic:
rw [smul_sub]
Proof state after:
no goals
Theorem: LipschitzOnWith.smul
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
K : ℝ≥0
s : Set X
hf : LipschitzOnWith K f s
a : ℝ
x : X
hx : x ∈ s
y : X
hy : y ∈ s
⊢ ‖a • (f x - f y)‖ = ‖a‖ * ‖f x - f y‖
Tactic:
rw [norm_smul]
Proof state after:
no goals
Theorem: LipschitzOnWith.smul
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
K : ℝ≥0
s : Set X
hf : LipschitzOnWith K f s
a : ℝ
x : X
hx : x ∈ s
y : X
hy : y ∈ s
⊢ ‖a‖ * ‖f x - f y‖ = ‖a‖ * dist (f x) (f y)
Tactic:
rw [← dist_eq_norm]
Proof state after:
no goals
Theorem: LipschitzOnWith.smul
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
K : ℝ≥0
s : Set X
hf : LipschitzOnWith K f s
a : ℝ
x : X
hx : x ∈ s
y : X
hy : y ∈ s
⊢ ‖a‖ * dist (f x) (f y) = ‖a‖ * dist (f x) (f y)
Tactic:
rw [← dist_smul₀]
Proof state after:
no goals
Theorem: LipschitzOnWith.smul
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
K : ℝ≥0
s : Set X
hf : LipschitzOnWith K f s
a : ℝ
x : X
hx : x ∈ s
y : X
hy : y ∈ s
this : dist (a • f x) (a • f y) = ‖a‖ * dist (f x) (f y)
⊢ edist (a • f x) (a • f y) = ENNReal.ofReal (dist (a • f x) (a • f y))
Tactic:
rw [edist_dist]
Proof state after:
no goals
Theorem: LipschitzOnWith.smul
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
K : ℝ≥0
s : Set X
hf : LipschitzOnWith K f s
a : ℝ
x : X
hx : x ∈ s
y : X
hy : y ∈ s
this : dist (a • f x) (a • f y) = ‖a‖ * dist (f x) (f y)
⊢ ENNReal.ofReal (dist (a • f x) (a • f y)) = ENNReal.ofReal (‖a‖ * dist (f x) (f y))
Tactic:
rw [this]
Proof state after:
no goals
Theorem: LipschitzOnWith.smul
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
K : ℝ≥0
s : Set X
hf : LipschitzOnWith K f s
a : ℝ
x : X
hx : x ∈ s
y : X
hy : y ∈ s
this : dist (a • f x) (a • f y) = ‖a‖ * dist (f x) (f y)
⊢ ENNReal.ofReal (‖a‖ * dist (f x) (f y)) = ENNReal.ofReal ‖a‖ * ENNReal.ofReal (dist (f x) (f y))
Tactic:
rw [← helper]
Proof state after:
no goals
Theorem: LipschitzOnWith.smul
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
K : ℝ≥0
s : Set X
hf : LipschitzOnWith K f s
a : ℝ
x : X
hx : x ∈ s
y : X
hy : y ∈ s
this : dist (a • f x) (a • f y) = ‖a‖ * dist (f x) (f y)
⊢ ENNReal.ofReal ‖a‖ * ENNReal.ofReal (dist (f x) (f y)) = ENNReal.ofReal ‖a‖ * edist (f x) (f y)
Tactic:
rw [edist_dist]
Proof state after:
no goals
Theorem: LipschitzOnWith.smul
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
K : ℝ≥0
s : Set X
hf : LipschitzOnWith K f s
a : ℝ
x : X
hx : x ∈ s
y : X
hy : y ∈ s
this : dist (a • f x) (a • f y) = ‖a‖ * dist (f x) (f y)
⊢ ENNReal.ofReal ‖a‖ * edist (f x) (f y) ≤ ↑‖a‖.toNNReal * (↑K * edist x y)
Tactic:
exact mul_le_mul_left' (hf hx hy) _
Proof state after:
no goals
Theorem: LipschitzOnWith.smul
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
K : ℝ≥0
s : Set X
hf : LipschitzOnWith K f s
a : ℝ
x : X
hx : x ∈ s
y : X
hy : y ∈ s
this : dist (a • f x) (a • f y) = ‖a‖ * dist (f x) (f y)
⊢ ↑‖a‖.toNNReal * (↑K * edist x y) = ↑(‖a‖.toNNReal * K) * edist x y
Tactic:
exact last a K (edist x y)
Proof state after:
no goals
Theorem: LocallyLipschitz.mysmul
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
hf : LocallyLipschitz f
a : ℝ
⊢ LocallyLipschitz fun x => a • f x
Tactic:
intro x
Proof state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
hf : LocallyLipschitz f
a : ℝ
x : X
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (fun x => a • f x) t
Theorem: LocallyLipschitz.mysmul
Proof state before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
hf : LocallyLipschitz f
a : ℝ
x : X
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (fun x => a • f x) t
Tactic:
rcases hf x with ⟨Kf, t, ht, hfL⟩
Proof state after:
case intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
hf : LocallyLipschitz f
a : ℝ
x : X
Kf : ℝ≥0
t : Set X
ht : t ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (fun x => a • f x) t
Theorem: LocallyLipschitz.mysmul
Proof state before:
case intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : NormedAddCommGroup Y
inst✝ : NormedSpace ℝ Y
f g : X → Y
hf : LocallyLipschitz f
a : ℝ
x : X
Kf : ℝ≥0
t : Set X
ht : t ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K (fun x => a • f x) t
Tactic:
exact ⟨ENNReal.toNNReal (ENNReal.ofReal ‖a‖) * Kf, t, ht, hfL.smul a⟩
Proof state after:
no goals