[Merged by Bors] - feat: Lipschitz extensions of maps into l^infty

[chriscamano]

A function f : α → ℓ^∞(ι, ℝ) which is K-Lipschitz on a subset s admits a K-Lipschitz extension to the whole space.

Co-authored-by: Ian Bunner 31334766+ian-bunner@users.noreply.github.com

---

[chriscamano]

Closes leanprover-community/mathlib#11571

[urkud]

Thank you for working on this! Looks very good! I have a few minor comments. I'll checkout the branch and have a look at the main proof later tonight.

[tb65536]

Some potential golfs/refactors:

[tb65536]

If you write refine' ⟨fun i ↦ ⟨swap g i, _⟩, _, _⟩, then you can move hf_extb as an extra goal from the refine.

[ian-bunner]

I like the other two refactors, but I think that it is clearer if we explicitly name our witness and show how it is constructed. I think it would take longer for someone to go through the proof if they have to make the realization themself that swap g i is the desired extension. One sticking point in the proof for us was also this translation back and forth between functions from alpha to iota to R and functions from alpha to l^infty(iota, R). Here it is clear that we get from a function from alpha to iota to R to one from alpha to l^infty(iota, R) by bundling it with a certificate that it is bound. If we instead leave it as inferred and it pops up as an extra goal I think that is more confusing. Also, with no explicit mention of f_ext the term hf_extb ("hypothesis that f_ext is bounded") would have to be changed and given that I cannot think of a meaningful way to name it I think that that is strong evidence that the way the proof is structured now is fairly natural.

However, I am very new and if I've completely misunderstood this suggestion or there is a general consensus on this type of issue I'm certainly open to the change.

Now that we have replaced all mentions of f_ext with swap g i, I do think we should replace f_ext' with f_ext.

[tb65536]

You wouldn't have to choose a new name for hf_extb, since it would just become an extra goal:

    refine' ⟨fun i ↦ ⟨swap g i, _⟩, _, _⟩
    . apply LipschitzWith.uniformly_bounded (swap g) hgl a₀
      use ‖f a₀‖
      rintro - ⟨i, rfl⟩
      simp_rw [←hgeq i ha₀_in_s]
      exact lp.norm_apply_le_norm top_ne_zero (f a₀) i
    · rw [LipschitzWith.coordinate]
      exact hgl
    · intro a hyp
      ext i
      exact (hgeq i) hyp

But I do see what you're saying about how it's nice to make it clear what the extension is, and I'm fine with keeping the current proof structure. I do like renaming f_ext' to f_ext, and using refine' rather than refine:

    let f_ext : α → ℓ^∞(ι) := fun i ↦ ⟨swap g i, hf_extb i⟩
    refine' ⟨f_ext, _, _⟩

[ian-bunner]

Ah I see! Thanks for all the helpful comments!

[PatrickMassot]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style