English
Symmetry of distance under reversal of arguments.
Русский
Симметрия расстояния при обращении аргументов.
LaTeX
$$riemannianEDist I x y = riemannianEDist I y x$$
Lean4
theorem riemannianEDist_comm : riemannianEDist I x y = riemannianEDist I y x :=
by
suffices H : ∀ x y, riemannianEDist I y x ≤ riemannianEDist I x y from le_antisymm (H y x) (H x y)
intro x y
apply le_of_forall_gt (fun r hr ↦ ?_)
rcases exists_lt_locally_constant_of_riemannianEDist_lt hr zero_lt_one with ⟨γ, γ0, γ1, γ_smooth, hγ, -⟩
let η : ℝ → ℝ := fun t ↦ -t
have h_smooth : ContMDiff 𝓘(ℝ) I 1 (γ ∘ η) := by
apply γ_smooth.comp ?_
simp only [contMDiff_iff_contDiff]
fun_prop
have : riemannianEDist I y x ≤ pathELength I (γ ∘ η) (η 1) (η 0) := by
apply riemannianEDist_le_pathELength h_smooth.contMDiffOn <;> simp [η, γ0, γ1]
rw [← pathELength_comp_of_antitoneOn zero_le_one] at this; rotate_left
· exact monotone_id.neg.antitoneOn _
· exact differentiableOn_neg _
· exact h_smooth.contMDiffOn.mdifferentiableOn le_rfl
apply this.trans_lt
convert hγ
ext t
simp [η]
