English
The triangle inequality holds for edist via pathELength and the invariance results.
Русский
Неравенство треугольника для edist через pathELength и инвариантности.
LaTeX
$$riemannianEDist I x z ≤ riemannianEDist I x y + riemannianEDist I y z$$
Lean4
theorem riemannianEDist_triangle : riemannianEDist I x z ≤ riemannianEDist I x y + riemannianEDist I y z :=
by
apply le_of_forall_gt (fun r hr ↦ ?_)
rcases ENNReal.exists_add_lt_of_add_lt hr with ⟨u, hu, v, hv, huv⟩
rcases exists_lt_locally_constant_of_riemannianEDist_lt hu zero_lt_one with
⟨γ₁, hγ₁0, hγ₁1, hγ₁_smooth, hγ₁, -, hγ₁_const⟩
rcases exists_lt_locally_constant_of_riemannianEDist_lt hv one_lt_two with
⟨γ₂, hγ₂1, hγ₂2, hγ₂_smooth, hγ₂, hγ₂_const, -⟩
let γ := piecewise (Iic 1) γ₁ γ₂
have : riemannianEDist I x z ≤ pathELength I γ 0 2 :=
by
apply riemannianEDist_le_pathELength
· apply ContMDiff.contMDiffOn
exact ContMDiff.piecewise_Iic hγ₁_smooth hγ₂_smooth (hγ₁_const.trans hγ₂_const.symm)
· simp [γ, hγ₁0]
· simp [γ, hγ₂2]
· exact zero_le_two
apply this.trans_lt (lt_trans ?_ huv)
rw [← pathELength_add zero_le_one one_le_two]
gcongr
· convert hγ₁ using 1
apply pathELength_congr
intro t ht
simp [γ, ht.2]
· convert hγ₂ using 1
apply pathELength_congr_Ioo
intro t ht
simp [γ, ht.1]
