Theorem: LipschitzOnWith.smul (Sard/LocallyLipschitz.lean)

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
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

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₀]
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

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)
State after:
no goals

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₀]
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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]
State after:
no goals

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]
State after:
no goals

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₀]
State after:
no goals

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]
State after:
no goals

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]
State after:
no goals

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]
State after:
no goals

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]
State after:
no goals

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) _
State after:
no goals

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)
State after:
no goals