Rectifiable paths

Stream: maths

[Rémi Bottinelli]

Hey, I foolishly decided I would start a christmas project consisting in formalizing rectifiable paths, in order to talk about path length, length spaces, etc.
My strategy was that partitions are defined using list of points as in the code below.
My problem is that all those length_on lemmas are a real pain to prove: they get confusing and I have to do case analysis in most of the cases (see my WIP here).
Does anyone have a better idea on how to define length and rectifiability of paths?

Thanks!

import data.real.ennreal
import data.real.nnreal
import data.set.intervals.basic
import topology.metric_space.emetric_space
import topology.metric_space.basic
import data.list.destutter

noncomputable theory

open_locale classical ennreal

open emetric nnreal set

-- TODO: allow `[emetric_space α]`

namespace function

section length_on

variables {α β : Type*} [metric_space α]
variables (f : β → α)

def length_on : list β → nnreal
| list.nil      := 0
| [_]           := 0
| (a :: b :: l) := nndist (f a) (f b) + length_on (b :: l)

lemma length_on_destutter : ∀ l, f.length_on l = f.length_on (list.destutter (≠) l) := sorry


lemma length_on_reverse : ∀ (l : list β), f.length_on l.reverse = f.length_on l := sorry

end length_on

section path_length

variables {α : Type*} [metric_space α] {s t : set ℝ}
variables (f : s → α) (l : list s)

/--
The path length of `f` is the supremum over all strictly increasing partitions `l`
of the length of `f` for `l`
-/
def path_length : ennreal :=
  ⨆ l ∈ {l : list s | l.pairwise (≤)}, f.length_on l

lemma path_length_mono (h : t ⊆ s) : (f ∘ inclusion h).path_length ≤ f.path_length := sorry

lemma path_length_comp (φ : t → s) :
  (f ∘ φ).path_length ≤ f.path_length := sorry

lemma path_length_reparametrize (φ : t → s) [monotone φ] [surjective φ] :
  (f ∘ φ).path_length = f.path_length := sorry

lemma path_length_reparametrize_anti (φ : t → s) [antitone φ] [surjective φ] :
  (f ∘ φ).path_length = f.path_length := sorry

lemma path_length_glue_split (x : ℝ) (xs : x ∈ s) : f.path_length =
  (f ∘ (inclusion (λ x h, h.1 : {y ∈ s | y ≤ x} ⊆ s))).path_length +
  (f ∘ (inclusion (λ x h, h.1 : {y ∈ s | y ≥ x} ⊆ s))).path_length := sorry

/--
A path is rectifiable if any of its restriction to a close interval has finite length
-/
def is_rectifiable := ∀ (a b : ℝ), ∃ (h : (Icc a b) ⊆ s), (f ∘ inclusion h).path_length ≠ ⊤


end path_length

end function

[Rémi Bottinelli]

We could want to define function.length_on (f : X -> Y) (s : finset X) -> R but that would be more work I think

[Yakov Pechersky]

How about defining it as "sum (zip_with nndist (map f l) (map f (tail l)))"? Or proving the two are the same

[Yakov Pechersky]

Then you get all the lemmas about how tail, map, zip_with operate on cons, append, etc, "for free"

[Yakov Pechersky]

l.pairwise le is spelled "sorted" iirc

[Rémi Bottinelli]

Yakov Pechersky said:

How about defining it as "sum (zip_with nndist (map f l) (map f (tail l)))"? Or proving the two are the same

I have this:

lemma length_on_cons_list_append_cons : ∀ (a : β) (l : list β) (z : β),
  f.length_on ([a] ++ l ++ [z]) = (list.map₂ (λ x y, nndist (f x) (f y)) ([a] ++ l) (l ++ [z])).sum

but your phrasing might be better indeed: it handles empty or singleton lists without problem I assume.

[Rémi Bottinelli]

Would you define the length as this zippy thing, or keep the original?

[Yakov Pechersky]

Since they're provably the same, does it matter?

[Yakov Pechersky]

I'm assuming that proving monotonicity is easier in the sum form

[Patrick Massot]

Rémi, are you familier with Yuri's work on Riemann-like integration? There are probably ideas to take there.

[Rémi Bottinelli]

Patrick Massot said:

Rémi, are you familier with Yuri's work on Riemann-like integration? There are probably ideas to take there.

Not familiar, no, thanks for the link!

[Rémi Bottinelli]

I think the definition is pretty solid, actually:

def path_length : ennreal :=
  ⨆ l ∈ {l : list s | l.sorted (≤)}, f.length_on l


lemma _root_.list.map_sorted {α β : Type*} [preorder α] [preorder β] {φ : α → β} (mφ : monotone φ) :
∀ (l : list α), l.sorted (≤) → (l.map φ).sorted (≤) :=
begin
  apply list.pairwise.rec,
  simp only [list.map_nil, list.sorted_nil],
  rintro a l hi sl hiφ,
  constructor, rotate, assumption,
  rintro a' a'mem,
  simp only [list.mem_map] at a'mem,
  obtain ⟨a,al,rfl⟩ := a'mem,
  apply mφ, apply hi, exact al,
end

lemma path_length_comp (φ : t → s) (mφ : monotone φ) :
  (f ∘ φ).path_length ≤ f.path_length :=
begin
  dsimp [path_length],
  simp only [supr₂_le_iff],
  rintro l ls,
  rw ←f.length_on_map,
  exact @le_supr₂ _ _ _ _
    (λ (l : list ↥s) (H : list.sorted (≤) l), (↑(f.length_on l) : ennreal))
    (l.map φ) (l.map_sorted mφ ls),
end

lemma path_length_mono (h : t ⊆ s) : (f ∘ inclusion h).path_length ≤ f.path_length :=
begin
  apply path_length_comp,
  rintro ⟨a,ha⟩ ⟨b,hb⟩,
  exact id,
end

lemma path_length_reparametrize (φ : t → s) (mφ : monotone φ) (sφ : surjective φ) :
  (f ∘ φ).path_length = f.path_length :=
begin
  apply le_antisymm,
  apply f.path_length_comp φ mφ,

  -- Yael should know a lemma for this
  obtain ⟨ψ,φψ⟩ := sφ.has_right_inverse,
  have mψ : monotone ψ := by
  { rintro x y l,
    have := le_total (ψ x) (ψ y),
    cases this,
    { exact this, },
    { let := mφ (this),
      rw [φψ x, φψ y] at this,
      cases le_antisymm l this, refl, } },

  --have fc : (f ∘ φ) ∘ ψ = f := by { ext, simp, rw φψ x, },
  --nth_rewrite_lhs 0 ←fc,
  convert (f ∘ φ).path_length_comp ψ mψ,
  ext x,
  simp only [comp_app, φψ x],

end

[Rémi Bottinelli]

I wouldn't have thought reparametrization would be so easy to show.

[Sebastien Gouezel]

We already have the definition and the main properties, see docs#has_bounded_variation_on and the results in this file.

[Rémi Bottinelli]

Ah, good, but too bad!

[Yaël Dillies]

Ahah, I love being called out in Lean comments :laughing:

[Yaël Dillies]

I'm sure there's a lemma for it, but I'll have to dig. If you're searching it before I get to a computer, try looking around docs#real.sqrt, whose definition proceeds the exact same way as your argument.

[Rémi Bottinelli]

I'd have thought there is some order lemma I can use for that purpose, no?

[Yaël Dillies]

I suspect it will be a definition instead. But yeah

[Rémi Bottinelli]

@Sebastien Gouezel I'm wondering: what made you decide on this formulation for rectifiability/bounded variation, in terms of infinite sums rather than the more "basic" version I'm trying?

[Sebastien Gouezel]

It's not in terms of infinite sums, it's in terms of finite sums indexed by range n. And the reason was probably that we already have a big API around sums indexed by range n (and also it's the way I'd write it in a math paper!). Lists are probably more natural from a computability point of view, but I don't care about computability :-) In fact I wouldn't say your version is more basic, maybe more CS-y

[Rémi Bottinelli]

Mmh, sorry, I didn't read in details enough it seems!

[Rémi Bottinelli]

I'm still trying to figure out rectifiability with lists as first presented, and my code has plenty of strange issues.

• Sometimes a single simp doesn't simplify enough.
• The sorry line 59 should be refl but that doesn't work.
• Similarly at line 363.

I tried extracting a MWE but the issue disappeared. There also is some general slowness working with this file. What can be going wrong?

[Rémi Bottinelli]

@Sebastien Gouezel Leaving aside my own trials, in bounded_variation.lean:

• I don't see anything about precomposing your function with a monotone function. Is there a reason for it? With may list approach it seems to work fine; it should be fine with yours too ?
• I don't see anything about arc-length parametrization. Would that fit here or should some other file in geometry be a better place for it?

[Rémi Bottinelli]

Since you've done plenty of the work already, I believe it's better for me to contribute on that codebase, hence my questions.

[Sebastien Gouezel]

There should be no problem to prove things for composition with monotone functions, it's just that I haven't needed it -- and it should be an essentially trivial consequence of the definition. As for arc-length parametrization, what you want is to get a parametrization which becomes an isometry on its domain, right? I think it would amount to composing with the inverse of the function t -> evariation_on f (Icc 0 t) (or a real version of this one), but that would definitely require some work.

[Rémi Bottinelli]

Indeed, I think as long as the space is not pseudo-metric, then evariation_on f (Icc 0 t) = evariation_on f (Icc 0 t') implies f t = f t', and the the arc-length parametrization is well-defined.

[Rémi Bottinelli]

I'm not exactly sure about what kind of domain we can have for f: would assuming an interval be general enough?

[Rémi Bottinelli]

variables {α β : Type*} [linear_order α] [linear_order β] (φ : β → α) (hφ : monotone φ)
{E F : Type*} [pseudo_emetric_space E] [pseudo_emetric_space F]
{V : Type*} [normed_add_comm_group V] [normed_space ℝ V] [finite_dimensional ℝ V]


namespace evariation_on

include hφ
lemma mono' (f : α → E) {s : set α} {t : set β} (φst : ∀ {x}, x ∈ t → φ x ∈ s) :
  evariation_on (f∘φ) t ≤ evariation_on f s :=
begin
  apply supr_le _,
  rintros ⟨n, ⟨u, hu, ut⟩⟩,
  exact le_supr (λ (p : ℕ × {u : ℕ → α // monotone u ∧ ∀ i, u i ∈ s}),
    ∑ i in finset.range p.1, edist (f ((p.2 : ℕ → α) (i+1))) (f ((p.2 : ℕ → α) i))) ⟨n, ⟨φ ∘ u, hφ.comp hu, λ i, φst (ut i)⟩⟩,
end

end evariation_on

[Rémi Bottinelli]

easy enough :)

[Sebastien Gouezel]

You should rather write it assuming only that phi is monotone on t, and your assumption phist is mapsto phi t s.

[Sebastien Gouezel]

Rémi Bottinelli said:

I'm not exactly sure about what kind of domain we can have for f: would assuming an interval be general enough?

I'd start with an interval, prove everything in this setting, and then check afterwards if things are easy to generalize or not.

[Rémi Bottinelli]

Sebastien Gouezel said:

You should rather write it assuming only that phi is monotone on t, and your assumption phist is mapsto phi t s.

Mmh, yeah, and I'm now troubled by trying to prove that if \phi maps t onto s then the evariation is equal. When not working with sets, you can just construct an inverse, but here I'll need to construct some kind of partial inverse with trash values outside of s I guess?

[Rémi Bottinelli]

Ah, I think the API around surj_on is complete enough… let me see.

[Sebastien Gouezel]

Note that even when working with sets you have to be careful when \phi is only monotone, not strictly monotone. There is still a good notion of pseudo-inverse, where f^{-1}(x) = Sup {y \in s | f y <= x} (or the dual version), but I am not sure we have anything on that in mathlib. The order experts would know!

[Rémi Bottinelli]

Are you talking about the arc-length parametrization question, or my last comment. If it's my last comment, I don't think we need any strictness. At least I didn't in my initial attempt.

[Sebastien Gouezel]

I mean, I agree you don't need any strictness, but the intuition works better when you have strictness since you have a genuine inverse on s / t.

[Rémi Bottinelli]

The whole point of u : nat -> \alpha and not Fin n -> \alpha is to get rid of the empty/singleton list troubles I have, right?

[Yaël Dillies]

Looks like the adjoint functor theorem to me :grinning_face_with_smiling_eyes:

[Rémi Bottinelli]

Just adapted my previous code: is it only slow for me?

/-
Copyright (c) 2022 Sébastien Gouëzel. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sébastien Gouëzel
-/
import measure_theory.measure.lebesgue
import analysis.calculus.monotone
import analysis.bounded_variation

open_locale big_operators nnreal ennreal
open set measure_theory

variables {α β : Type*} [linear_order α] [linear_order β]
{E F : Type*} [pseudo_emetric_space E] [pseudo_emetric_space F]
{V : Type*} [normed_add_comm_group V] [normed_space ℝ V] [finite_dimensional ℝ V]


namespace evariation_on

lemma comp_mono (f : α → E) {s : set α} {t : set β} (φ : β → α)
  (hφ : monotone_on φ t ) (φst : set.maps_to φ t s) :
  evariation_on (f∘φ) t ≤ evariation_on f s :=
begin
  apply supr_le _,
  rintros ⟨n, ⟨u, hu, ut⟩⟩,
  exact le_supr (λ (p : ℕ × {u : ℕ → α // monotone u ∧ ∀ i, u i ∈ s}),
    ∑ i in finset.range p.1, edist (f ((p.2 : ℕ → α) (i+1))) (f ((p.2 : ℕ → α) i)))
    ⟨n, ⟨φ ∘ u, λ x y xy, hφ (ut x) (ut y) (hu xy), λ i, φst (ut i)⟩⟩,
end

lemma eq_of_eq_on {f f' : α → E} {s : set α} (h : set.eq_on f f' s) :
  evariation_on f s = evariation_on f' s := sorry

lemma comp_eq (f : α → E) {s : set α} {t : set β} [nonempty β] (φ : β → α)
  (hφ : monotone_on φ t ) (φst : set.maps_to φ t s) (φsur : set.surj_on φ t s) :
  evariation_on (f∘φ) t = evariation_on f s :=
begin

  apply le_antisymm,
  { apply comp_mono f φ hφ φst, },

  let ψ := φ.inv_fun_on t,
  have ψφs : set.eq_on (φ∘ψ) id s := φsur.right_inv_on_inv_fun_on,
  have ψts : set.maps_to ψ s t := φsur.maps_to_inv_fun_on,
  have hψ : monotone_on ψ s, by
  { rintro x xs y ys l,
    rcases  le_total (ψ x) (ψ y) with (ψxy|ψyx),
    { exact ψxy, },
    { let := hφ (ψts ys) (ψts xs) ψyx,
      simp only [←function.comp_app φ ψ] at this,
      rw [ψφs xs,ψφs ys] at this,
      cases le_antisymm l this,
      refl, }, },

  change evariation_on (f∘id) s ≤ evariation_on (f ∘ φ) t,
  rw ←eq_of_eq_on (ψφs.comp_left : set.eq_on (f ∘ (φ∘ψ)) (f ∘ id) s),
  apply comp_mono _ ψ hψ ψts,
end


end evariation_on

[Rémi Bottinelli]

Seems longer than necessary?

/-
Copyright (c) 2022 Sébastien Gouëzel. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sébastien Gouëzel
-/
import measure_theory.measure.lebesgue
import analysis.calculus.monotone
import analysis.bounded_variation
import tactic.swap_var

open_locale big_operators nnreal ennreal
open set measure_theory

variables {α β : Type*} [linear_order α] [linear_order β]
{E F : Type*} [pseudo_emetric_space E] [pseudo_emetric_space F]
{V : Type*} [normed_add_comm_group V] [normed_space ℝ V] [finite_dimensional ℝ V]


namespace evariation_on

lemma eq_of_eq_on {f f' : α → E} {s : set α} (h : set.eq_on f f' s) :
  evariation_on f s = evariation_on f' s :=
begin
  apply le_antisymm,
  work_on_goal 2 { swap_var f ↔ f', replace h := h.symm, },
  all_goals
  { apply supr_le _,
    rintros ⟨n, ⟨u, hu, us⟩⟩,
    simp,
    have : ∑ (x : ℕ) in finset.range n, edist (f (u (x + 1))) (f (u x)) =
           ∑ (x : ℕ) in finset.range n, edist (f' (u (x + 1))) (f' (u x)), by
    { congr, funext n, congr; apply h (us $ _), },
    rw this,
    apply le_supr (λ (p : ℕ × {u : ℕ → α // monotone u ∧ ∀ i, u i ∈ s}),
      ∑ i in finset.range p.1, edist (f' ((p.2 : ℕ → α) (i+1))) (f' ((p.2 : ℕ → α) i)))
      ⟨n, ⟨u, hu, us⟩⟩, },
end

end evariation_on

[Sebastien Gouezel]

lemma eq_of_eq_on {f f' : α → E} {s : set α} (h : set.eq_on f f' s) :
  evariation_on f s = evariation_on f' s :=
begin
  dsimp only [evariation_on],
  congr' 1 with p : 1,
  congr' 1 with i : 1,
  congr' 1;
  exact h (p.2.2.2 _),
end

[Kevin Buzzard]

comp_eq is slow for me too, and it's the final apply. If you change it to exact it becomes fast.

[Sebastien Gouezel]

Rémi Bottinelli said:

The whole point of u : nat -> \alpha and not Fin n -> \alpha is to get rid of the empty/singleton list troubles I have, right?

Not only empty or singletons. Also when gluing two sequences into a bigger sequences it will make your life easier. Avoiding dependent type hell is always a good idea. That's why summing over range n is almost always a better idea than summing over fin n.

[Sebastien Gouezel]

As Kevin says, changing apply to exact makes it fast. Also, it would probably be a good idea to extract the lemma saying that the inverse of a monotone_on map is monotone_on (your hψ). Otherwise, this looks very good and pretty efficient!

[Rémi Bottinelli]

I'll try arc-length parametrization tomorrow, and then I can try to play with the length metric and more complicated stuff.

[Rémi Bottinelli]

Kevin Buzzard said:

comp_eq is slow for me too, and it's the final apply. If you change it to exact it becomes fast.

It seems that apply is never the right choice: refine is more intelligent and exact faster ?!

[Ruben Van de Velde]

I've unfortunately also heard of cases where apply was much faster than exact

[Rémi Bottinelli]

I want to work on the bounded_variation code-base since it's already there, but kept exploring my initial approach and it turned out to work quite well imo :

-- definition 'length_on' depends on 'ennreal.canonically_ordered_comm_semiring
-- so says lean
noncomputable def length_on : list β → ennreal :=
list.rec 0
  (λ (a : β) (l : list β) (ih : ennreal),
      list.rec 0 (λ (b : β) (l : list β) (ih' : ennreal), edist (f a) (f b) + ih) l)

lemma length_on_nil : f.length_on list.nil = 0 := rfl
lemma length_on_singleton (a : β) : f.length_on [a] = 0 := rfl
lemma length_on_cons_cons (a b : β) (l : list β) :
  f.length_on (a::b::l) = edist (f a) (f b) + f.length_on (b::l) := rfl

lemma length_on_pair (a b : β) : edist (f a) (f b) = f.length_on [a, b] :=
by simp only [length_on_cons_cons, length_on_singleton, add_zero]

lemma length_on_append_cons_cons :
   ∀ (l : list β) (a b : β), f.length_on (l ++ [a, b]) = f.length_on (l ++ [a]) + edist (f a) (f b)
| [] a b := by
  { simp only [length_on, list.nil_append, add_zero, zero_add], }
| [x] a b := by
  { simp only [length_on, list.singleton_append, add_zero], }
| (x :: y :: l) a b := by
  { simp only [length_on_cons_cons, list.cons_append, add_assoc],
    congr,
    simp only [←list.cons_append],
    apply length_on_append_cons_cons, }

lemma length_on_le_length_on_cons (c : β) (l : list β) : f.length_on l ≤ (f.length_on $ c :: l) :=
by { cases l, simp only [length_on, le_zero_iff], simp only [length_on], apply self_le_add_left _ _, }

lemma length_on_drop_second_cons_le :
  ∀ (a b : β) (l : list β), f.length_on (a :: l) ≤ f.length_on (a :: b :: l)
| _ _ []  := by
  { apply length_on_le_length_on_cons, }
| a b (c::l) := by
  { simp only [length_on, ←add_assoc],
    apply add_le_add_right (edist_triangle _ _ _) (f.length_on (c :: l)), }

lemma length_on_append : ∀ l l', f.length_on l + f.length_on l' ≤ f.length_on (l ++ l')
| [] l' := by
  { rw [list.nil_append, length_on, zero_add], exact le_refl (f.length_on l'), }
| [a] l' := by
  { rw [list.singleton_append, length_on, zero_add],
    apply length_on_le_length_on_cons, }
| (a :: b :: l) l' := by
  { rw [list.cons_append, length_on, add_assoc],
    refine add_le_add_left (length_on_append (b::l) l') _, }

lemma length_on_reverse : ∀ (l : list β), f.length_on l.reverse = f.length_on l
| [] := rfl
| [a] := rfl
| (a :: b :: l) := by
  { simp only [length_on_append_cons_cons, ←length_on_reverse (b :: l), list.reverse_cons,
               list.append_assoc, list.singleton_append, length_on_cons_cons],
    rw [add_comm, edist_comm], }

lemma length_on_map {γ : Type*} (φ : γ → β) :
  ∀ (l : list γ), f.length_on (l.map φ) = (f ∘ φ).length_on l
| [] := by { simp only [length_on, list.map_nil], }
| [a] := by { simp only [length_on, list.map], }
| (a :: b :: l)  := by
  { simp only [length_on_cons_cons, list.map, comp_app, ←length_on_map (b::l)], }

lemma length_on_le_append_singleton_append :
  ∀ (l : list β) (x : β) (l' : list β), f.length_on (l ++ l') ≤ f.length_on (l ++ [x] ++ l')
| [] x l' := by { apply length_on_le_length_on_cons, }
| [a] x l' := by { apply length_on_drop_second_cons_le, }
| (a :: b :: l) x l' := by
  { change a :: b :: l ++ l' with a :: b :: (l ++ l'),
    change a :: b :: l ++ [x] ++ l' with a :: b :: (l ++ [x] ++ l'),
    simp only [length_on],
    apply add_le_add_left _ (edist (f a) (f b)),
    exact length_on_le_append_singleton_append (b :: l) x l', }

lemma length_on_append_singleton_append :
  ∀ (l : list β) (x : β) (l' : list β),
    f.length_on (l ++ [x] ++ l') = f.length_on (l ++ [x]) + f.length_on ([x] ++ l')
| [] x l' := by { simp only [length_on, list.nil_append, zero_add]}
| [a] x l' := by
  { simp only [length_on, list.singleton_append, list.cons_append, add_zero, eq_self_iff_true,
               list.nil_append], }
| (a :: b :: l) x l' := by
  { simp only [length_on_cons_cons, list.cons_append, list.append_assoc, list.singleton_append,
    add_assoc],
    congr,
    simp_rw [←list.cons_append b l, ←@list.singleton_append _ x l',←list.append_assoc],
    exact length_on_append_singleton_append (b::l) x l', }

lemma length_on_mono' :
  ∀ {l l' : list β}, l <+ l' → ∀ x, f.length_on (x::l) ≤ f.length_on (x::l')
| _ _ list.sublist.slnil             x := by { simp only [length_on, le_zero_iff], }
| _ _ (list.sublist.cons  l₁ l₂ a s) x :=
  (f.length_on_drop_second_cons_le x a l₁).trans $ add_le_add_left (length_on_mono' s a) _
| _ _ (list.sublist.cons2 l₁ l₂ a s) x := add_le_add_left (length_on_mono' s a) _

lemma length_on_mono : ∀ {l l' : list β}, l <+ l' → f.length_on l ≤ f.length_on l'
| _ _ list.sublist.slnil             := by { simp only [length_on, le_zero_iff], }
| _ _ (list.sublist.cons  l₁ l₂ a s) :=
  (f.length_on_le_length_on_cons a l₁).trans $ f.length_on_mono' s a
| _ _ (list.sublist.cons2 l₁ l₂ a s) := f.length_on_mono' s a

lemma edist_le_length_on_of_mem {a b : β} {l : list β} (al : a ∈ l) (bl : b ∈ l) :
  edist (f a) (f b) ≤ f.length_on l :=
begin
  rcases l.pair_mem_list al bl with rfl|ab|ba,
  { simp only [edist_self, zero_le'], },
  { rw [length_on_pair], exact f.length_on_mono ab, },
  { rw [edist_comm, length_on_pair], exact f.length_on_mono ba, }
end

end length_on

section path_length

variables {α : Type*} [pseudo_emetric_space α]
  {β : Type*} [linear_order β]
  {γ : Type*} [linear_order γ]
variables (f : β → α) (l : list β)

/--
The path length of `f` is the supremum over all strictly increasing partitions `l`
of the length of `f` for `l`
-/
noncomputable def path_length : ennreal :=
  ⨆ l ∈ {l : list β | l.pairwise (≤)}, f.length_on l

def sorted_list_nonempty : set.nonempty {l : list β | l.pairwise (≤)} := ⟨[],list.pairwise.nil⟩

lemma path_length_comp_mono (φ : γ → β) (mφ : monotone φ) :
  (f ∘ φ).path_length ≤ f.path_length :=
begin
  simp only [path_length, supr₂_le_iff, ←f.length_on_map φ],
  rintro l ls,
  exact @le_supr₂ _ _ _ _ (λ l H, f.length_on l) (l.map φ) (list.pairwise.map φ mφ ls),
end

lemma path_length_comp_anti (φ : γ → β) (mφ : antitone φ) :
  (f ∘ φ).path_length ≤ f.path_length :=
begin
  simp only [path_length, supr₂_le_iff, ←f.length_on_map φ],
  rintro l ls,
  rw [←f.length_on_reverse, ←list.map_reverse],
  refine @le_supr₂ _ _ _ _  (λ l H, f.length_on l) _ _,
  apply list.pairwise.map φ _ (list.pairwise_reverse.mpr ls),
  rintro a b h, exact mφ h,
end

lemma path_length_reparametrize_mono (φ : γ → β) (mφ : monotone φ) (sφ : surjective φ) :
  (f ∘ φ).path_length = f.path_length :=
begin
  apply le_antisymm,
  apply f.path_length_comp_mono φ mφ,

  obtain ⟨ψ,φψ⟩ := sφ.has_right_inverse,

  convert (f ∘ φ).path_length_comp_mono ψ (right_inverse_monotone φ mφ ψ φψ),
  ext x,
  simp only [comp_app, φψ x],
end

lemma path_length_reparametrize_anti (φ : γ → β) (mφ : antitone φ) (sφ : surjective φ) :
  (f ∘ φ).path_length = f.path_length :=
begin
  apply le_antisymm,
  apply f.path_length_comp_anti φ mφ,

  obtain ⟨ψ,φψ⟩ := sφ.has_right_inverse,

  convert (f ∘ φ).path_length_comp_anti ψ (right_inverse_antitone φ mφ ψ φψ),
  ext x,
  simp only [comp_app, φψ x],
end

lemma path_length_ge_parts (l r : set β) (lr : ∀ x ∈ l, ∀ y ∈ r, x ≤ y) :
  (f ∘ (coe : subtype l → β)).path_length
  + (f ∘ (coe : subtype r → β)).path_length ≤ (f.path_length) :=
begin
  apply ennreal.bsupr_add_bsupr_le sorted_list_nonempty sorted_list_nonempty,
  rintro left lefts right rights,
  simp_rw [←length_on_map f coe],
  apply (f.length_on_append _ _).trans,
  dsimp only [path_length],
  refine @le_supr₂ _ _ _ _ (λ l H, f.length_on l) _ _,
  rw [mem_set_of, list.pairwise_append],
  refine ⟨list.pairwise.map _ (λ a b h, h) lefts,
          list.pairwise.map _ (λ a b h, h) rights,
          λ x xleft y yright, _⟩,
  simp only [list.mem_map, subtype.exists, subtype.coe_mk, exists_and_distrib_right,
             exists_eq_right] at xleft yright,
  obtain ⟨xl,xleft⟩ := xleft,
  obtain ⟨yr,yright⟩ := yright,
  exact lr x xl y yr,
end

lemma path_length_glue_split (m : β) :
  f.path_length = (f ∘ (coe : {x // x ≤ m} → β)).path_length
                + (f ∘ (coe : {x // m ≤ x} → β)).path_length :=
begin
  dsimp only [path_length],
  apply le_antisymm,
  { rw supr₂_le_iff,
    rintro l ls,
    rw ←list.take_while_append_drop (≤m) l,
    apply (length_on_le_append_singleton_append f _ m _).trans,
    rw length_on_append_singleton_append,
    refine add_le_add _ _,
    { transitivity' (f ∘ coe).length_on (l.take_while_subtype m ++ [⟨m,le_refl m⟩]),
      { rw [←f.length_on_map coe, list.map_append, list.take_while_subtype_map_coe],
        simp only [list.map, subtype.coe_mk], exact le_refl _, },
      { refine @le_supr₂ _ _ _ _ (λ l H, length_on (f ∘ coe) l) _ _,
        simp only [list.pairwise_append, mem_set_of_eq, list.mem_singleton],
        refine ⟨list.take_while_subtype_pairwise_le _ _, list.pairwise_singleton _ _, _⟩,
        rintro y yl _ rfl,
        exact list.take_while_subtype_le_base m l y yl, }, },
    { transitivity' (f ∘ coe).length_on
        ([(⟨m,le_refl m⟩ : {x // m ≤ x})] ++ (l.drop_while_subtype_ge m ls)),
      { rw [←f.length_on_map coe, list.map_append, list.drop_while_subtype_ge_map_coe],
        simp only [list.map, subtype.coe_mk], exact le_refl _, },
      { refine @le_supr₂ _ _ _ _ (λ l H, length_on (f ∘ coe) l) _ _,
        simp only [list.singleton_append, mem_set_of_eq, list.pairwise_cons,
                   subtype.mk_le_mk],
        refine ⟨list.drop_while_subtype_ge_ge_base _ _ _,
                list.drop_while_subtype_ge_pairwise_le _ _ _⟩, }, }, },
  { apply path_length_ge_parts,
    rintro x xm y my, apply le_trans xm my, }, -- `xm.trans my` doesn't work
end

end path_length

end function

There is some sorried-out stuff hiding in a side file, but still, the code looks more concise than the one for bounded_variation, doesn't it?

[Rémi Bottinelli]

I removed many uses of linarith here : https://github.com/leanprover-community/mathlib/pull/17998

[Rémi Bottinelli]

I need this one to get that the path metric is symmetric.

lemma comp_antitone_mono (f : α → E) {s : set α} {t : set β} (φ : β → α)
  (hφ : antitone_on φ t ) (φst : set.maps_to φ t s) :
  evariation_on (f∘φ) t ≤ evariation_on f s :=
begin
  apply supr_le _,
  rintros ⟨n, ⟨u, hu, ut⟩⟩,
  have : ∑ i in finset.range n, edist (f∘φ $ u (i+1)) (f∘φ $ u i) =
         ∑ i in finset.range n, edist (f∘φ $ u $ n-(i+1)) (f∘φ $ u $ n-i), by
  { induction n with m ih,
    { simp only [finset.range_zero, finset.sum_empty], },
    { simp only [function.comp_app],
    rw [finset.sum_range_succ, finset.sum_range_succ'],
    simp [nat.succ_sub_succ_eq_sub, zero_add, nat.succ_add_sub_one, tsub_zero,
               function.comp_app] at ih ⊢,
    rw ih,
    nth_rewrite_rhs 0 edist_comm, } },
  change ∑ i in finset.range n, edist (f∘φ $ u (i+1)) (f∘φ $ u i) ≤ evariation_on f s,
  rw this,
  let ru : ℕ → β := λ i, u (n-i),
  have rut : ∀ i : ℕ, ru i ∈ t := λ i, ut (n-i),
  have hru : antitone ru := λ i j l, hu (n.sub_le_sub_left l),
  exact le_supr (λ (p : ℕ × {u : ℕ → α // monotone u ∧ ∀ i, u i ∈ s}),
    ∑ i in finset.range p.1, edist (f ((p.2 : ℕ → α) (i+1))) (f ((p.2 : ℕ → α) i)))
    ⟨n, ⟨φ ∘ ru, λ x y xy, hφ (rut y) (rut x) (hru xy), λ i, φst (rut i)⟩⟩,
end

[Sebastien Gouezel]

I agree that your code looks nice! You are a little bit reinventing the wheel at the beginning with your inductive definition of length_on, though: instead, you should probably use list.sum with some zip operation or whatever. Also, there is no subset in sight (you are considering increasing lists without requiring that the points belong to a subset s) -- you can work this around using subtypes, but from an API point of view the subset approach is probably better.

[Rémi Bottinelli]

Rémi Bottinelli said:

I need this one to get that the path metric is symmetric.

lemma comp_antitone_mono (f : α → E) {s : set α} {t : set β} (φ : β → α)
  (hφ : antitone_on φ t ) (φst : set.maps_to φ t s) :
  evariation_on (f∘φ) t ≤ evariation_on f s :=
begin
  apply supr_le _,
  rintros ⟨n, ⟨u, hu, ut⟩⟩,
  have : ∑ i in finset.range n, edist (f∘φ $ u (i+1)) (f∘φ $ u i) =
         ∑ i in finset.range n, edist (f∘φ $ u $ n-(i+1)) (f∘φ $ u $ n-i), by
  { induction n with m ih,
    { simp only [finset.range_zero, finset.sum_empty], },
    { simp only [function.comp_app],
    rw [finset.sum_range_succ, finset.sum_range_succ'],
    simp [nat.succ_sub_succ_eq_sub, zero_add, nat.succ_add_sub_one, tsub_zero,
               function.comp_app] at ih ⊢,
    rw ih,
    nth_rewrite_rhs 0 edist_comm, } },
  change ∑ i in finset.range n, edist (f∘φ $ u (i+1)) (f∘φ $ u i) ≤ evariation_on f s,
  rw this,
  let ru : ℕ → β := λ i, u (n-i),
  have rut : ∀ i : ℕ, ru i ∈ t := λ i, ut (n-i),
  have hru : antitone ru := λ i j l, hu (n.sub_le_sub_left l),
  exact le_supr (λ (p : ℕ × {u : ℕ → α // monotone u ∧ ∀ i, u i ∈ s}),
    ∑ i in finset.range p.1, edist (f ((p.2 : ℕ → α) (i+1))) (f ((p.2 : ℕ → α) i)))
    ⟨n, ⟨φ ∘ ru, λ x y xy, hφ (rut y) (rut x) (hru xy), λ i, φst (rut i)⟩⟩,
end

I think the have here probably should be covered by a lemma telling us that reversing doesn't change sums, but couldn't find it.

[Rémi Bottinelli]

Sebastien Gouezel said:

I agree that your code looks nice! You are a little bit reinventing the wheel at the beginning with your inductive definition of length_on, though: instead, you should probably use list.sum with some zip operation or whatever. Also, there is no subset in sight (you are considering increasing lists without requiring that the points belong to a subset s) -- you can work this around using subtypes, but from an API point of view the subset approach is probably better.

Thanks!

• Regarding reinventing the wheel, yeah, Yakov proposed sum (zip_with nndist (map f l) (map f (tail l))) above, but after trying this, lemmas that are very simple by induction become quite messy (imo), because of the multiple unpackings you have to do, and the tail being defined by cases, etc.
• Regarding subset: that's a "design choice" I didn't even think of at first. It could probably be changed easily.

If it seems like this is a reasonable alternative, I'd be happy to work on it some more and eventually do a swap. Otherwise I'll continue using the original code.

[Rémi Bottinelli]

α: Type u_1
β: Type u_2
_inst_1: linear_order α
_inst_2: linear_order β
E: Type u_3
_inst_3: pseudo_emetric_space E
f: α → E
s: set α
t: set β
φ: β → α
hφ: antitone_on φ t
φst: maps_to φ t s
n: ℕ
u: ℕ → β
hu: monotone u
ut: ∀ (i : ℕ), u i ∈ t
⊢ ∑ (x : ℕ) in finset.range n, edist ((f ∘ φ) (u (n - x - 1))) ((f ∘ φ) (u (n - x - 1 + 1))) ≤ evariation_on f s

I'm trying to change n-x-1+1 to n-x here. I tried using conv but getting to the term I want doesn't include the assumption x<n necessary for this rewrite to be legal.

[Kevin Buzzard]

You'll need to use docs#finset.sum_congr

[Rémi Bottinelli]

Not much shorter, but at least there is no induction going on in comp_antitone_mono

theorem finset.sum_range_reverse {β : Type*} [add_comm_monoid β] (f : ℕ → β) (n : ℕ) :
  (finset.range n).sum (λ (x : ℕ), f x) = (finset.range n).sum (λ (x : ℕ), f $ n-x-1) :=
begin
  induction n with m ih,
  { simp only [finset.range_zero, finset.sum_empty], },
  { simp only [function.comp_app],
  rw [finset.sum_range_succ, finset.sum_range_succ'],
  simp [nat.succ_sub_succ_eq_sub, zero_add, nat.succ_add_sub_one, tsub_zero,
             function.comp_app] at ih ⊢,
  rw ih, },
end

lemma comp_antitone_mono (f : α → E) {s : set α} {t : set β} (φ : β → α)
  (hφ : antitone_on φ t ) (φst : set.maps_to φ t s) :
  evariation_on (f∘φ) t ≤ evariation_on f s :=
begin
  apply supr_le _,
  rintros ⟨n, ⟨u, hu, ut⟩⟩,
  change ∑ i in finset.range n, edist (f∘φ $ u (i+1)) (f∘φ $ u i) ≤ evariation_on f s,
  rw finset.sum_range_reverse,
  have : ∀ x : ℕ, x ∈ finset.range n →
                  edist ((f ∘ φ) (u (n - x - 1 + 1))) ((f ∘ φ) (u (n - x - 1))) =
                  edist ((f ∘ φ) (u (n - (x + 1)))) ((f ∘ φ) (u (n - x))) := λ x hx, by
  { rw [edist_comm, nat.sub_one, nat.add_one],
    congr,
    apply nat.succ_pred_eq_of_pos,
    simpa only [tsub_pos_iff_lt, finset.mem_range] using hx, },
  rw finset.sum_congr rfl this,
  let ru : ℕ → β := λ i, u (n-i),
  have rut : ∀ i : ℕ, ru i ∈ t := λ i, ut (n-i),
  have hru : antitone ru := λ i j l, hu (n.sub_le_sub_left l),
  exact le_supr (λ (p : ℕ × {u : ℕ → α // monotone u ∧ ∀ i, u i ∈ s}),
    ∑ i in finset.range p.1, edist (f ((p.2 : ℕ → α) (i+1))) (f ((p.2 : ℕ → α) i)))
    ⟨n, ⟨φ ∘ ru, λ x y xy, hφ (rut y) (rut x) (hru xy), λ i, φst (rut i)⟩⟩,
end

[Sebastien Gouezel]

I think we already have docs#finset.sum_range_reflect.

[Rémi Bottinelli]

https://github.com/leanprover-community/mathlib/pull/18001

[Rémi Bottinelli]

As said in the PR comment, I just don't know where those lemmas about inverse of mono/antitone maps should go.

[Rémi Bottinelli]

The naming is not set in stone, but anything longer seemed overkill.

[Rémi Bottinelli]

I'll work on the path metric now because it's more fun, but I think I'll need to add some lemmas to bounded_variation, e.g.

lemma constant_on (f : α → E) {s : set α}
  (hf : (f '' s).subsingleton) : evariation_on f s = 0 :=
begin
  apply le_antisymm _ (zero_le _),
  apply supr_le _,
  rintros ⟨n, ⟨u, hu, ut⟩⟩,
  have : ∀ i, f (u i) = f (u 0) := λ i, hf ⟨u i, ut i, rfl⟩ ⟨u 0, ut 0, rfl⟩,
  simp [subtype.coe_mk, le_zero_iff, finset.sum_eq_zero_iff, finset.mem_range, this],
end

@[simp] protected lemma subsingleton (f : α → E) {s : set α} (hs : s.subsingleton) :
  evariation_on f s = 0 := constant_on f (hs.image f)

[Rémi Bottinelli]

I'm getting kind of stuck on very basic stuff:

• I tried at first to define the path length metric, and this works here, but it's the bare minimum (just that we have a coarser(finer?) metric).
• Then I wanted to attack facts such as the property that taking the length metric is idempotent, and that's where I got into troubles:
• For this I need to show that the arc-length function is continuous on its parameters (under suitable assumptions), and
• For that I need to say that given a continuous path with finite variation, I can cut its domain into pieces in a way given by uniform continuity, and then that I can cut it even finer, etc.
• So I thought all this talk of partitions is not going to cut it if I work with monotonous maps u : nat -> E as a basis for the variation.
• So I tried to actually port the bounded_variation.lean file to work with lists, as I initially planned here, but for all my biais in its favour, I can't really claim that I gain much by working with that new definition, and the port isn't even complete.

[Rémi Bottinelli]

I still kind of like this list approach better since:

• There is a clear separation between everything that concerns finite approximations of length with lists (function.length_on l) and the variation proper, which is just an appropriate supr.
• This makes proofs less bulky and made of more small lemmas, which I believe is preferred for mathlib?
• (Not really an argument but:) with finset.sort, we should easily be able to talk about approximation on finsets instead of lists, which is maybe actually a good idea?

I'm not sure it's necessarily going to help with the kind of thing I need to talk about idempotence of the length metric though.

I'd like to get some opinions on the best approach to continue working on this and actually get something off the ground.
For instance, what would a lemma proving "given a path, there exists a partition of its domain such that the images in each part are at distance at most eps from each other" look like? Is it somewhere in mathlib?

Anyway, I think I spent too much time blindly trying to force things to typecheck, and should let things rest for a while…

[Junyan Xu]

given a path, there exists a partition of its domain such that the images in each part are at distance at most eps from each other

You can use docs#compact_space.uniform_continuous_of_continuous with docs#metric.uniform_continuous_iff and just partition the interval into pieces of length < delta.

[Junyan Xu]

Several comments:
In the bounded_variation_path file:

• I think you can just define length_on of a list E without mentioning the map f : α → E, and use docs#list.map when you have a list α.
• If you use a pattern match definition of length_on, you can probably prove the three lemmas by rw length_on, so you won't need to write them out.
• If you no longer want to replace the whole file bounded_variation.lean with your version based on lists, you still have the option of building APIs around the original definition, including defining length_on and showing the original evariation_on is the supremum of length_on.
• For monotone_on.evariation_on_le (which you stuck on), you could show by induction that the length_on of an ordered list ℝ is equal to the last element minus the first element; monotonicity guarantees orderedness via docs#list.pairwise.map.

In the path_metric file:

• expand_bot/top_half could be defined using docs#set.proj_Icc, which is used to define docs#path.trans.
• For idempotency of the path length metric, I think the proof doesn't invoke continuity the arc-length function; you can take a look at Burago-Burago-Ivanov 2001, Proposition 2.3.12. You do need that to_length_metric is continuous, so a path continuous in the path length metric is also continuous under the original topology. Then the fact that the length of the concatenation of finitely many paths is equal to the sum of the lengths should suffice to complete the proof. You may want to allow paths to take any (not necessarily closed) interval in ℝ as domains, as is done in [BBI]; they also have an axiomatic definition of length structures in 2.1.1 that would apply to lengths from a Riemannian metric, I think, and may be what you're trying to do with paths_with_lengths in your other topic.

[Rémi Bottinelli]

In the meantime, I've got this

lemma edist_sub_of_le {a b : ℝ} {ab : a ≤ b} : edist a b = ennreal.of_real (b - a) :=
begin
  rw [edist_comm, edist_dist, real.dist_eq],
  congr,
  rw [abs_eq_self, sub_nonneg],
  exact ab,
end

lemma edist_triangle_eq_of_aligned {a b c : ℝ} (ab : a ≤ b) (bc : b ≤ c) :
  edist a b + edist b c = edist a c := sorry

lemma function.length_on_le_edist_of_monotone_on {f : α → ℝ} {s : set α} (hf : monotone_on f s) :
  ∀ {l : list α} (lm : l.pairwise (≤)) (ls : ∀ x ∈ l, x ∈ s) {x y : ℝ}
    (hxy : ∀ a ∈ l, x ≤ f a ∧  f a ≤ y), f.length_on l ≤ edist x y
| [] lm ls x y hxy := by simp [function.length_on_nil]
| [a] lm ls x y hxy := by simp [function.length_on_singleton]
| (a::b::l) lm ls x y hxy := by
  begin
    rw [list.pairwise_cons] at lm,
    have aabl : a ∈ a::b::l := or.inl rfl,
    have bbl : b ∈ b::l := or.inl rfl,
    have babl : b ∈ a::b::l := or.inr bbl,
    rw function.length_on_cons_cons,
    transitivity' edist (f a) (f b) + edist (f b) y,
    { refine add_le_add_left _ _,
      apply function.length_on_le_edist_of_monotone_on lm.right (λ c cl, ls _ (or.inr cl)),
      refine λ c cl, ⟨_,(hxy _ (or.inr cl)).right⟩,
      apply hf (ls _ babl) (ls _ (or.inr cl))
              (list.pairwise.rel_first_of_mem_cons is_refl.reflexive lm.right cl), },
    {  rw edist_triangle_eq_of_aligned (hf (ls _ aabl) (ls _ babl) (lm.left b bbl)) (hxy b babl).right,
      rw ←@edist_triangle_eq_of_aligned x (f a) y (hxy a aabl).left (hxy a aabl).right,
      exact self_le_add_left _ _, }
  end

which is not too bad I believe.

[Rémi Bottinelli]

Thanks a lot for the feedback, it's very helpful!

Junyan Xu said:

• I think you can just define length_on of a list E without mentioning the map f : α → E, and use docs#list.map when you have a list α.

Indeed, it didn't seem useful at first, but lately I've been thinking it's probably the right way forward (if continuing with lists at all); see code below.
The monotone_on.evariation_on_le lemma (and your proposal for solving it) makes such an approach more natural.

• If you use a pattern match definition of length_on, you can probably prove the three lemmas by rw length_on, so you won't need to write them out.

I had a pattern-match at first, but it built an ugly term (not at all just a double list.rec, and troubles later on).

• If you no longer want to replace the whole file bounded_variation.lean with your version based on lists, you still have the option of building APIs around the original definition, including defining length_on and showing the original evariation_on is the supremum of length_on.

Good point. If people are not convinced by the list approach, I think I'll do that.

• For monotone_on.evariation_on_le (which you stuck on), you could show by induction that the length_on of an ordered list ℝ is equal to the last element minus the first element; monotonicity guarantees orderedness via docs#list.pairwise.map.

One of the reasons I was stuck is the "last" and "first" element thing, which I kind of had trouble formulating in a nice and usable fashion.
Also, all we really need here is that the list has "metric triangle equalities" all the ways, so that the sum is just a big "triangle line" and the sum "squashes".

So, I tried defining length_on on lists with no function in sight here, and it's indeed much better.
Here is a snippet:

variables {E : Type*} [pseudo_emetric_space E]

namespace list

@[protected]
noncomputable def edist : list E → ennreal :=
list.rec 0
  (λ (a : E) (l : list E) (ih : ennreal),
      list.rec 0 (λ (b : E) (l : list E) (ih' : ennreal), edist a b + ih) l)

lemma edist_nil : edist (@list.nil E) = 0 := rfl
lemma edist_singleton (a : E) : edist [a] = 0 := rfl
lemma edist_cons_cons (a b : E) (l : list E) :
  edist (a::b::l) = edist a b + edist (b::l) := rfl

lemma edist_pair (a b : E) : edist [a, b] = edist a b :=
by simp only [edist_cons_cons, edist_singleton, add_zero]

lemma edist_eq_zip_sum :
  ∀ (l : list E), edist l = (list.zip_with (λ x y, edist x y) l l.tail).sum
| [] := by simp [edist_nil]
| [a] := by simp [edist_singleton]
| (a::b::l) := by simp [edist_cons_cons, edist_eq_zip_sum (b::l)]

/- [...] -/

lemma edist_of_triangles_eq :
  ∀ {l : list E} {a b : E} (hl : list.chain (λ x y, edist x y + edist y b = edist x b) a l),
    l.edist ≤ edist a b
| [] a b hl := by simp [edist_nil]
| [x] a b hl := by simp [edist_singleton]
| (x::y::l) a b hl :=
begin
  simp only [chain_cons] at hl,
  calc (x::y::l).edist
     = edist x y + (y::l).edist : edist_cons_cons _ _ _
  ...≤ edist x y + edist y b    : add_le_add_left (@edist_of_triangles_eq (y::l) y b _) _
  ...= edist x b                : hl.2.1
  ...≤ edist a x + edist x b    : self_le_add_left _ _
  ...= edist a b                : hl.1,
  constructor,
  simp only [edist_self, zero_add],
  exact hl.2.2,
end

-- mathlib?
lemma _root_.real.edist_triangle_eq_of_aligned {a b c : ℝ} (ab : a ≤ b) (bc : b ≤ c) :
  edist a b + edist b c = edist a c := sorry

lemma edist_of_monotone_le_real :
  ∀ {l : list ℝ} (hl : l.pairwise (≤)) {a b : ℝ} (hab : ∀ x ∈ l, a ≤ x ∧ x ≤ b),
  l.edist ≤ edist a b :=
begin
  rintro l hl a b hab,
  apply edist_of_triangles_eq,
  revert a b hl,
  induction l,
  { simp only [pairwise.nil, not_mem_nil, forall_const, chain.nil], },
  { rintro a b hl hab,
    simp only [pairwise_cons] at hl,
    exact chain.cons
      (_root_.real.edist_triangle_eq_of_aligned (hab l_hd (or.inl rfl)).left (hab l_hd (or.inl rfl)).right)
      (l_ih hl.right (λ (x : ℝ) (xl : x ∈ l_tl), ⟨hl.left x xl, (hab x (or.inr xl)).right⟩))},
end

and then the variation is defined as:

noncomputable def function.evariation_on {α : Type*} [linear_order α] (f : α → E) (s : set α) :=
⨆ l ∈ {l : list α | l.pairwise (≤) ∧ ∀ ⦃x⦄, x ∈ l → x ∈ s}, (l.map f).edist

I feel this definition of edist for lists has some value in its own; and then it's a good building block for the variation.
Can I get some kind of show of hands on whether merging list.edistsomewhere in topology.metric_space and then redefining evariation_on would be acceptable?

[Rémi Bottinelli]

Junyan Xu said:

• expand_bot/top_half could be defined using docs#set.proj_Icc, which is used to define docs#path.trans.

Indeed, I saw set.proj_Icc, but I don't think it's used to define path.trans (at least, it's not referred to directly in the code).
and actually, proj_Icc is not exactly what I need I believe.
I think the right way to do expand_bot/top_half would be to have

def shrink {a b : \R} (c d : Icc a b) : Icc a b -> Icc a b := sorry
def expand {a b : \R} (c d : Icc a b) : Icc a b -> Icc a b := sorry

that would shrink Icc a b to Icc c d and back, essentially, by fixing everything inside Icc c d and projecting the rest (the two maps would be monotone and inverse of each other on Icc c d).

• For idempotency of the path length metric, I think the proof doesn't invoke continuity the arc-length function; you can take a look at Burago-Burago-Ivanov 2001, Proposition 2.3.12. You do need that to_length_metric is continuous, so a path continuous in the path length metric is also continuous under the original topology. Then the fact that the length of the concatenation of finitely many paths is equal to the sum of the lengths should suffice to complete the proof. You may want to allow paths to take any (not necessarily closed) interval in ℝ as domains, as is done in [BBI]; they also have an axiomatic definition of length structures in 2.1.1 that would apply to lengths from a Riemannian metric, I think, and may be what you're trying to do with paths_with_lengths in your other topic.

For idempotency, I believed I needed continuity, but maybe I actually don't. I feel BBI are going a bit fast and loose, but you're probably right: I'll check it again (I had Bridson & Haefliger as another reference).
In any case, continuity of the arc-length is an important thing to have I believe.
As for path structures, and arbitrary intervals, that's a question I have: I started with path because it's already in mathlib, and so it's easier to base stuff on that primitive, and I'm not sure what exactly there is to gain by allowing arbitrary intervals when doing the length metric.
For now, I feel like it would probably be good to have "general" things in bounded_variation.lean, and, for length_metric, restrict stuff to path from the unit interval, so that we can reuse as much as possible.

As for the axiomatic definition in BBI, I thought it was probably too general to start with. Isn't it better to start with one working instance of path length, and, if need be, generalize it when time comes?

[Junyan Xu]

I think the main reason that proofs are bulky with the current definition of docs#evariation_on is the lack of API around the gadget consisting of a monotone function ℕ → α (with junk values) and a natural number, for example there's no definition of concatenation of two gadgets like this, while we readily have that for lists. Maybe we should make it a structure and develop APIs around it, and the main question is whether it's more convenient to work with this structure or with lists. If they both have their advantages, we could develop API to go from a list to this structure and back: there's a natural way to fill in the junk values, by repeating the last non-junk value, which is nice.

The setup of absolute continuity indicates that we should instead define the edist of a list of pairs, and apply it to docs#list.zip of l : list E with its tail in the setting of arclength. For absolute continuity I think we'd be dealing directly with a list (α × α) which pairwisely satisfies the relation r with r a b := a.2 ≤ b.1. (We could use this to do arclength as well, but it's probably more complicated.) (Is absolute continuity what this undergraduate item is about? It's also used in a general fundamental theorem of calculus and in the theory of quasiconformal maps, among others.)

Indeed, I saw set.proj_Icc, but I don't think it's used to define path.trans (at least, it's not referred to directly in the code).

Yeah it's not a direct reference. docs#path.trans is defined using docs#path.extend, which is defined using docs#set.Icc_extend, which is defined using docs#set.Icc_proj. set.Icc_proj 0 1 _ (2 * t) is the way to use the way to define extend_bot_half for example, see also here. The advantage of allowing arbitrary intervals as domains of paths seem to be to allow a separation between affine transformation of ℝ and concatenation of intervals, but I agree it's hard to assess whether it leads to a simplification without actually working on it.

[Junyan Xu]

You do need that to_length_metric is continuous, so a path continuous in the path length metric is also continuous under the original topology.

Oh sorry I got it backwards: from_length_metric is always continuous (Lipschitz constant 1) but not the other way. But the conclusion (a path continuous in the path length metric is also continuous under the original topology) is still true, because I made two mistakes in my mind and they cancel out :)

[Junyan Xu]

@Rémi Bottinelli
I tried my hands at it and have completed a proof of the crucial arclength continuity lemma at https://gist.github.com/alreadydone/a8e58edee5d9f1642d548da0c1640d34. Still using the original evariation_on definition. Happy new year!

[Junyan Xu]

Bridson-Haefliger invokes uniform continuity but you can see from my proof that it's not necessary. I even only assume continuity at one point from one side.

[Rémi Bottinelli]

Wow, impressive! Did you get the proof from BBI ?

[Junyan Xu]

No, the idea is still from BH.

[Rémi Bottinelli]

I don't really get what the first lemma is for: it looks at first sight like it's a defeq from the definition of variation

[Rémi Bottinelli]

(haven't run it yet, though)

[Rémi Bottinelli]

What's your takaway from this proof you did? Should I then stick with the N -> E-with-junk-values approach?

[Junyan Xu]

The first lemma allows you to only cosider summing over a nonempty range, with left endpoint of the interval as the first point, and with the first point less than the second point.

[Rémi Bottinelli]

Ah, indeed, thanks!

[Junyan Xu]

From my working on the proof, my assessment is that the current definition is nice enough to work with.

[Rémi Bottinelli]

I was thinking we should define the arclength like:

noncomputable def _root_.has_locally_bounded_variation_on.variation_on_from_to
 (hf : has_locally_bounded_variation_on f s) (a b : α) : real :=
f a ≤ b then (evariation_on f (s ∩ Icc a b)).to_real else - (evariation_on f (s ∩ Icc b a)).to_real

because I'm not entirely sure it's useful to deal with the generality of infinite length when proving interesting stuff about arclength.

[Rémi Bottinelli]

Junyan Xu said:

From my working on the proof, my assessment is that the current definition is nice enough to work with.

What about your comment on absolute continuity? I haven't had time to look at it closely yet.

[Sebastien Gouezel]

I went for ennreal-valued variation because it made the proofs much much easier: when you take a supremum over ennreal, you don't need to worry whether the thing you're maximizing over is nonempty and bounded above. In fact, my first try was real-valued, and it was way more painful. Once the API is there and you don't need to talk about suprema any more, switching to the real-valued version if it helps is definitely a possibility.

[Rémi Bottinelli]

(OK, I spent too much time trying to port it not to at least create a branch, so here goes in the eventuality it's ever useful https://github.com/leanprover-community/mathlib/compare/bottine/analysis.bounded_variation/using_lists?expand=1)

[Rémi Bottinelli]

@Sebastien Gouezel Ah, I didn't mean to say that the evariation shouldn't be ennreal-valued, but thinking that when talking specifically about continuity of the arc-length and stuff, it may be easier to only assume has_locally_bounded_variation_on and get a real value, as in the def I wrote above.

[Rémi Bottinelli]

And if I'm not mistaken, I can use exactly this definition to "simplify" refactor your proof of the fact that a real function with locally finite variation is a difference of monotone functions: simply extract your p in the proof, which is just this function.

[Junyan Xu]

Rémi Bottinelli said:

I was thinking we should define the arclength like:

noncomputable def _root_.has_locally_bounded_variation_on.variation_on_from_to
 (hf : has_locally_bounded_variation_on f s) (a b : α) : real :=
f a ≤ b then (evariation_on f (s ∩ Icc a b)).to_real else - (evariation_on f (s ∩ Icc b a)).to_real

because I'm not entirely sure it's useful to deal with the generality of infinite length when proving interesting stuff about arclength.

I think we shouldn't pass to real numbers too early, because we're gonna define the path length (pseudo_e)metric as the infimum of arclengths, and there could legitimately exist no (rectifiable) paths between two points, in which case we want the infimum to be infinity rather than 0 (a junk value), so we want ennreal/ereal rather than real. Using e(nn)real also allows you to take infimum over all (continuous) paths instead of only rectifiable paths, so one less condition to deal with.

[Rémi Bottinelli]

I agree with this, and in this case we can just use the variation itself.
What I meant was that in the context of talking about the continuity of the arc-length, or its monotonicity as a signed function, we might as well restrict our attention to when it is finite, no?

[Rémi Bottinelli]

As below:

namespace has_locally_bounded_variation_on

variables {f : α → E} {s : set α} (hf : has_locally_bounded_variation_on f s)

noncomputable def variation_from_to (hf : has_locally_bounded_variation_on f s) (a b : α) : real :=
if a ≤ b then (evariation_on f (s ∩ Icc a b)).to_real else
            - (evariation_on f (s ∩ Icc b a)).to_real

lemma variation_from_to_self (a : α) : hf.variation_from_to a a = 0 :=
begin
  dsimp only [variation_from_to],
  rw [if_pos (le_refl _), Icc_self, evariation_on.subsingleton, ennreal.zero_to_real],
  exact λ x hx y hy, hx.2.trans hy.2.symm,
end

lemma variation_from_to_nonneg_of_le {a b : α} (h : a ≤ b) : 0 ≤ hf.variation_from_to a b :=
by { dsimp only [variation_from_to], rw if_pos h, simp only [ennreal.to_real_nonneg], }

lemma variation_from_to_nonpos_of_ge {a b : α} (h : a ≥ b) : hf.variation_from_to a b ≤ 0 :=
begin
  dsimp only [variation_from_to],
  split_ifs,
  { cases le_antisymm h h_1,
    rw [Icc_self, evariation_on.subsingleton, ennreal.zero_to_real],
    exact λ x hx y hy, hx.2.trans hy.2.symm, },
  { simp only [right.neg_nonpos_iff, ennreal.to_real_nonneg], },
end

lemma variation_from_to_eq_of_le {a b : α} (h : a ≤ b) :
  hf.variation_from_to a b = (evariation_on f (s ∩ Icc a b)).to_real := if_pos h

lemma variation_from_to_eq_of_ge {a b : α} (h : a ≥ b) :
  hf.variation_from_to a b = - (evariation_on f (s ∩ Icc b a)).to_real :=
begin
  dsimp only [variation_from_to],
  split_ifs with h',
  { cases le_antisymm h h',
    rw [Icc_self, evariation_on.subsingleton, ennreal.zero_to_real],
    simp only [neg_zero],
    exact λ x hx y hy, hx.2.trans hy.2.symm, },
  { refl, }
end

lemma variation_from_to_eq_neg_swap (a b : α) :
  hf.variation_from_to a b = - hf.variation_from_to b a :=
begin
  rcases lt_trichotomy a b with ab|rfl|ba,
  { simp only [variation_from_to, if_pos ab.le, if_neg ab.not_le, neg_neg], },
  { simp only [variation_from_to_self, neg_zero], },
  { simp only [variation_from_to, if_pos ba.le, if_neg ba.not_le, neg_neg], },
end

lemma variation_from_to_add {a b c : α} (ha : a ∈ s) (hb : b ∈ s) (hc : c ∈ s) :
  hf.variation_from_to a b + hf.variation_from_to b c = hf.variation_from_to a c :=
begin
  rcases le_total a b with ab|ba;
  rcases le_total a c with ac|ca;
  rcases le_total b c with bc|cb,
  { rw [hf.variation_from_to_eq_of_le ab,
        hf.variation_from_to_eq_of_le bc,
        hf.variation_from_to_eq_of_le ac,
        ←ennreal.to_real_add (hf a b ha hb) (hf b c hb hc),
        evariation_on.Icc_add_Icc f ab bc hb], },
  { rw [hf.variation_from_to_eq_of_ge cb,
        hf.variation_from_to_eq_of_le ab,
        hf.variation_from_to_eq_of_le ac,
        ←sub_eq_add_neg,
        sub_eq_iff_eq_add,
        ←ennreal.to_real_add (hf a c ha hc) (hf c b hc hb),
        evariation_on.Icc_add_Icc f ac cb hc], },
  { cases le_antisymm (ab.trans bc) ca, cases le_antisymm ab bc,
    simp only [hf.variation_from_to_self, add_zero], },
  { rw [hf.variation_from_to_eq_of_le ab,
        hf.variation_from_to_eq_of_ge ca,
        hf.variation_from_to_eq_of_ge cb,
        ←sub_eq_add_neg],
    rw  sub_eq_iff_eq_add,
    rw add_comm,
    rw ←sub_eq_add_neg,
    symmetry,
    rw sub_eq_iff_eq_add,
    symmetry,
    rw ←ennreal.to_real_add (hf a b ha hb) (hf c a hc ha),
    rw add_comm,
    rw evariation_on.Icc_add_Icc f ca ab ha, },
  { sorry, },
  { cases le_antisymm (ba.trans ac) cb, cases le_antisymm ba ac,
    simp only [hf.variation_from_to_self, add_zero], },
  { sorry, },
  { sorry, },
end

-- Probably simply `monotone` holds with no reference to `s`, but then we can't use `variation_from_to_add` and it's
-- not very useful anyway ?
lemma variation_from_monotone_on {a : α} (as : a ∈ s) :
  monotone_on (hf.variation_from_to a) s :=
begin
  rintro b bs c cs bc,
  rw ←hf.variation_from_to_add as bs cs,
  nth_rewrite_lhs 0 ←add_zero (hf.variation_from_to a b),
  refine add_le_add_left (hf.variation_from_to_nonneg_of_le bc) _,
end

lemma variation_to_antitone_on {b : α} (bs : b ∈ s) :
  antitone_on (λ a, hf.variation_from_to a b) s :=
begin
  rintro a as c cs ac,
  simp,
  rw ←hf.variation_from_to_add as cs bs,
  nth_rewrite_lhs 0 ←zero_add (hf.variation_from_to c b),
  refine add_le_add_right (hf.variation_from_to_nonneg_of_le ac) _,
end

lemma sub_le_sub'' (a b c d : ℝ) : a - b ≤ c - d ↔ a - c ≤ b - d :=
begin
  have : c - d + b = b - d + c, by abel,
  simp only [tsub_le_iff_right, this],
end

lemma self_sub_variation_from_monotone_on {f : α → ℝ} {s : set α}
  (hf : has_locally_bounded_variation_on f s)
  {a : α} (as : a ∈ s) :
  monotone_on (λ x, hf.variation_from_to a x - f x) s :=
begin
  rintro b bs c cs bc,
  dsimp only,
  rw sub_le_sub'',
  calc f b - f c
     ≤ |f b - f c| : le_abs_self _
  ...= dist (f b)  (f c) : by simp
  ...= dist (f c)  (f b) : dist_comm _ _
  ...≤ hf.variation_from_to c b : by {rw hf.variation_from_to_eq_of_le bc}
  ...= hf.variation_from_to a b - hf.variation_from_to a c : sorry

end
-- TODO arc-length parameterization!

end has_locally_bounded_variation_on

[Rémi Bottinelli]

My goal here for now is just to use this to extract stuff from has_locally_bounded_variation_on.exists_monotone_on_sub_monotone_on

[Rémi Bottinelli]

By the way, for the length metric, I wonder how a more-but-not-too-general construction would look like.
Something like constructing a length metric for a family of sets of paths (with fixed domain the unit interval or not?) with a "reversal" and "concatenation" operation.
Say, have a way to at least be able to restrict to either continuous, or piecewise smooth paths would be a good goal?

[Junyan Xu]

You might want to check how APIs are built around docs#interval_integral, specifically docs#interval_integral.integral_add_adjacent_intervals (and it just occurred to me that Riemann integrals also have a similar setup involving partitions). I think we want to state additivity in greatest generality allowing infinite length, but certainly cases involving infinity minus infinity need to be excluded.

[Junyan Xu]

This is the definition on BBI of a length structure; is it too general?
image.png
image.png

[Junyan Xu]

In the above, paths are still parametrized by an interval in ℝ, but maybe a more convenient approach in Lean would be making path a structure consisting of a continuous function ℝ → E and two points start end : ℝ (not sure if it's necessary to enforce start ≤ end). It's only necessary to require the path to be continuous on the closed interval, but it's not less general to require it to be continuous on ℝ, because we have docs#continuous.Icc_extend'. I'm planning to define the path length metric as the infimum over such paths; it's nice to get rid of the 2 * involved in docs#path.trans.

On a second thought, maybe we can still use C(set.Icc start end, E) in the structure, but provide a coercion to ℝ → E via docs#set.Icc_extend`.

[Junyan Xu]

Even in homotopy theory, paths indexed by variable intervals are used: https://en.wikipedia.org/wiki/Path_space_fibration#Moore's_path_space

[Rémi Bottinelli]

Junyan Xu said:

This is the definition on BBI of a length structure; is it too general?
image.png
image.png

Two concerns for me:

• Isn't there a point to be made for "approximate concatenation": instead of stating that the concatenation of paths in the family must also be a family, something like: Given two paths in the family and an eps, there exists a "concatenated" path of length less than eps plus the sum?
  This would allow, say, talking about smooth paths, instead of piecewise smooth ones. But maybe it's a stupid idea?

• It would be nice to have a definition that covers the path metric on graphs, whene there is no such thing as a C(Icc 0 1, X) since X is just a simple graph, but that's mybe too general.

[Rémi Bottinelli]

Junyan Xu said:

In the above, paths are still parametrized by an interval in ℝ, but maybe a more convenient approach in Lean would be making path a structure consisting of a continuous function ℝ → E and two points start end : ℝ (not sure if it's necessary to enforce start ≤ end). It's only necessary to require the path to be continuous on the closed interval, but it's not less general to require it to be continuous on ℝ, because we have docs#continuous.Icc_extend'. I'm planning to define the path length metric as the infimum over such paths; it's nice to get rid of the 2 * involved in docs#path.trans.

On a second thought, maybe we can still use C(set.Icc start end, E) in the structure, but provide a coercion to ℝ → E via docs#set.Icc_extend`.

I feel it's maybe easier indeed to just let paths be maps from the reals, even though it kind of feel hackish. This way, restricting to subintervals and such doesn't require any coercion.

[Rémi Bottinelli]

I made a PR with the definition I mentionned here: https://github.com/leanprover-community/mathlib/pull/18040

[Junyan Xu]

Rémi Bottinelli said:

Junyan Xu said:

This is the definition on BBI of a length structure; is it too general?

Two concerns for me:
...

Oh sorry I misread, you want a more-but-not-too-general construction, not a less general one. Indeed I think it's probably pointless to avoid piecewise-ness in the smooth setting. For simple graphs, I think you can take its "geometric realization" that adds edges of appropriate lengths; the edges can't pop out from nowhere just from the construction of the path length metric. Without adding the edges, even if you get a metric on the vertices, this is not an intrinsic metric / length space, as there are no paths between the vertices. (I think the BBI definition is meant to yield a length space via the path length metric construction.)

[Rémi Bottinelli]

For simple graphs, I think you can take its "geometric realization" that adds edges of appropriate lengths; the edges can't pop out from nowhere just from the construction of the path length metric. Without adding the edges, even if you get a metric on the vertices, this is not an intrinsic metric / length space, as there are no paths between the vertices. (I think the BBI definition is meant to yield a length space via the path length metric construction.)

Well, the point is that maybe, as in this other thread I made that you linked to, there should be some generic infrastructure to allow constructing a metric out of some abstract notion of "paths", that doesn't have to be actual topological paths. I don't really believe constructing metric spaces out of some "path length" idea should need to invoke topology. But that's probably too far out.

[Rémi Bottinelli]

@Junyan Xu

I'm planning to define the path length metric as the infimum over such paths;

Can you expand some on these plans (so that I don't spend too much time working on redundant things)?

[Rémi Bottinelli]

Ah, it seems that BBI do exactly the same proof as you did for continuity of the arclength. Screenshot-from-2023-01-02-10-41-34.png

[Rémi Bottinelli]

I tried defining the arc-length parameterization again, using the definitions in my PR:

/-
Copyright (c) 2022 Sébastien Gouëzel. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sébastien Gouëzel
-/
import measure_theory.measure.lebesgue
import analysis.calculus.monotone
import data.set.function
import .bounded_variation


open_locale big_operators nnreal ennreal
open set measure_theory
open classical
local attribute [instance, priority 10] prop_decidable


variables {α β : Type*} [linear_order α] [linear_order β]
{E F : Type*} [pseudo_emetric_space E] [pseudo_emetric_space F]
{V : Type*} [normed_add_comm_group V] [normed_space ℝ V] [finite_dimensional ℝ V]

namespace evariation_on

lemma edist_congr_left {a b c : E} (hab : edist a b = 0) : edist a c = edist b c :=
begin
  apply le_antisymm,
  rw [←zero_add (edist b c), ←hab],
  apply edist_triangle,
  rw edist_comm at hab,
  rw [←zero_add (edist a c), ←hab],
  apply edist_triangle,
end
lemma edist_congr_right {a b c : E} (hab : edist a b = 0) : edist c a = edist c b :=
by { rw [edist_comm c a, edist_comm c b], apply edist_congr_left hab,  }

lemma eq_of_edist_zero_on {f f' : α → E} {s : set α} (h : ∀ ⦃x⦄, x ∈ s → edist (f x) (f' x) = 0) :
  evariation_on f s = evariation_on f' s :=
begin
  dsimp only [evariation_on],
  congr' 1 with p : 1,
  congr' 1 with i : 1,
  rw edist_congr_left (h $ p.snd.prop.2 (i+1)),
  rw edist_congr_right (h $ p.snd.prop.2 i),
end

end evariation_on

namespace has_locally_bounded_variation_on

variables {f : α → E} {s : set α} (hf : has_locally_bounded_variation_on f s)


noncomputable def arc_length_parameterization_or {a : α} (as : a ∈ s) (e : E) : ℝ → E :=
λ x, if h : ∃ b, b ∈ s ∧ x = hf.variation_from_to a b then f h.some else e

/--
In a metric space, precomposing arc-length parameterization with variation yields the original
map.
-/
lemma arc_length_parameterization_edist_zero {a : α} (as : a ∈ s) {b : α} (bs : b ∈ s) (e : E) :
  edist (f b) (hf.arc_length_parameterization_or as e (hf.variation_from_to a b)) = 0 :=
begin
  dsimp only [arc_length_parameterization_or],

  let cc : ∃ (b : α), b ∈ s ∧ hf.variation_from_to a b = hf.variation_from_to a b := ⟨b, bs, rfl⟩,
  rw [dif_pos cc],
  /-let c := cc.some,
  let cs := cc.some_spec.1,
  let cb := cc.some_spec.2,
  rw [←hf.variation_from_to_add as bs cs, add_right_eq_self] at cb,
  rw [←ennreal.bot_eq_zero, eq_bot_iff, ennreal.bot_eq_zero],
  by_cases h : b ≤ c,
  { rw [←ennreal.of_real_zero, ←cb, hf.variation_from_to_eq_of_le h,
        ennreal.of_real_to_real (hf b c bs cs)],
    apply evariation_on.edist_le f,
    exact ⟨bs, ⟨le_refl _, h⟩⟩,
    exact ⟨cs, ⟨h, le_refl _⟩⟩, },
  { replace h : c ≤ b := (lt_of_not_le h).le,
    rw [hf.variation_from_to_eq_neg_swap, neg_eq_zero] at cb,
    rw [edist_comm, ←ennreal.of_real_zero, ←cb, hf.variation_from_to_eq_of_le h,
        ennreal.of_real_to_real (hf c b cs bs)],
    apply evariation_on.edist_le f,
    exact ⟨cs, ⟨le_refl _, h⟩⟩,
    exact ⟨bs, ⟨h, le_refl _⟩⟩, }-/
end

end has_locally_bounded_variation_on

but get an error at the simp [dif_pos cc] line. I believe there is some instance trouble going on here?

[Rémi Bottinelli]

At first I defined the arc-length parameterization only on s.image $ hf.variation_from_to a, but then you have to coerce a lot to be able to piece the different functions together.

[Rémi Bottinelli]

@Junyan Xu Concerning the lemma in your proof of continuity. Would it make sense to generalize it to something like:

lemma evariation_eq_bsupr (f : α → E) {s : set α} (F : set $ ℕ → α)
  (hF : ∀ (ε : ℝ≥0∞), ε > 0 → ∀ p : ℕ × {u : ℕ → α // monotone u ∧ ∀ i, u i ∈ s},
          ∃ q : ℕ × {u : ℕ → α // monotone u ∧ ∀ i, u i ∈ s},
          (∑ i in finset.range q.1, edist (f ((q.2 : ℕ → α) (i+1))) (f ((q.2 : ℕ → α) i))) >
          (∑ i in finset.range p.1, edist (f ((p.2 : ℕ → α) (i+1))) (f ((p.2 : ℕ → α) i))) - ε) :
  evariation_on f s = ⨆ (p : ℕ × {u : ℕ → α // monotone u ∧ ∀ i, u i ∈ s ∧ u ∈ F}),
  ∑ i in finset.range p.1, edist (f ((p.2 : ℕ → α) (i+1))) (f ((p.2 : ℕ → α) i)) := sorry

[Rémi Bottinelli]

As in you may want to say that the supr is the same as when restricting only to us that are:

• strictly monotonous
• have a range containing the range of a given fixed u
• have endpoints the max and min of s
• …

[Rémi Bottinelli]

Well, the lemma itself is not specific to evariation, but I wonder if there can be some infrastructure in place to facilitate such statements

[Junyan Xu]

there should be some generic infrastructure to allow constructing a metric out of some abstract notion of "paths", that doesn't have to be actual topological paths.

Yeah, continuity and intervals are not involved there, and I guess we can worry about them later :)

Can you expand some on these plans (so that I don't spend too much time working on redundant things)?

I was distracted by other tasks and haven't written any code to redefine the path length metric yet, and I also haven't got time to review your #18040 or diagnose your arclength parametrization code (which depends on #18040) either.

But at least I've just now completed the proof that the arclength function is continuous on the closed interval, using #18037 to transfer right continuity to left continuity: https://gist.github.com/alreadydone/a8e58edee5d9f1642d548da0c1640d34

lemma evariation_eq_bsupr (f : α → E) {s : set α} (F : set $ ℕ → α)

I haven't been able to decipher the statement yet; will think about it later!

[Rémi Bottinelli]

In the meantime, I've tried showing 1.20.(7) of Bridson-Haefliger, but get stuck on dealing with coercions:

example {ι : Type*} {F : ι → α → E} {f : α → E} {p : filter ι} {s : set α}
  (hF : tendsto_uniformly_on F f p s) (hf : has_bounded_variation_on f s) :
  ∀ (ε : ℝ≥0), ε ≠ 0 → (∀ᶠ (n : ι) in p, evariation_on f s ≤ evariation_on (F n) s + ε) :=
begin
  by_cases hs : s.nonempty, swap,
  { rw [evariation_on.subsingleton f],
    simp only [zero_le', filter.eventually_true, implies_true_iff],
    exact λ x hx y hy, (hs ⟨x,hx⟩).elim, },
  rintro ε hε,
  rw emetric.tendsto_uniformly_on_iff at hF,
  obtain ⟨⟨n,⟨u,um,us⟩⟩,hlt⟩ := eps_approx hs hf ((ε : ℝ≥0∞)/2)
    (by {simp only [hε, ne.def, ennreal.div_zero_iff, ennreal.coe_eq_zero, ennreal.bit0_eq_top_iff,
                    ennreal.one_ne_top, or_self, not_false_iff]}),
  specialize hF ((ε : ℝ≥0∞)/(4*n))
    (by {simp only [hε, gt_iff_lt, ennreal.div_pos_iff, ne.def, ennreal.coe_eq_zero, not_false_iff,
                    with_top.mul_eq_top_iff, ennreal.nat_ne_top, and_false, ennreal.bit0_eq_top_iff,
                    ennreal.one_ne_top, false_and, or_self, and_self],}),
  refine (hF.mono $ λ i hi, hlt.le.trans (le_trans _ (add_le_add_right (sum_le (F i) n um us) ε))),
  clear hlt hF,
  have : (ε : ℝ≥0∞) = (↑ε/2) + (↑ε/2), simp only [ennreal.add_halves],
  nth_rewrite_rhs 0 this, rw ←add_assoc,
  refine add_le_add_right _ _,
  calc ∑ (j : ℕ) in finset.range n, edist (f (u j.succ)) (f (u j))
     ≤ ∑ (j : ℕ) in finset.range n, (edist (F i (u j.succ)) (F i (u j)) + ↑ε/(2*n)) : by
  begin
    refine finset.sum_le_sum (λ j jn, _),
    apply (edist_triangle4 _ (F i (u j.succ)) (F i (u j)) _).trans,
    have : (ε : ℝ≥0∞)/(2*↑n) = ε/(4*n) + ε/(4*n), by { rw ←ennreal.add_div, rw ←two_mul, sorry, },
    rw [this, ←add_assoc],
    refine add_le_add _ _,
    { nth_rewrite_lhs 0 add_comm, refine add_le_add_left ((hi (u j.succ) (us j.succ)).le) _, },
    { rw edist_comm, exact (hi (u j) (us j)).le,  }
  end
  ...= ∑ (j : ℕ) in finset.range n, edist (F i (u j.succ)) (F i (u j)) + n*(↑ε/(2*n)) :
  by  simp only [finset.sum_add_distrib, finset.sum_const, finset.card_range, nsmul_eq_mul]
  ...≤ ∑ (j : ℕ) in finset.range n, edist (F i (u j.succ)) (F i (u j)) + (↑ε/2) : by
  begin
    refine add_le_add_left _ _,
    sorry,
  end
end

[Junyan Xu]

Should we state it with docs#lower_semicontinuous (as on BBI)?

[Rémi Bottinelli]

Junyan Xu said:

Should we state it with docs#lower_semicontinuous (as on BBI)?

Ah, yes, let me try (I don't (yet?) know my way around topology in generalmathlib ).

[Rémi Bottinelli]

How do I tell lean I want the uniform convergence topology?

lemma evariation_on_lower_continuous' {f : α → E} {s : set α} (hf : has_bounded_variation_on f s) :
  lower_semicontinuous_at (λ g, evariation_on g s) f :=
begin
  rintro v hv,
end

[Rémi Bottinelli]

Mmh, we actually probably don't even need to have has_bounded_variation_on f s as an assumption

[Rémi Bottinelli]

I'll try and adapt the proof tomorrow

[Junyan Xu]

How do I tell lean I want the uniform convergence topology?

There is docs#uniform_fun, but maybe you want docs#uniform_on_fun (with 𝔖 := {s})

[Junyan Xu]

I think the commonality between continuous vs. graph path length metric is that you have a set L x y of ennreals (lengths) between any two points/vertices x and y, satisfying 0 ∈ L x x, L x y = L y x, and L x y + L y z ⊆ L x z (pointwise addition) (or you may relax this to ∀ l ∈ L x y + L y z, ∃ l' ≤ l, l' ∈ L x z).
It's convenient to work with ennreal since we can assign weight 1 to edges and infinite weight to non-edges, so we can consider all maps fin n → G.verts (or ℕ or ℤ as the domain) rather than only walks.

A crucial difference between the two is that, in the continuous case we start from a emetric, while the weights on (non-)edges in a graph don't satisfy triangle inequality. So I'm thinking we should probably generalize docs#evariation from pseudo_emetric_space to has_edist whenever possible, and we can show that when applied to a map f : ℤ → E, arclength f m n is simply the sum over the interval [m,n) of all adjacent edists. Notice that in the continuous case the resulting path metric is bounded below by the original, while in the graph/discrete case it's bounded above by the original (because there is no continuity restriction; even if you impose it it would be vacuous since ℤ is discrete).

Here's my tentative definition of the path length metric that covers both continuous and discrete cases:
https://gist.github.com/alreadydone/a8e58edee5d9f1642d548da0c1640d34#file-continuous_arclength-lean-L15-L31

[Rémi Bottinelli]

OK, I've got the rectifiability assumption out; remains to rewrite it in terms of continuity.

lemma eps_approx' {f : α → E} {s : set α} (hs: s.nonempty) (v : ℝ≥0∞) (h : v < evariation_on f s) :
  ∃ (p : ℕ × {u : ℕ → α // monotone u ∧ ∀ i, u i ∈ s}),
    v < ∑ i in finset.range p.1, edist (f ((p.2 : ℕ → α) (i+1))) (f ((p.2 : ℕ → α) i))  :=
begin
  by_contra' hn,
  apply (lt_of_lt_of_le h (supr_le (λ x, hn x))).ne rfl,
end

lemma evariation_on_lower_continuous {ι : Type*} {F : ι → α → E} {p : filter ι}
  {f : α → E} {s : set α} (hF : tendsto_uniformly_on F f p s) :
  ∀ (v : ℝ≥0∞), v < evariation_on f s → (∀ᶠ (n : ι) in p, v < evariation_on (F n) s) :=
begin
  by_cases hs : s.nonempty, swap,
  { simp only [evariation_on.subsingleton f (λ x hx _ _, (hs ⟨x,hx⟩).elim)],
    simp only [implies_true_iff, not_lt_zero, is_empty.forall_iff], },
  rintro v hv,
  rw emetric.tendsto_uniformly_on_iff at hF,
  obtain ⟨v',vv',v'var⟩ := exists_between hv,
  obtain ⟨⟨n,⟨u,um,us⟩⟩,hlt⟩ := eps_approx' hs v' v'var,
  let ε := (v' - v)/(2*n),
  have hvp : 0 < v' - v, by { simp only [vv', tsub_pos_iff_lt],},
  have : v' - v ≠ ⊤ := ennreal.sub_ne_top (ne_of_lt (lt_of_lt_of_le v'var le_top)),
  have : v' = v + (v' - v) := (add_tsub_cancel_of_le vv'.le).symm,
  have hε : 0 < ε, by
  { dsimp [ε],
    rw ennreal.div_pos_iff,
    refine ⟨hvp.ne.symm, mul_ne_top two_ne_top (nat_ne_top n)⟩, },
  specialize hF ε hε,
  apply hF.mono, clear hF,
  rintro i hi,
  suffices h : v' < evariation_on (F i) s + (v' - v),
  { nth_rewrite 0 this at h,
    rw ←ennreal.add_lt_add_iff_right ‹v'-v≠⊤›,
    exact h, },
  calc v'
     < ∑ (j : ℕ) in finset.range n, edist (f (u j.succ)) (f (u j))  : hlt
  ...≤ ∑ (j : ℕ) in finset.range n, (edist (F i (u j.succ)) (F i (u j)) + 2*ε) : by
  begin
    refine finset.sum_le_sum (λ j jn, (edist_triangle4 _ (F i (u j.succ)) (F i (u j)) _).trans _),
    rw [two_mul, ←add_assoc _ ε ε, add_comm _ ε, ←add_assoc],
    refine add_le_add (add_le_add_right (hi (u j.succ) (us j.succ)).le _) _,
    rw edist_comm, exact (hi (u j) (us j)).le,
  end
  ...= ∑ (j : ℕ) in finset.range n, edist (F i (u j.succ)) (F i (u j)) + 2*n*ε :
  begin
    simp only [finset.sum_add_distrib, finset.sum_const, finset.card_range, nsmul_eq_mul,
               ←mul_assoc, mul_comm _ (2:ℝ≥0∞)],
  end
  ...≤ ∑ (j : ℕ) in finset.range n, edist (F i (u j.succ)) (F i (u j)) + (v' - v) :
  begin
    refine add_le_add_left (mul_div_le) _,
  end
  ...≤ evariation_on (F i) s  + (v' - v) : add_le_add_right (sum_le (F i) _ um us) (v' - v)
end

[Junyan Xu]

Sorry, I realized the idea in my last post doesn't work: if ab and bc are edges but ac is not, then the map 0->a, 1->b, 2->c would have unbounded variation between 0 and 2 (because the variation is a supremum, and infinity is achieved at the monotone map 0->0, 1->2 (which omits b)). So it doesn't make sense to generalize evariation from pseudo_emetric_space to has_edist.

[Rémi Bottinelli]

I expect this can be golfed to one line (note that I'm using the "original" lower semicontinuity lemma) :)

lemma evariation_on_lower_continuous' {s : set α} :
  lower_semicontinuous (λ f : uniform_on_fun α E {s}, evariation_on f s) :=
begin
  rintro f v hv,
  apply evariation_on_lower_continuous,
  { suffices : ∀ t ∈ {s}, tendsto_uniformly_on (λ (n : uniform_on_fun α E {s}), n) f (nhds f) t,
    { apply this s (set.mem_singleton s), },
    rw ←uniform_on_fun.tendsto_iff_tendsto_uniformly_on,
    exact filter.tendsto_id, },
  { exact hv, },
end

I'll probably clean it up some more and open a PR

[Rémi Bottinelli]

@Junyan Xu Your proposal in terms of ennreals (L x y) differs from my "paths with length stub" in that you simply forget about the original paths and only look at the set of lengths, right?

[Rémi Bottinelli]

for your path_btw, you don't care about generalizing to graphs or other things, right (just trying to know the context)?

[Junyan Xu]

Your proposal in terms of ennreals (L x y) differs from my "paths with length stub" in that you simply forget about the original paths and only look at the set of lengths, right?

Probably, I don't remember all details in your code. Maybe we want to keep the indexing type as we normally do in type theory, or maybe not.

[Rémi Bottinelli]

If we're staying purely in the topological realm, would it make sense to have a path type that would then be extended by the already present path ? (In order to keep some kind of coherent hierarchy)

[Junyan Xu]

for your path_btw, you don't care about generalizing to graphs or other things, right (just trying to know the context)?

I attempted to cover the graph case but it doesn't actually work as I just found out. I should probably stick with real rather than M in my current code ...

[Rémi Bottinelli]

If path x y is a function from R to the space, then equality becomes kind of meaningless, no?

[Rémi Bottinelli]

I think I still prefer having paths with the correct domain

[Rémi Bottinelli]

Well, you could add

(constant_below : \forall m ≤ source, path m = path source)
(constant_above : \forall m ≥ target, path m = path target)

[Rémi Bottinelli]

https://github.com/leanprover-community/mathlib/pull/18058

[Yaël Dillies]

Junyan Xu said:

Sorry, I realized the idea in my last post doesn't work: if ab and bc are edges but ac is not, then the map 0->a, 1->b, 2->c would have unbounded variation between 0 and 2 (because the variation is a supremum, and infinity is achieved at the monotone map 0->0, 1->2 (which omits b)). So it doesn't make sense to generalize evariation from pseudo_emetric_space to has_edist.

Is that not fixed by redefining the evariation as the infimum over all paths of the supremum of <whatever is in the current definition>?

[Rémi Bottinelli]

@Yaël Dillies do you mean defining the evariation for paths in graphs as the supremum over the us such that consecutive values of u are adjacent or equal, say?

[Rémi Bottinelli]

I think the only common theme between the graph and metric cases is that we have a type of "Paths between _ and _" for any pair of points, with associated lengths satisfying some reflexivity, symmetry, and transitivity properties. Extending evariation to graph-theoretical walks seems probably pointless.

[Rémi Bottinelli]

Also, if we go as far as defining such a general framework, it would probably be helpful to be able to allow different weighs on the edges of a simple_graph, when defining the metric.

[Rémi Bottinelli]

@Junyan Xu, also, I think(le : source ≤ target) is better than (lt : source < target): Then we can define path.refl as having domain Icc 0 0 and concatenation with path.refl is almost defeq equal to the original path.

[Rémi Bottinelli]

Also, is there much point to have an arbitrary start value?

[Rémi Bottinelli]

What about this?

import data.real.ennreal
import data.real.nnreal
import topology.metric_space.emetric_space

noncomputable theory

open_locale classical nnreal ennreal

open emetric ennreal
open emetric nnreal

section path_emetric

variables  {E : Type*} [pseudo_emetric_space E]

structure path_btw (l : ℝ≥0) (x y : E) :=
(path : ℝ → E)
(map_source : ∀ ⦃t⦄, t ≤ 0 → path t = x)
(map_target : ∀ ⦃t⦄, l ≤ t → path t = y)
-- (continuous : continuous_on path (set.Icc 0 l))

def path_btw.trans {l l'} {x y z : E} (p : path_btw l x y) (p' : path_btw l' y z) : path_btw (l+l') x z :=
{ path := λ t, if t ≤ l then p.path t else p'.path (l + t),
  map_source := sorry,
  map_target := sorry, }

def path_btw.symm {l} {x y : E} (p : path_btw l x y) : path_btw l y x :=
{ path := λ t, p.path (l-t),
  map_source := sorry,
  map_target := sorry, }


end path_emetric

[Sebastien Gouezel]

Are you aware of docs#path, which is already used in mathlib to construct the fundamental group?

[Sebastien Gouezel]

It already has nice API, like docs#path.extend, which corresponds to your extended version to the whole real line.

[Rémi Bottinelli]

I am. I don't believe I mind working with docs#path, but you get into a bit of trouble because of reparameterization, and not having a fixed domain (the entire real line) to work on: instead having to deal with compositions and subtypes and stuff. Or at least that's what I believe the motivation for a different type for path is (@Junyan Xu )?

[Sebastien Gouezel]

Normally, that's the role of the API around docs#path. If there are things that are painful to do, it might mean that the API is lacking, and it would probably be worth extending the API to make things smoother, instead of trying to come up with a different implementation. Ideally, proving that the evariation of a composition of paths is bounded by the sum of the evariations should be pretty smooth -- if it's not, we definitely need to improve something!

[Rémi Bottinelli]

I've got to go, but in the meantime: I'm restating lower semicontinuity:

lemma lower_continuous_aux {ι : Type*} {F : ι → α → E} {p : filter ι}
  {f : α → E} {s : set α} (Ffs : ∀ x ∈ s, p.tendsto (λ i, F i x) (nhds (f x)))
  {v : ℝ≥0∞} (hv v < evariation_on f s) : (∀ᶠ (n : ι) in p, v < evariation_on (F n) s) :=

but couldn't seem to find something like tendsto_on for my Ffs assumption. Where should I look?

[Sebastien Gouezel]

I think your current formulation is fine. We have the topology of pointwise convergence on the whole space (that's the default topology on function spaces), but I don't think we have ever needed to spell out pointwise convergence on a subset.

[Rémi Bottinelli]

The closest would be uniform on the family of singletons of elements of s I guess.

[Sebastien Gouezel]

Aside: please don't write p.tendsto f q, use instead tendsto f p q. It's closer to the intended mathematical content.

[Rémi Bottinelli]

So, should I still have the non-aux statement, e.g. like :

lemma lower_continuous {s : set α} :
  lower_semicontinuous (λ f : uniform_on_fun α E (s.image $ λ x, {x}), evariation_on f s) := sorry

or just have the "manual" statement that doesn't explicitely use lower_semicontinuous ?

[Sebastien Gouezel]

I'd write the statement with lower_continuous for the uniform convergence topology, with a docstring explaining the situation, and the manual statement as you did above.

[Sebastien Gouezel]

Note that the proof of the manual statement can be done without any epsilon: just say that the sum for F n converges to the sum for f, and the latter is > v, so the former is eventually > v (I'm trying to spare you a lot of useless pain here :-)

[Rémi Bottinelli]

Thanks, this filter-based infrastructure is very neat but I need a bit of time to get acquainted.

[Rémi Bottinelli]

(lower semicontinuity is continuity relative to the Iio i.e. ]x,\infty[ topology, right?)

[Rémi Bottinelli]

I would think it's better to stick to neighborhoods instead of having the indexed family as I did before, no ?:

lemma lower_continuous_aux' {ι : Type*}
  {f : α → E} {s : set α} (Ffs : ∀ x ∈ s, filter.tendsto (λ (g : α → E), g x) (nhds f) (nhds (f x)))
  {v : ℝ≥0∞} (hv : v < evariation_on f s) : (∀ᶠ g in nhds f, v < evariation_on g s) :=
begin
  obtain ⟨⟨n, ⟨u, um, us⟩⟩, hlt⟩ := lt_supr_iff.mp hv,
  dsimp only at hlt,
  have : filter.tendsto
    (λ (g : α → E), ∑ (i : ℕ) in finset.range n, edist (g (u (i + 1))) (g (u i))) (nhds f)
    (nhds (∑ (i : ℕ) in finset.range n, edist (f (u (i + 1))) (f (u i)))), by
  { sorry, },
  replace this := (eventually_gt_of_tendsto_gt hlt this),
  dsimp only at this,
  refine this.mono (λ g h, lt_of_lt_of_le h (sum_le g n um us)),
end

[Sebastien Gouezel]

No, please use a general filter. Here you are using the filter of pointwise convergence on the whole space, which has nothing to do with the question at hand (in your snippet, your assumption Ffs is true by definition, by the way!)

I know filters look strange at first, but they are really the right level of generality. If you like, you can write your proof first for F : nat → α → E assuming that, for all x in s, then F n x tends to f x as n tends to infinity (i.e., using the at_top filter on nat). And then generalize nat to a general type, at_top to a general filter, and see that it doesn't make the slightest difference.

[Rémi Bottinelli]

Sebastien Gouezel said:

No, please use a general filter. Here you are using the filter of pointwise convergence on the whole space, which has nothing to do with the question at hand (in your snippet, your assumption Ffs is true by definition, by the way!)

Can you expand on that? I was thinking along the lines that the original way was proving stuff about filters with one level of indirection to many.

[Rémi Bottinelli]

As in, given the topological spaces A B and f : A -> B, instead of showing simply that the pullback of a neighborhood filter in nhds (f x) is contained in neigborhood filter nhds x, it showed that given a third map F : I -> A and a filter on I such that the pullback of nhds (F) is contained in the filter, the composite f \circ F also behave that way, which is equivalent to the simpler form by just taking F be the identity.

[Rémi Bottinelli]

I believe modulo mistakes and the problem of taking the right topology, what I wrote above is right. Does the problem then arise from this difference in topologies, or am I mistaken somewhere else?

[Rémi Bottinelli]

Ah, yes, I think that's it: because with the snippet above, nhds f takes pointwise topology, and then the Ffs is really just a restatement of that topology.

[Rémi Bottinelli]

But say I wasn't dealing with two different topologies, then should the form in the snippet be preferred?

[Sebastien Gouezel]

Indeed, the problem is that nhds f uses the global pointwise convergence topology, not pointwise convergence topology on s. If you had the right topology, then yes the two statements (with a general filter or with nhds f) would indeed be equivalent. And I'd probably state the lemma as you did, i.e., without Ffs and with a conclusion ∀ᶠ g in nhds f, v < evariation_on g s.

Note however that, often, for applications, the version with a general filter is more convenient to use. This is explained in the library note https://leanprover-community.github.io/mathlib_docs/notes.html#continuity%20lemma%20statement (for continuity, but the same goes for limits). So in many cases, I give both versions as separate lemmas, deducing one from the other.

[Rémi Bottinelli]

Thanks! I think I need to familiarize myself some more with the API: are there a few pedagogically useful files you recommend? Beside I guess filter and topological_space

[Rémi Bottinelli]

(I know "nets"/generalized sequences/directed sets already, but the filter approach is kind of backwards in my head, it gets confusing!)

[Rémi Bottinelli]

OK, not there yet but looking better (I mean, the statements typecheck at least :) ):

lemma lower_continuous_aux {ι : Type*} {F : ι → α → E} {p : filter ι}
  {f : α → E} {s : set α} (Ffs : ∀ x ∈ s, filter.tendsto (λ i, F i x) p (nhds (f x)))
  {v : ℝ≥0∞} (hv : v < evariation_on f s) : (∀ᶠ (n : ι) in p, v < evariation_on (F n) s) := sorry

lemma lower_semicontinuous {s : set α} :
  lower_semicontinuous (λ f : uniform_on_fun α E (s.image $ λ x, {x}), evariation_on f s) :=
begin
  rintro f,
  apply @lower_continuous_aux _ _ _ _ (uniform_on_fun α E (s.image singleton)) id (nhds f) f s _,
  have : filter.tendsto id (nhds f) (nhds f) := filter.tendsto_id,
  simp only [uniform_on_fun.tendsto_iff_tendsto_uniformly_on, mem_image, forall_exists_index,
             and_imp, forall_apply_eq_imp_iff₂,
             tendsto_uniformly_on_singleton_iff_tendsto] at this,
  exact this,
end

[Rémi Bottinelli]

When trying to make progress on lower_continuous_aux I get a strange instance problem:

At the let := @emetric.… line,

lemma lower_continuous_aux {ι : Type*} {F : ι → α → E} {p : filter ι}
  {f : α → E} {s : set α} (Ffs : ∀ x ∈ s, filter.tendsto (λ i, F i x) p (nhds (f x)))
  {v : ℝ≥0∞} (hv : v < evariation_on f s) : (∀ᶠ (n : ι) in p, v < evariation_on (F n) s) :=
begin
  obtain ⟨⟨n, ⟨u, um, us⟩⟩, hlt⟩ := lt_supr_iff.mp hv,
  dsimp only at hlt,
  have :
    filter.tendsto (λ j, ∑ (i : ℕ) in finset.range n, edist (F j (u (i + 1))) (F j (u i))) p
    (nhds (∑ (i : ℕ) in finset.range n, edist (f (u (i + 1))) (f (u i)))), by
  { let := @emetric.tendsto_nhds ℝ≥0∞ ι _ p (λ j, ∑ (i : ℕ) in finset.range n, edist (F j (u (i + 1))) (F j (u i))) (∑ (i : ℕ) in finset.range n, edist (f (u (i + 1))) (f (u i))),
    sorry,
   },
  exact (eventually_gt_of_tendsto_gt hlt this).mono
    (λ i h, lt_of_lt_of_le h (sum_le (F i) n um us)),
end

I get:

failed to synthesize type class instance for
α : Type u_1,
_inst_1 : linear_order α,
E : Type u_3,
_inst_3 : pseudo_emetric_space E,
ι : Type u_2,
F : ι → α → E,
p : filter ι,
f : α → E,
s : set α,
Ffs : ∀ (x : α), x ∈ s → filter.tendsto (λ (i : ι), F i x) p (nhds (f x)),
v : ℝ≥0∞,
hv : v < evariation_on f s,
n : ℕ,
u : ℕ → α,
um : monotone u,
us : ∀ (i : ℕ), u i ∈ s,
hlt : v < ∑ (i : ℕ) in finset.range n, edist (f (u (i + 1))) (f (u i))
⊢ pseudo_emetric_space ℝ≥0∞

[Sebastien Gouezel]

There is no emetric_space instance on ennreal, because the topology induced by the to-be edistance would not be the right one (there would be no finite sequence tending to infinity for the edistance, because the edistance would always be infinite).

[Rémi Bottinelli]

Ah, so I have to deal with this differently, thanks!

[Sebastien Gouezel]

You should just apply the lemma saying that sums on finsets are continuous, I think.

[Rémi Bottinelli]

Have a link by any chance ?

[Yaël Dillies]

docs#continuous_finset_sum

[Sebastien Gouezel]

Or docs#tendsto_finset_sum

[Junyan Xu]

Or at least that's what I believe the motivation for a different type for path is (@Junyan Xu )?

There are several motivations:

1. Using variable interval as domain is what's on the textbooks (BBI and BH) and also come up in homotopy theory (which is the main customer of docs#path at the moment, I think). I don't completely get their motivation yet, we'll see. I'll see if I can complete the proof of idempotency with the current path.

2. To consider arclength parametrization you have to use an interval of length equal to the length of the path, though the left endpoint could be chosen to be 0. If you just want a constant speed parametrization then [0,1] (as in docs#path) is good enough, but docs#path.trans of two constant speed paths may not be constant speed. So either develop a version of docs#path.trans that joins two paths not just at 1/2 but at any point in [0,1] (involves division which introduce unnecessary complexity), or paths with variable start/end points are needed.

[Sebastien Gouezel]

Sebastien Gouezel said:

Aside: please don't write p.tendsto f q, use instead tendsto f p q. It's closer to the intended mathematical content.

#18062

[Junyan Xu]

Rémi Bottinelli said:

What about this?

(map_source : ∀ ⦃t⦄, t ≤ 0 → path t = x)
(map_target : ∀ ⦃t⦄, l ≤ t → path t = y)

I agree this is a nice way to restore extensionality; and this is equivalent to the more succinct set.Icc_extend (zero_le l) (path ∘ coe) = path which has some API like docs#continuous.Icc_extend'.

[Junyan Xu]

Aside: please don't write p.tendsto f q, use instead tendsto f p q. It's closer to the intended mathematical content.

Is writing p.tendsto f q really so counterintuitive? It could be written as x → p ⇒ f x → q in usual mathematical notation, where f is between p and q (although it's probably more commonly written as f x → q as x → p.
Oh sorry, these are filters, so I don't know what the usual mathematical notations are... but I like infix notations which can be thought of as l₁ --f-→ l₂.
If you really want to put pp_nodot, though, you should probably do the same for docs#filter.map.

[Rémi Bottinelli]

Is there a one-liner for the sorried-out lemma?

lemma emetric.tendsto_edist' {ι : Type*} {F G : ι → E} {p : filter ι} {f g : E}
  (Ff : filter.tendsto F p (nhds f)) (Gg : filter.tendsto G p (nhds g)) :
  filter.tendsto (λ i, edist (F i) (G i)) p (nhds $ edist f g) := sorry

lemma lower_continuous_aux {ι : Type*} {F : ι → α → E} {p : filter ι}
  {f : α → E} {s : set α} (Ffs : ∀ x ∈ s, filter.tendsto (λ i, F i x) p (nhds (f x)))
  {v : ℝ≥0∞} (hv : v < evariation_on f s) : (∀ᶠ (n : ι) in p, v < evariation_on (F n) s) :=
begin
  obtain ⟨⟨n, ⟨u, um, us⟩⟩, hlt⟩ := lt_supr_iff.mp hv,
  have : filter.tendsto (λ j, ∑ (i : ℕ) in finset.range n, edist (F j (u (i + 1))) (F j (u i)))
           p (nhds (∑ (i : ℕ) in finset.range n, edist (f (u (i + 1))) (f (u i)))), by
  { apply tendsto_finset_sum,
    exact λ i hi, emetric.tendsto_edist' (Ffs (u i.succ) (us i.succ)) (Ffs (u i) (us i)) },
  exact (eventually_gt_of_tendsto_gt hlt this).mono
    (λ i h, lt_of_lt_of_le h (sum_le (F i) n um us)),
end

/--
`λ f, evariation_on f s` is lower semicontinuous for pointwise convergence *on `s`*.
Pointwise convergence on `s` is encoded here as uniform convergence on the family consisting of the
singletons of elements of `s`.
-/
lemma lower_semicontinuous {s : set α} :
  lower_semicontinuous (λ f : uniform_on_fun α E (s.image $ λ x, {x}), evariation_on f s) :=
begin
  intro f,
  apply @lower_continuous_aux _ _ _ _ (uniform_on_fun α E (s.image singleton)) id (nhds f) f s _,
  simpa only [uniform_on_fun.tendsto_iff_tendsto_uniformly_on, mem_image, forall_exists_index,
             and_imp, forall_apply_eq_imp_iff₂,
             tendsto_uniformly_on_singleton_iff_tendsto] using @filter.tendsto_id _ (nhds f),
end

[Sebastien Gouezel]

docs#filter.tendsto.edist

[Sebastien Gouezel]

Also, please use 𝓝 instead of nhds (opening the locale topological_space).

[Rémi Bottinelli]

:) I was looking at emetric.tends_to_nhbds

[Sebastien Gouezel]

In general, we have lemmas with dot notation for most convergence results, so that it is straightforward to build convergence statements from the different constituants.

[Rémi Bottinelli]

Updated: https://github.com/leanprover-community/mathlib/pull/18058

[Rémi Bottinelli]

I actually also removed a coercion in the def of the variation, after seeing a comment of Junyan, and it does cut elaboration time by a lot, but since it's not the purpose of the PR, I can revert that change (it just happened to be on the branch I was working on)

[Rémi Bottinelli]

https://github.com/leanprover-community/mathlib/pull/18040/files <- updated the variation_from_to PR

[Sebastien Gouezel]

Junyan Xu said:

Or at least that's what I believe the motivation for a different type for path is (@Junyan Xu )?

2. To consider arclength parametrization you have to use an interval of length equal to the length of the path, though the left endpoint could be chosen to be 0. If you just want a constant speed parametrization then [0,1] (as in docs#path) is good enough, but docs#path.trans of two constant speed paths may not be constant speed. So either develop a version of docs#path.trans that joins two paths not just at 1/2 but at any point in [0,1] (involves division which introduce unnecessary complexity), or paths with variable start/end points are needed.

I wouldn't use a new structure for that: only a function defined on the whole real-line, and in relevant lemmas I would put an assumption is_arclength_on f a b (meaning that for all c, d in [a, b], the variation of f from c to d is d - c). Introducing new types has a cost (you need to build a whole API around it, and make sure it interacts nicely with as much as you can), so it shoudn't be done lightly. For instance, the structure path x y is necessary because fundamental groups are built as quotients of these, so you can't just get away with an assumption you put in some lemmas. Here, it's not obvious to me which problem it would solve. (I'm not saying: "don't do it"; I'm saying "do it if you really thought the design through and it's the best solution").

[Rémi Bottinelli]

Should we keep an "indexing set" s for your is_arclength_on?

def is_linearly_parameterized_on_by (f : ℝ → E) (s : set ℝ) (l : ℝ) :=
∀ x y, evariation_on f (s ∩ Icc x y) = ennreal.of_real (l * (y - x))

[Rémi Bottinelli]

Uh, that's wrong, we want only to quantify over x y in s I believe

[Junyan Xu]

I saw that you posted a comment on GitHub as well.

I think it's good to keep an indexing set s, because we do want to consider (half-)infinite paths/geodesics (example), and that shows my path_btw is too restrictive; a remedy could be allowing ereal values for source/target, but it maybe easier to just allow the generality of an arbitrary indexing set, which may be required to be docs#set.ord_connected (which covers all kinds of intervals including Ioo) in theorems.

Assuming s is ord_connected, which says Icc x y is included in s whenever x and y are, we may simplify evariation_on f (s ∩ Icc x y) to evariation_on f (Icc x y), which is exactly my arclength f x y. For this reason, I'm not sure whether I should include s into arclength, since I can't think of situations in which we want to consider s that are not intervals/ord_connected.

On GitHub I said there are four specializations of evariation_on that could be done independently:

(1) restrict to intervals (replace s by s ∩ Icc x y)
(2) upgrade to the signed version (ennreal -> ereal, nnreal -> real)
(3) specialize to the bounded variation / finite length case (ennreal -> nnreal, ereal -> real)
(4) stop carrying around the set s (i.e. take s := univ)

I did (1)&(4) in the arclength gist while you did (1)(2)(3) in #18040. Item (1) is common to both, and I feel that it's reasonable to bundle (2)&(3) together (as you did). You said on GitHub that "(1) probably should not be changed for as long as possible" but in your is_linearly_parameterized_on_by, what you do is exactly item (1), and none of (2)(3)(4). Maybe my description of the four items has some ambiguity so you didn't catch my intended meaning?

If I keep s around in my gist (i.e. don't do item (4)), then you'd be able to define your variation_on_from_to in terms of my arclength. However, now I think it's better to keep the two separate, and I'd be happy to see #18040 go through, after refactoring a proof to use multiplicative_of_total (now in #18080).

I think your formulation of uniqueness of natural parametrization is probably true (when l, l' > 0) for general s (it would have to be dense in an interval in order to naturally parametrize some curve, though), no matter you use s ∩ Icc x y or just Icc x y in the definition of linear parametrization. Monotonicity can probably be replaced by injectivity if s is ord_connected. I'm also thinking a statement of the form

example {f : ℝ → E} {s : set ℝ} (φ ψ : ℝ → ℝ)
  (φm : monotone_on φ s) (ψm : monotone_on ψ s)
  (hφ : is_naturally_parameterized_on (f ∘ φ) (φ⁻¹' s))
  (hψ : is_naturally_parameterized_on (f ∘ ψ) (ψ⁻¹' s)) :
  ∃ r : ℝ, ∀ x, ψ x = φ (x + r) /- should be replaced by eq_on -/ :=

but it's not true because if f stops at a point during some interval then there's freedom to change a value of ψ or φ in that interval to any other point in the same interval.

[Rémi Bottinelli]

What I meant I think was about your item 4 actually: We should keep s as long as possible, in order to allow to talk about functions that might be badly behaved outside of a given s. E.g. talking about arc-length of functions that are defined on all of real but that we really mean as path from some interval.
As for my snippet above, to be clear, I meant it as

def is_linearly_parameterized_on_by (f : ℝ → E) (s : set ℝ) (l : ℝ) :=
∀ (x y \in s), evariation_on f (s ∩ Icc x y) = ennreal.of_real (l * (y - x))

and in that case, I agree that it might be easier to replace s ∩ Icc x y by Icc x y, but I think I wouldn't do it: it might be helpful to allow removing "singularities" from the domain, no, like if we start with piecewise smooth functions, we might get in situation where the easiest is just to drop the non-smooth parts from s ?

[Rémi Bottinelli]

Junyan Xu said:

If I keep s around in my gist (i.e. don't do item (4)), then you'd be able to define your variation_on_from_to in terms of my arclength. However, now I think it's better to keep the two separate, and I'd be happy to see #18040 go through, after refactoring a proof to use multiplicative_of_total (now in #18080).

I'm getting a bit lost: Would you have two different definitions of "variation"/arclength that are so close together yet not defined in terms of each other? What kind of hierarchy of definitions do you envision, and where would is_linearly_parameterized_on_by (or equivalent) sit?

[Junyan Xu]

it might be helpful to allow removing "singularities" from the domain, no, like if we start with piecewise smooth functions, we might get in situation where the easiest is just to drop the non-smooth parts from s ?

I don't know what removing "singularities" buys you when it comes to evariation_on. The curve would still have to continuous everywhere (in an interval) right? I think when f is continuous you can show evariation_on f (closure s) = evariation_on f s. Unfortunately it's not necessarily true that evariation_on f (closure s ∩ Icc x y) = evariation_on f (s ∩ Icc x y), for example when s = {-1/n, 1 + 1/n | n > 0}, x = 0 and y = 1 (LHS is {0, 1} while RHS is empty). When t is open, I think we do have evariation_on f (closure s ∩ t) = evariation_on f (s ∩ t) though, because of docs#is_open.closure_inter.

[Rémi Bottinelli]

What about this for the path metric? Tomorrow, I plan on trying to set up the infrastructure to show that the path metric is idempotent, leaving the necessary technical lemmas out, in order to get something going, and see what formulations of the lemmas (E.g. continuity of variation, and rectifiability of paths wrt the path metric) are necessary.
@Junyan Xu If you already have something fleshed out, can you share it?

def path_emetric.edist (x y : E) : ℝ≥0∞ :=
  ⨅ (p : ℝ → E) (l : ℝ≥0) (h : p 0 = x ∧ p l = y ∧ continuous_on p (set.Icc 0 l)),
    evariation_on p (set.Icc 0 l)

[Sebastien Gouezel]

It's not clear to me if the definition will work out better by allowing a varying l as you do, or just fixing l = 1 for definiteness. Probably the difference won't really matter anyway.

[Junyan Xu]

@Rémi Bottinelli I haven't got a chance to work on path metric/idempotency yet; mostly dealing with algebra PRs these days. You can find latest updates on the continuity results here (made some adjustments to make them hopefully easier to apply).

[Rémi Bottinelli]

I got to that: plenty of sorrys remaining, and it's not very satisfying:

import topology.metric_space.emetric_space
import analysis.bounded_variation
import topology.metric_space.lipschitz

noncomputable theory

open_locale nnreal ennreal big_operators

section real_line_map

variables (a b : ℝ)

lemma continuous_line_map : continuous (λ x, a + (b-a)*x) := sorry
lemma surj_on_unit_interval_line_map_of_le (h : a ≤ b) :
  set.surj_on (λ x, a + (b-a)*x) unit_interval (set.Icc a b) := sorry
lemma maps_to_unit_interval_line_map_of_le (h : a ≤ b) :
  set.maps_to (λ x, a + (b-a)*x) unit_interval (set.Icc a b) := sorry
lemma monotone_line_map_of_le (h : a ≤ b) :
  monotone (λ x, a + (b-a)*x) := sorry

lemma surj_on_unit_interval_line_map_of_ge (h : b ≤ a) :
  set.surj_on (λ x, a + (b-a)*x) unit_interval (set.Icc b a) := sorry
lemma maps_to_unit_interval_line_map_of_ge (h : b ≤ a) :
  set.maps_to (λ x, a + (b-a)*x) unit_interval (set.Icc b a) := sorry
lemma antitone_line_map_of_ge (h : b ≤ a) :
  antitone (λ x, a + (b-a)*x) := sorry

end real_line_map

namespace evariation_on

lemma sum_on_Icc_le {α E : Type*} [linear_order α] [pseudo_emetric_space E]
  (f : α → E) {s : set α} (n : ℕ) {u : ℕ → α} (hu : monotone u) (us : ∀ i, i ≤ n → u i ∈ s) :
  ∑ i in finset.range n, evariation_on f (set.Icc (u i) (u i.succ) ∩ s) ≤ evariation_on f s :=
begin
  revert s,
  induction n,
  { rintro s us, simp only [finset.range_zero, finset.sum_empty, zero_le'], },
  { rintro s us,
    specialize @n_ih {x | x ∈ s ∧ x ≤ u n_n} (λ i hi,  ⟨us i (hi.trans (nat.le_succ _)), hu hi⟩),
    rw finset.sum_range_succ,
    have : ∑ (i : ℕ) in finset.range n_n, evariation_on f (set.Icc (u i) (u i.succ) ∩
                                                           {x : α | x ∈ s ∧ x ≤ u n_n})
         = ∑ (i : ℕ) in finset.range n_n, evariation_on f (set.Icc (u i) (u i.succ) ∩ s), by
    { refine finset.sum_congr rfl (λ i hi, _),
      congr' 1 with x : 1,
      refine ⟨λ h, ⟨h.1,h.2.1⟩, λ h, ⟨h.1, ⟨h.2, h.1.2.trans (hu (nat.succ_le_of_lt _))⟩⟩⟩,
      rw finset.mem_range at hi,
      exact hi, },
    rw this at n_ih,
    refine (add_le_add_right n_ih _).trans ((add_le_union f _).trans (mono f _)),
    { rintros x ⟨_,hx⟩ y ⟨⟨hy,_⟩,_⟩, exact hx.trans hy, },
    { rintros x (⟨h,_⟩|⟨_,h⟩); exact h, }, },
end

end evariation_on

section path_emetric

universe u

private abbreviation 𝕀 := unit_interval

def path_emetric (E : Type u) [pseudo_emetric_space E] : Type u := E

variables {E : Type u} [pseudo_emetric_space E]

def to_path_emetric : E → path_emetric E := id
def from_path_emetric : path_emetric E → E := id
abbreviation of : E → path_emetric E := to_path_emetric
abbreviation fo : path_emetric E → E := from_path_emetric

lemma from_to_path_emetric (x : E) : from_path_emetric (to_path_emetric x) = x := rfl
lemma to_from_path_emetric (x : path_emetric E) : to_path_emetric (from_path_emetric x) = x := rfl

def path_emetric.edist (x y : E) : ℝ≥0∞ :=
  ⨅ (p : ℝ → E) (h : p 0 = x ∧ p 1 = y ∧ continuous_on p 𝕀), evariation_on p 𝕀

instance : pseudo_emetric_space (path_emetric E) :=
{ edist := λ x y, path_emetric.edist (from_path_emetric x) (from_path_emetric y),
  edist_self := λ x, by
  { dsimp [path_emetric.edist],
    refine le_antisymm _ zero_le',
    transitivity' (evariation_on (λ (t : ℝ), fo x) 𝕀),
    { refine infi₂_le (λ t : ℝ, fo x) ⟨rfl,rfl, continuous_on_const⟩,  },
    { refine eq.le (evariation_on.constant_on _),
      simp only [set.nonempty.image_const, set.nonempty_Icc, zero_le_one, set.subsingleton_singleton], }, },
  edist_comm := λ x y, by
  { apply le_antisymm;
    { dsimp [path_emetric.edist],
      apply le_infi₂ _,
      rintro p ⟨px,py,pc⟩,
      rw ←evariation_on.comp_eq_of_antitone_on p (λ u, 1 + (0-1)*u),
      apply infi₂_le _ _,
      split,
      { simp only [zero_sub, neg_mul, one_mul, function.comp_app, neg_zero, add_zero, py], },
      split,
      { simp only [px, zero_sub, neg_mul, one_mul, function.comp_app, eq_self_iff_true, true_and,
                   ←sub_eq_add_neg, sub_self], },
      apply pc.comp (continuous_line_map 1 0).continuous_on,
      exact maps_to_unit_interval_line_map_of_ge 1 0 (zero_le_one),
      exact (antitone_line_map_of_ge 1 0 (zero_le_one)).antitone_on _,
      exact maps_to_unit_interval_line_map_of_ge 1 0 (zero_le_one),
      exact surj_on_unit_interval_line_map_of_ge 1 0 (zero_le_one), }, },
  edist_triangle := λ x y z, by
  { dsimp only [path_emetric.edist],
    simp_rw [ennreal.infi_add, ennreal.add_infi],
    refine le_infi (λ p, le_infi (λ hp, le_infi (λ q, le_infi (λ hq, _)))),
    obtain ⟨px,py,pc⟩ := hp,
    obtain ⟨qy,qz,qc⟩ := hq,
    have : evariation_on p 𝕀 + evariation_on q 𝕀 =
           evariation_on (λ t, if t ≤ 1/2 then p (2 * t) else q (2 * t - 1)) 𝕀, by
    { nth_rewrite_rhs 0 ←set.inter_self 𝕀,
      rw ←evariation_on.Icc_add_Icc (λ t, if t ≤ 1/2 then p (2 * t) else q (2 * t - 1)) (sorry : 0 ≤ 1/2) (half_le_self zero_le_one) sorry,
      congr' 1,
      { sorry, },
      { sorry, }, },
    rw this, clear this,
    refine infi₂_le _ _,
    have : ¬ 1 ≤ 1/2, by sorry,
    simp only [one_div, inv_nonneg, zero_le_bit0, zero_le_one, mul_zero, if_true, mul_one],
    refine ⟨px,_,_⟩, sorry, sorry,
  } }

lemma path_emetric.edist_le {x y : E} {p : ℝ → E} {s t : ℝ} (st : s ≤ t)
  (ps : p s = x) (pt : p t = y) (pc : continuous_on p (set.Icc s t)) :
  edist (of x) (of y) ≤ evariation_on p (set.Icc s t) :=
begin
  have : evariation_on p (set.Icc s t) = (evariation_on (p ∘ (λ u, s + (t-s)*u)) 𝕀), by
  { symmetry, apply evariation_on.comp_eq_of_monotone_on,
    exact (monotone_line_map_of_le _ _ st).monotone_on _,
    exact (maps_to_unit_interval_line_map_of_le _ _ st),
    exact (surj_on_unit_interval_line_map_of_le _ _ st), },
  rw this,
  apply infi₂_le _ _,
  simp only [function.comp_app, mul_zero, add_zero, mul_one, add_sub_cancel'_right],
  exact ⟨ps, pt, pc.comp (continuous_line_map s t).continuous_on
                         (maps_to_unit_interval_line_map_of_le s t st)⟩,
end

lemma from_path_emetric_nonexpanding :
  lipschitz_with 1 (from_path_emetric : path_emetric E → E) :=
begin
  rintro x y,
  dsimp only [edist, path_emetric.edist],
  simp only [ennreal.coe_one, one_mul, le_infi₂_iff],
  rintro p ⟨px, py, pc⟩,
  rw [←px, ←py],
  exact evariation_on.edist_le p unit_interval.zero_mem unit_interval.one_mem,
end

lemma continuous_for_path_metric_of_bounded_variation_of_continuous {f : ℝ → E}
  (fc : continuous_on f 𝕀) (fb : has_bounded_variation_on f 𝕀) :
  continuous_on (of ∘ f) 𝕀 := sorry

lemma sum_for_path_metric_le_evariation_on_of_bounded_variation {f : ℝ → E}
  {s : set ℝ} (hs : ∀ (x z ∈ s) (y : ℝ), x ≤ y → y ≤ z → y ∈ s)
  (fb : has_locally_bounded_variation_on f s) (fc : continuous_on f s)
  (n : ℕ) {u : ℕ → ℝ} (us : ∀ i, u i ∈ s) (um : monotone u) :
  ∑ i in finset.range n, edist ((of ∘ f) (u (i + 1))) ((of ∘ f) (u i)) ≤ evariation_on f s :=
begin
  calc ∑ i in finset.range n, edist ((of ∘ f) (u (i + 1))) ((of ∘ f) (u i))
     ≤ ∑ i in finset.range n, evariation_on f (set.Icc (u i) (u i.succ)) : by
  begin
    refine finset.sum_le_sum (λ i hi, _),
    rw edist_comm,
    refine path_emetric.edist_le (um (i.le_succ)) rfl rfl (continuous_on.mono fc _),
    exact λ t ht, hs (u i) (us i) (u i.succ) (us i.succ) t ht.left ht.right,
  end
  ...= ∑ i in finset.range n, evariation_on f (set.Icc (u i) (u i.succ) ∩ s) : by
  { congr' 1 with i : 1, congr, symmetry,
    apply set.inter_eq_self_of_subset_left,
    exact λ t ht, hs (u i) (us i) (u i.succ) (us i.succ) t ht.left ht.right, }
  ...≤ evariation_on f s : evariation_on.sum_on_Icc_le f n um (λ i hi, us i)
end

lemma evariation_on_for_path_metric_le_evariation_on_of_bounded_variation {f : ℝ → E}
  {s : set ℝ} (hs : ∀ (x z ∈ s) (y : ℝ), x ≤ y → y ≤ z → y ∈ s)
  (fb : has_locally_bounded_variation_on f s)  (fc : continuous_on f s) :
  evariation_on (of ∘ f) s ≤ evariation_on f s :=
begin
  dsimp only [evariation_on],
  refine supr_le _,
  rintro ⟨n, ⟨u, um, us⟩⟩,
  apply sum_for_path_metric_le_evariation_on_of_bounded_variation hs fb fc n us um,
end

lemma path_metric_idempotent : isometry (of : path_emetric E → path_emetric (path_emetric E)) :=
begin
  rintro x y,
  dsimp only [edist, from_path_emetric, path_emetric.edist],
  apply le_antisymm; simp only [le_infi_iff],
  { rintro f ⟨fx, fy, fc⟩,
    by_cases h : evariation_on f 𝕀 ≠ ⊤,
    { refine le_trans _ (evariation_on_for_path_metric_le_evariation_on_of_bounded_variation (λ x ⟨zx,xo⟩ y ⟨zy,yo⟩ u xu uy, ⟨zx.trans xu, uy.trans yo⟩ ) (has_bounded_variation_on.has_locally_bounded_variation_on h) fc),
      refine infi₂_le (of ∘ f) ⟨congr_arg of fx, congr_arg of fy, _⟩,
      exact continuous_for_path_metric_of_bounded_variation_of_continuous fc h, },
    { rw not_not.mp h, exact le_top, }, },
  { rintro f' ⟨f'x, f'y, f'c⟩,
    have : evariation_on f' 𝕀 = (1 : ennreal) * (evariation_on f' 𝕀), by rw [one_mul], rw this,
    refine le_trans _ (((from_path_emetric_nonexpanding).lipschitz_on_with set.univ).comp_evariation_on_le (set.maps_to_univ _ _)),
    refine infi₂_le (fo ∘ f') ⟨congr_arg fo f'x, congr_arg fo f'y, _⟩,
    exact from_path_emetric_nonexpanding.continuous.continuous_on.comp f'c (set.maps_to_univ _ 𝕀), }
end

end path_emetric

[Rémi Bottinelli]

But I'd welcome feedback on the formulation of it: is that architecturally what you were thinking of, @Junyan Xu ?

[Rémi Bottinelli]

Maybe it would be easier to just have continuous p as an assumption for the distance, since it allows using continuous.if_le

[Rémi Bottinelli]

I'll do that, at least for the time being.

[Rémi Bottinelli]

I think it's looking OK, and it's better to use path x y and add some API around it, like I tried to do here.
Some questions:

• I need the following:

def comp
  {X : Type*} [topological_space X] {x y : X} (γ : path x y)
  {Y : Type*} [topological_space Y] (φ : X → Y) (φc : continuous φ ) : path (φ x) (φ y) := sorry

lemma extend_comp
  {X : Type*} [topological_space X] {x y : X} (γ : path x y)
  {Y : Type*} [topological_space Y] (φ : X → Y) (φc : continuous φ ) :
  (γ.comp φ φc).extend = φ ∘ γ.extend := sorry

This should be somewhere in mathlib, no?

• I used the following statement for continuity of arc-length:

lemma variation_on_from_to_continuous_on {E : Type*} [pseudo_emetric_space E] {f : ℝ → E}
  {s : set ℝ} (hs : ∀ ⦃x⦄ (xs : x∈s) ⦃z⦄ (zs : z∈s), set.Icc x z ⊆ s)
  (fc : continuous_on f s) (fb : has_locally_bounded_variation_on f s) {a : ℝ} (as : a ∈ s) :
  continuous_on (variation_on_from_to f s a) s := sorry

Does that look reasonable?

[Rémi Bottinelli]

Mmh, we can probably drop the a \in s assumption here.

[Rémi Bottinelli]

OK, the way I used variation_on_from_to was kind of a détour, I'm using this now:

theorem continuous_right_self_evariation' {f : ℝ → E} {a b : ℝ} (ab : a < b)
  (fb : has_locally_bounded_variation_on f (set.Ico a b))
  (hcont : continuous_within_at f (set.Ico a b) a) /- f is right continuous at a -/ :
  filter.tendsto (λ (x : ℝ), evariation_on f (set.Icc a x))
    (nhds_within a (set.Ici a)) (nhds 0) := sorry

theorem continuous_right_self_evariation {f : ℝ → E}
  {s : set ℝ} (hs : ∀ ⦃x⦄ (xs : x∈s) ⦃z⦄ (zs : z∈s), set.Icc x z ⊆ s)
  (fb : has_locally_bounded_variation_on f s) {a : ℝ} (as : a ∈ s)
  (hcont : continuous_within_at f (s ∩ set.Ici a) a) /- f is right continuous at a -/ :
  filter.tendsto (λ (b : ℝ), evariation_on f (set.Icc a b))
    (nhds_within a (s ∩ set.Ici a)) (nhds 0) :=
begin
  rw emetric.tendsto_within_nhds_ennreal_zero,
  by_cases h : ∃ b, b ∈ s ∧ b > a,
  { obtain ⟨b,bs,ab⟩ := h,
    let := continuous_right_self_evariation' ab _ _,
    sorry, sorry, sorry, },
  { push_neg at h,
    rintro ε hε,
    refine ⟨1,zero_lt_one, λ x hx dxa, _⟩,
    obtain ⟨xs,xa⟩ := hx,
    cases le_antisymm (h x xs) xa,
    rw evariation_on.subsingleton _ (by simp : (set.Icc a a).subsingleton),
    exact hε, },

end
theorem continuous_left_self_evariation' {f : ℝ → E} {a b : ℝ}  (ba : b < a)
  (fb : has_locally_bounded_variation_on f (set.Ioc b a))
  (hcont : continuous_within_at f (set.Ioc b a) a) /- f is left continuous at a -/ :
  filter.tendsto (λ (x : ℝ), evariation_on f (set.Icc x a))
    (nhds_within a (set.Iic a)) (nhds 0) := sorry

theorem continuous_left_self_evariation {f : ℝ → E}
  {s : set ℝ} (hs : ∀ ⦃x⦄ (xs : x∈s) ⦃z⦄ (zs : z∈s), set.Icc x z ⊆ s)
  (fb : has_locally_bounded_variation_on f s) {a : ℝ} (as : a ∈ s)
  (hcont : continuous_within_at f (s ∩ set.Iic a) a) /- f is left continuous at a -/ :
  filter.tendsto (λ (b : ℝ), evariation_on f (set.Icc b a))
    (nhds_within a (s ∩ set.Iic a)) (nhds 0) := sorry

I believe the non-prime versions follow from the prime ones, (not finished the proof though).
I wrote everything in terms of tendsto … (nhds 0) because writing in terms of continuity felt kind of wrong.

[Rémi Bottinelli]

I used the following too, which I couldn't find in mathlib because ennreal complicates epsilon-delta arguments it seems:

lemma emetric.tendsto_within_nhds_ennreal_zero
  {α : Type*} [pseudo_emetric_space α] {s : set α} {f : α → ℝ≥0∞} {a : α} :
  filter.tendsto f (nhds_within a s) (nhds 0) ↔
    ∀ (ε : ennreal), ε > 0 →
      (∃ (δ : ennreal) (H : δ > 0), ∀ {x : α}, x ∈ s → has_edist.edist x a < δ → f x < ε) :=
begin
  rw ennreal.tendsto_nhds_zero,
  split,
  { rintro h ε hε,
    let ε' := (ε/2) ⊓ 1,
    have : ε' > 0 := lt_inf_iff.mpr ⟨(ennreal.half_pos hε.lt.ne.symm),zero_lt_one⟩,
    have : ε' < ε, by
    { by_cases ht : ε = ⊤,
      { cases ht, rw inf_lt_iff, right, exact ennreal.one_lt_top, },
      { rw inf_lt_iff, left, exact ennreal.half_lt_self hε.lt.ne.symm ht, } },
    specialize h ε' ‹ε'>0›,
    obtain ⟨δ,hδ,h⟩ := emetric.mem_nhds_within_iff.mp h,
    refine ⟨δ,hδ,λ x xs dxa, _⟩,
    apply lt_of_le_of_lt (h ⟨dxa,xs⟩) ‹ε'<ε›, },
  { rintro h ε hε,
    obtain ⟨δ,hδ,h⟩ := h ε hε,
    dsimp only [filter.eventually],
    rw emetric.mem_nhds_within_iff,
    refine ⟨δ,hδ, λ x hx, (h hx.2 hx.1).le⟩, }
end

[Rémi Bottinelli]

And then the proof that a continuous rectifiable curve stays continuous looks like this:

lemma continuous_for_path_metric_of_bounded_variation_of_continuous {f : ℝ → E}
  {s : set ℝ} (hs : ∀ ⦃x⦄ (xs : x∈s) ⦃z⦄ (zs : z∈s), set.Icc x z ⊆ s)
  (fc : continuous_on f s) (fb : has_locally_bounded_variation_on f s) :
  continuous_on (of ∘ f) s :=
begin
  rw emetric.continuous_on_iff,
  rintros b bs ε hε,
  let hleft := continuous_right_self_evariation hs fb bs
                 ((fc.continuous_within_at bs).mono (set.inter_subset_left _ _)),
  rw emetric.tendsto_within_nhds_ennreal_zero at hleft,
  obtain ⟨δl,hδl,hl⟩ := hleft ε hε,
  let hright := continuous_left_self_evariation hs fb bs
                 ((fc.continuous_within_at bs).mono (set.inter_subset_left _ _)),
  rw emetric.tendsto_within_nhds_ennreal_zero at hright,
  obtain ⟨δr,hδr,hr⟩ := hright ε hε,
  refine ⟨δl ⊓ δr, lt_inf_iff.mpr ⟨hδl.lt,hδr.lt⟩, λ a as hab, _⟩,
  simp only [function.comp_app],
  rcases lt_trichotomy a b with (ab|rfl|ba),
  { apply lt_of_le_of_lt,
    apply edist_le ab.le rfl rfl (fc.mono (hs as bs)),
    apply hr ⟨as,ab.le⟩ (lt_of_lt_of_le hab inf_le_right), },
  { simp only [edist_self], exact hε, },
  { rw edist_comm,
    apply lt_of_le_of_lt,
    apply edist_le ba.le rfl rfl (fc.mono (hs bs as)),
    refine hl ⟨as,ba.le⟩ (lt_of_lt_of_le hab inf_le_left), },
end

That's probably heavily simplifiable.

[Rémi Bottinelli]

I'll continue and try to clean everything up, and then try with a PR when satisfied with how it looks. Hope I'm going in the right direction.

[Sebastien Gouezel]

Rémi Bottinelli said:

I'll continue and try to clean everything up, and then try with a PR when satisfied with how it looks. Hope I'm going in the right direction.

That looks definitely like the right direction!

[Junyan Xu]

path.comp is docs#path.map in mathlib:

import topology.path_connected
namespace path

def comp
  {X : Type*} [topological_space X] {x y : X} (γ : path x y)
  {Y : Type*} [topological_space Y] (φ : X → Y) (φc : continuous φ ) : path (φ x) (φ y) :=
γ.map φc

lemma extend_comp
  {X : Type*} [topological_space X] {x y : X} (γ : path x y)
  {Y : Type*} [topological_space Y] (φ : X → Y) (φc : continuous φ ) :
  (γ.comp φ φc).extend = φ ∘ γ.extend := rfl
/- a bit weird this isn't stated as a lemma, even though it holds by definition. -/
end path

And here hs is exactly docs#set.ord_connected:

lemma variation_on_from_to_continuous_on {E : Type*} [pseudo_emetric_space E] {f : ℝ → E}
  {s : set ℝ} (hs : ∀ ⦃x⦄ (xs : x∈s) ⦃z⦄ (zs : z∈s), set.Icc x z ⊆ s)

[Junyan Xu]

I now think maybe we needn't to use docs#path.extend much, which maybe in some sense goes into implementation details of docs#path and sort of breaks API. I'm trying to see if this works:

def length {x y : E} (p : path x y) : ℝ≥0∞ := evariation_on p set.univ

[Rémi Bottinelli]

It's what I had I first, and found it to be messier, but you may have more success than I did.

[Rémi Bottinelli]

Btw, I tried to adapt your arclength code to my needs (which ended up being practically nothing), in order to get the lemmas:

lemma continuous_right_self_arclength
  (hcont : continuous_within_at f (set.Ico a b) a) /- f is right continuous at a -/ :
  filter.tendsto (arclength f a) (nhds_within a (set.Ici a)) (nhds 0) := sorry

and respectively continuous_left_self_arclength:

• Are you planning to open a PR with that code?
• If so, can you include that lemma/formulation?
• If not, should I do it?
• def arclength seems a bit on the edge of being worth it: it and the lemmas that you defined shorten a lot of things, but at the same time it really only calls already present evariation_on code. Should we keep it?

[Junyan Xu]

I guess I'll wait after we make sure the proof of idempotency works before PR'ing arclength continuity. Whatever lemmas that ends up in the final proof will certainly get PR'd. This particular lemma is easy:

lemma continuous_right_self_arclength
  (hcont : continuous_within_at f (set.Ico a b) a) /- f is right continuous at a -/ :
  filter.tendsto (arclength f a) (nhds_within a (set.Ici a)) (nhds 0) :=
by { convert continuous_right_self_arclength f hab hrect hcont, rw arclength_self }

I guess it becomes continuous_right_self_evariation' in your code.

def arclength seems a bit on the edge of being worth it: it and the lemmas that you defined shorten a lot of things, but at the same time it really only calls already present evariation_on code. Should we keep it?

So you propose to inline arclength as evariation_on everywhere? I think there are enough lemmas about it to deserve a separate definition; we would need some docstring to explain its similarity and difference with evariation_on_from_to though.

[Rémi Bottinelli]

Junyan Xu said:

So you propose to inline arclength as evariation_on everywhere? I think there are enough lemmas about it to deserve a separate definition; we would need some docstring to explain its similarity and difference with evariation_on_from_to though.

Well, I tried it and it got too much hassle and I gave up, which kind of shows its utility, but assuming evariation_on_from_to stays, that would make 3 similar-ish definitions, and I seem to have been drilled to think that the number of defs should be minimized as much as possible…

[Rémi Bottinelli]

Where would you include this definition?

[Rémi Bottinelli]

But I guess, too, that having this "set of discourse" s everywhere is kind of useless when talking specifically about rectifiablity, and then we could base everything on arclength, but then again, we'd have to make a new definition for a "signed" arclength.

[Junyan Xu]

All code in mathlib are built upon existing code, and I think it's good to specialize general APIs to make statements more like what you see on books. I think maths works best when you make abstraction at the right level, and I don't think minimizing the number of defs is the right philosophy.

[Junyan Xu]

I guess I'll include the definition in the bounded_variation file. Making a "variation" folder that include the bounded_variation file and a new arclength file would also be an option; the bounded_variation file is a bit long and we may consider break it down, though some proofs look golf-able.

[Rémi Bottinelli]

splitting the file would be nice, already just to make it easier to work on it without waiting for the orange bars to disappear.

[Rémi Bottinelli]

I guess there no way to make evariation_on_from_to and arclength more compatible, because arclength is essentially an alias for choosing endpoints, while evariation_on_from_to chooses endpoints _and_ is signed, in addition to keeping s and passing to reals.

[Rémi Bottinelli]

Well, we could have (unsigned_)evariation_on_from_to : ennreal and signed_evariation_on_from_to : ereal and arclength := (unsigned_)evariation_on_from_to set.univ

[Rémi Bottinelli]

taking into account your last comment on the from_to PR

[Junyan Xu]

Yeah the "set of discourse" is probably useless in this context.
However, I'm not fully convinced that a signed version of arclength is strictly necessary; can you give an example where it's used? And I think we may consider using evariation_on_from_to when we need it.

[Rémi Bottinelli]

Can you rephrase that last sentence, I'm not sure I follow? Are you saying we should maybe not rush merging evariation_on_from_to ?
In general, I don't really have any other example for a signed arclength/variation than the arc-length parameterization I guess. So I agree we might want to work with an "on-use" approach: arclength is useful already, while evariation_on_from_to hasn't proven useful beyond its own definition/lemmas. But for a fullest formulation of the arclength parameterization, I think we'll probably still need evariation_on_from_to : real.

[Junyan Xu]

I mean that in the cases we need the signed version, we're probably in the finite case, and can then use evariation_on_from_to specialized to s = univ (but then we probably need to build some APIs around the specialization).
evariation_on_from_to was used to golf the proof that BV functions to the reals are differences of monotone functions, so I'd say it has proved its utility there but not in the path length context.
Arclength parametrization can be characterized by considering only ordered pairs of points x ≤ y:

def is_linearly_parameterized_on_by (f : ℝ → E) (s : set ℝ) (l : ℝ) :=
∀ {x y} (h : x ≤ y), evariation_on f (s ∩ Icc x y) = ennreal.of_real (l * (y - x))
/- or ∀ {x y} (h : x ≤ y), (arclength f x y).to_real = l * (y - x) which seems better -/

so it seems to me that a signed version isn't strictly necessary.(In fact your original definition already doesn't use a signed version, but relied on truncation of docs#ennreal.of_real at 0, while if you consider ordered pairs then it doesn't rely on the truncation.)

[Rémi Bottinelli]

Mmh, but when you define the arc-length parameterization, say for a function on all of real, you'll have to choose a basepoint, and before this basepoint, you'll want to have negative values I believe.
I mean, the endgoal being to be able to say that a sufficiently nice function f can be written as f' \circ \phi where \phi is arc-length of f, and f' is linearly parameterized.

[Rémi Bottinelli]

(gtg)

[Junyan Xu]

Indeed, for paths parametrized by left-infinite intervals it's more convenient to have a signed version of arclength.

[Rémi Bottinelli]

I made some progress with https://github.com/bottine/mathlib/blob/bottine/analysis.bounded_variation/natural_parameterization_two/src/analysis/natural_parameterization.lean

[Rémi Bottinelli]

I'll try and actually prove this thing about arc-length parameterization tomorrow

[Junyan Xu]

Great, I've now filled up sorries and cleaned up your idempotency proof: 609 lines with a few unnecessary lemmas.

• I proved the general versions of arclength continuity lemmas for ord_connected sets that you formulated, for which I generalized the hypotheses of the intermediate continuity lemmas used.

• I've chosen evariation_on p set.univ as the definition of path.length, and showed it's the same as your definition in evariation_on_extend_unit_interval_eq_length. My definition seems to be easier to work with when proving symmetry and transitivity of length, but when showing continuity of paths in path metric, I converted to your definition. Maybe that's unnecessary but I need to think about it.

[Rémi Bottinelli]

def length (p : path x y) : ℝ≥0∞ := evariation_on p set.univ --arclength p 0 1

Didn't use arclength p 0 1 because univ is easier to work with ?

[Rémi Bottinelli]

https://github.com/bottine/mathlib/blob/bottine/analysis.bounded_variation/natural_parameterization_two/src/analysis/natural_parameterization.lean <- How does that look?

[Rémi Bottinelli]

I'm quite happy with it: I have e.g. the following:

lemma is_linearly_parameterized_on_by.ratio {f : ℝ → E} {s t : set ℝ} {φ : ℝ → ℝ}
  (φm : monotone_on φ s) (φst : s.maps_to φ t) (φst' : s.surj_on φ t)
  {l l' : ℝ} (hl : 0 ≤ l) (hl' : 0 < l')
  (hfφ : is_linearly_parameterized_on_by (f ∘ φ) s l)
  (hf : is_linearly_parameterized_on_by f t l')
  ⦃x : ℝ⦄ (xs : x ∈ s) : s.eq_on φ (λ y, (l / l') * (y - x) + (φ x)).

noncomputable def natural_parameterization (f : α → E) {s : set α}
  {a : α} (as : a ∈ s) : ℝ → E :=
f ∘ (@function.inv_fun_on _ _ ⟨a⟩ (variation_on_from_to f s a) s)

lemma natural_parameterization_edist_zero {f : α → E} {s : set α}
  (hf : has_locally_bounded_variation_on f s) {a : α} (as : a ∈ s) {b : α} (bs : b ∈ s) :
  edist (f b) (((natural_parameterization f as) ∘ (variation_on_from_to f s a)) b) = 0.

lemma natural_parameterization_is_naturally_parameterized (f : α → E) {s : set α}
  (hf : has_locally_bounded_variation_on f s) {a : α} (as : a ∈ s) :
  is_naturally_parameterized_on (natural_parameterization f as) (variation_on_from_to f s a '' s).

[Rémi Bottinelli]

This is essentially what I was aiming for. I'll try for a PR soon-ish, knowing that it depends on the variation_on_from_to PR.

[Rémi Bottinelli]

Here we go: https://github.com/leanprover-community/mathlib/pull/18208
Feedback welcome

[Rémi Bottinelli]

@Sebastien Gouezel In your opinion, how much work would it be to prove that arclength = integral of speed ? Is everything needed already in mathlib?

[Sebastien Gouezel]

If I understand correctly the question, that's not true in general: there exist continuous functions which are differentiable Lebesgue almost everwyhere with derivative equal to zero Lebesgue almost everywhere but which are not constant (google Cantor staircase). You need an additional assumption of absolute continuity. See for instance Rudin, Real and Complex Analysis, Theorem 8.18 for instance.

[Rémi Bottinelli]

Ah, sorry, I meant "under reasonable assumptions"

[Sebastien Gouezel]

The correct assumption is called absolute continuity. It holds for instance for Lipschitz functions. I don't think we have anything on these yet in mathlib, so these would be prerequisites.

[Rémi Bottinelli]

I see, thanks. I guess C¹ by parts would also suffice, and with more prerequisites already present?

[Sebastien Gouezel]

For C^1 functions, we already have the result. But C^1 by parts is a pain to work with formally...

[Rémi Bottinelli]

ah, neat, what's the name of the lemma/theorem?

[Sebastien Gouezel]

There are many versions, you can browse around docs#integral_eq_sub_of_has_deriv_at_of_le

[Rémi Bottinelli]

@Junyan Xu I'm trying to make your latest iteration of the path_emetric into something PR-able:

• Should your unit_interval lemmas be put in the unit_interval file?
  I'd say everything up to two_mul_div_two should, and the three others left here.

• Is div_two better than half ?

• What about the affine_map and related lemmas?
• (@Sebastien Gouezel too:) How should we deal with arclength? it seems quite clear to me that it should have its own file rather than taking half or more of the path_emetric file, but where?
• Also, it seems a bit of a missed opportunity not to have the continuity lemmas be stated for evariation_on and put in the bounded_variation file, no?

[Junyan Xu]

Hi @Rémi Bottinelli, thanks for doing this! Here are my opinions:

• Yes the unit_intervals should be put in the unit_interval file should be put in the unit_interval file, and I don't see an obvious reason why "the three others" should be left here ... Even the affine_map stuff can be moved there, because docs#affine_homeomorph_image_I and docs#Icc_homeo_I (though there's also docs#set.image_affine_Icc' in a probably earlier file).

• I'm fine with half if you are happy with it.

• I think the arclength and length space stuff should be put under topology.metric_space, where docs#pseudo_emetric_space is located. And you're welcome to generalize the results to evariation_on!

• I made just a bit of revision to my gist in the meantime.

[Rémi Bottinelli]

Thanks, will try to put everything where it belongs, and ping here when it's done/I get stuck.

[Rémi Bottinelli]

I see affine_homeomorph needs the multiplicative factor to be non-zero. Perhaps it's better we restate the "reparameterization" lemmas in terms of affine_homeomorph too?

[Rémi Bottinelli]

@Junyan Xu Re. your "very strange" comment here. It's probably due to the fact that of_length_ne_top was a lemma. refl works if it's turned into a def.

[Junyan Xu]

I see affine_homeomorph needs the multiplicative factor to be non-zero. Perhaps it's better we restate the "reparameterization" lemmas in terms of affine_homeomorph too?

It certainly needs non-zeroness to be a bijection ... Your link directs to my gist; do you mean docs#has_constant_speed_on_with.ratio instead? There it won't make things less general, but I don't see how it simplifies things either.

Re. your "very strange" comment here. It's probably due to the fact that of_length_ne_top was a lemma. refl works if it's turned into a def.

Good catch, thanks! If I'd put it into a branch the def-lemma linter would have caught it. That "lemma" was probably originally proving continuity but later I bundled it into a path.

[Rémi Bottinelli]

No, I'm just not sure how to fit those affine_map lemmas and was wondering how to use more of the "existing infra".

[Rémi Bottinelli]

https://github.com/leanprover-community/mathlib/pull/18375 Here is a PR (draft) to get started.

[Rémi Bottinelli]

oh, this is clearly not gonna compile now because I changed some of the lemmas for affine_map by putting the additive constant after the multiplication (in order to match what's already here)