𝓕 : Type ?u.1208856
𝕜 : Type ?u.1208859
α : Type u_1
ι : Type ?u.1208865
κ : Type ?u.1208868
E : Type u_2
F : Type ?u.1208874
G : Type ?u.1208877
inst✝² : SeminormedCommGroup E
inst✝¹ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
inst✝ : PseudoEMetricSpace α
K Kf Kg : ℝ≥0
f g : α → E
hf : AntilipschitzWith Kf f
hg : LipschitzWith Kg g
hK : Kg < Kf⁻¹
this : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace (_ : ∀ (x y : α), edist x y ≠ ⊤)
⊢ AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ fun x => f x * g x
𝓕 : Type ?u.1208856
𝕜 : Type ?u.1208859
α : Type u_1
ι : Type ?u.1208865
κ : Type ?u.1208868
E : Type u_2
F : Type ?u.1208874
G : Type ?u.1208877
inst✝² : SeminormedCommGroup E
inst✝¹ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
inst✝ : PseudoEMetricSpace α
K Kf Kg : ℝ≥0
f g : α → E
hf : AntilipschitzWith Kf f
hg : LipschitzWith Kg g
hK : Kg < Kf⁻¹
⊢ AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ fun x => f x * g x
letI : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace hf.edist_ne_top
𝓕 : Type ?u.1208856
𝕜 : Type ?u.1208859
α : Type u_1
ι : Type ?u.1208865
κ : Type ?u.1208868
E : Type u_2
F : Type ?u.1208874
G : Type ?u.1208877
inst✝² : SeminormedCommGroup E
inst✝¹ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
inst✝ : PseudoEMetricSpace α
K Kf Kg : ℝ≥0
f g : α → E
hf : AntilipschitzWith Kf f
hg : LipschitzWith Kg g
hK : Kg < Kf⁻¹
this : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace (_ : ∀ (x y : α), edist x y ≠ ⊤)
x y : α
⊢ dist x y ≤ ↑(Kf⁻¹ - Kg)⁻¹ * dist (f x * g x) (f y * g y)
𝓕 : Type ?u.1208856
𝕜 : Type ?u.1208859
α : Type u_1
ι : Type ?u.1208865
κ : Type ?u.1208868
E : Type u_2
F : Type ?u.1208874
G : Type ?u.1208877
inst✝² : SeminormedCommGroup E
inst✝¹ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
inst✝ : PseudoEMetricSpace α
K Kf Kg : ℝ≥0
f g : α → E
hf : AntilipschitzWith Kf f
hg : LipschitzWith Kg g
hK : Kg < Kf⁻¹
this : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace (_ : ∀ (x y : α), edist x y ≠ ⊤)
⊢ AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ fun x => f x * g x
refine' AntilipschitzWith.of_le_mul_dist fun x y => _
𝓕 : Type ?u.1208856
𝕜 : Type ?u.1208859
α : Type u_1
ι : Type ?u.1208865
κ : Type ?u.1208868
E : Type u_2
F : Type ?u.1208874
G : Type ?u.1208877
inst✝² : SeminormedCommGroup E
inst✝¹ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
inst✝ : PseudoEMetricSpace α
K Kf Kg : ℝ≥0
f g : α → E
hf : AntilipschitzWith Kf f
hg : LipschitzWith Kg g
hK : Kg < Kf⁻¹
this : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace (_ : ∀ (x y : α), edist x y ≠ ⊤)
x y : α
⊢ dist x y ≤ dist (f x * g x) (f y * g y) / ↑(Kf⁻¹ - Kg)
𝓕 : Type ?u.1208856
𝕜 : Type ?u.1208859
α : Type u_1
ι : Type ?u.1208865
κ : Type ?u.1208868
E : Type u_2
F : Type ?u.1208874
G : Type ?u.1208877
inst✝² : SeminormedCommGroup E
inst✝¹ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
inst✝ : PseudoEMetricSpace α
K Kf Kg : ℝ≥0
f g : α → E
hf : AntilipschitzWith Kf f
hg : LipschitzWith Kg g
hK : Kg < Kf⁻¹
this : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace (_ : ∀ (x y : α), edist x y ≠ ⊤)
x y : α
⊢ dist x y ≤ ↑(Kf⁻¹ - Kg)⁻¹ * dist (f x * g x) (f y * g y)
rw [NNReal.coe_inv, ← _root_.div_eq_inv_mul]
𝓕 : Type ?u.1208856
𝕜 : Type ?u.1208859
α : Type u_1
ι : Type ?u.1208865
κ : Type ?u.1208868
E : Type u_2
F : Type ?u.1208874
G : Type ?u.1208877
inst✝² : SeminormedCommGroup E
inst✝¹ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
inst✝ : PseudoEMetricSpace α
K Kf Kg : ℝ≥0
f g : α → E
hf : AntilipschitzWith Kf f
hg : LipschitzWith Kg g
hK : Kg < Kf⁻¹
this : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace (_ : ∀ (x y : α), edist x y ≠ ⊤)
x y : α
⊢ dist x y * ↑(Kf⁻¹ - Kg) ≤ dist (f x * g x) (f y * g y)
𝓕 : Type ?u.1208856
𝕜 : Type ?u.1208859
α : Type u_1
ι : Type ?u.1208865
κ : Type ?u.1208868
E : Type u_2
F : Type ?u.1208874
G : Type ?u.1208877
inst✝² : SeminormedCommGroup E
inst✝¹ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
inst✝ : PseudoEMetricSpace α
K Kf Kg : ℝ≥0
f g : α → E
hf : AntilipschitzWith Kf f
hg : LipschitzWith Kg g
hK : Kg < Kf⁻¹
this : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace (_ : ∀ (x y : α), edist x y ≠ ⊤)
x y : α
⊢ dist x y ≤ dist (f x * g x) (f y * g y) / ↑(Kf⁻¹ - Kg)
rw [le_div_iff (NNReal.coe_pos.2 <| tsub_pos_iff_lt.2 hK)]
𝓕 : Type ?u.1208856
𝕜 : Type ?u.1208859
α : Type u_1
ι : Type ?u.1208865
κ : Type ?u.1208868
E : Type u_2
F : Type ?u.1208874
G : Type ?u.1208877
inst✝² : SeminormedCommGroup E
inst✝¹ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
inst✝ : PseudoEMetricSpace α
K Kf Kg : ℝ≥0
f g : α → E
hf : AntilipschitzWith Kf f
hg : LipschitzWith Kg g
hK : Kg < Kf⁻¹
this : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace (_ : ∀ (x y : α), edist x y ≠ ⊤)
x y : α
⊢ ↑Kf⁻¹ * dist x y - ↑Kg * dist x y ≤ dist (f x * g x) (f y * g y)
𝓕 : Type ?u.1208856
𝕜 : Type ?u.1208859
α : Type u_1
ι : Type ?u.1208865
κ : Type ?u.1208868
E : Type u_2
F : Type ?u.1208874
G : Type ?u.1208877
inst✝² : SeminormedCommGroup E
inst✝¹ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
inst✝ : PseudoEMetricSpace α
K Kf Kg : ℝ≥0
f g : α → E
hf : AntilipschitzWith Kf f
hg : LipschitzWith Kg g
hK : Kg < Kf⁻¹
this : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace (_ : ∀ (x y : α), edist x y ≠ ⊤)
x y : α
⊢ dist x y * ↑(Kf⁻¹ - Kg) ≤ dist (f x * g x) (f y * g y)
rw [mul_comm, NNReal.coe_sub hK.le, _root_.sub_mul]
no goals
𝓕 : Type ?u.1208856
𝕜 : Type ?u.1208859
α : Type u_1
ι : Type ?u.1208865
κ : Type ?u.1208868
E : Type u_2
F : Type ?u.1208874
G : Type ?u.1208877
inst✝² : SeminormedCommGroup E
inst✝¹ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
inst✝ : PseudoEMetricSpace α
K Kf Kg : ℝ≥0
f g : α → E
hf : AntilipschitzWith Kf f
hg : LipschitzWith Kg g
hK : Kg < Kf⁻¹
this : PseudoMetricSpace α := PseudoEMetricSpace.toPseudoMetricSpace (_ : ∀ (x y : α), edist x y ≠ ⊤)
x y : α
⊢ ↑Kf⁻¹ * dist x y - ↑Kg * dist x y ≤ dist (f x * g x) (f y * g y)
calc
  ↑Kf⁻¹ * dist x y - Kg * dist x y ≤ dist (f x) (f y) - dist (g x) (g y) :=
    sub_le_sub (hf.mul_le_dist x y) (hg.dist_le_mul x y)
  _ ≤ _ := le_trans (le_abs_self _) (abs_dist_sub_le_dist_mul_mul _ _ _ _)