Extending a linear map from a neighborhood of zero

Stream: Is there code for X?

[Igor Khavkine]

If $U$ is an open neighborhood of zero in vector space $V$ and $f \colon U \to W$ is a function that is known to be compatible with addition and scalar multiplication, as long as these operations fit inside the domain $U$, does Mathlib already have a way of extending $f$ to a LinearMap $\bar{f} \colon V \to W$ by linearity?

[Kevin Buzzard]

There are lots of assumptions missing here before this even makes syntactic sense and I very much doubt that even after adding them you'll have a statement which is mathematically valid.

[Kenny Lau]

Really? I thought this is "obviously true"

[Kenny Lau]

import Mathlib

open TopologicalSpace

variable {k V W : Type*} [NormedField k] [NormedAddCommGroup V] [NormedAddCommGroup W]
  [NormedSpace k V] [NormedSpace k W] (U : OpenNhdsOf (0 : V)) (f : U → W)
  (hf : Continuous f) (hfadd : ∀ x : U, ∀ y : U, (h : x.1 + y ∈ U) → f ⟨x + y, h⟩ = f x + f y)
  (hfsmul : ∀ c : k, ∀ x : U, (h : c • x.1 ∈ U) → f ⟨c • x, h⟩ = c • f x)

def extension : { g : V →ₗ[k] W // Continuous g ∧ ∀ x : U, g x = f x } := sorry

[Aaron Liu]

This looks false as stated (you need a NontriviallyNormedField)

[Edward van de Meent]

i feel like continuousness of f or topology of the codomain isn't really part of the question here? the intuition (as i understand it) is that any (open) neighbourhood of 0 would contain a basis, and so it would enable you to extend f to the full space?

[Edward van de Meent]

something along the lines of "choose a basis, scale their vectors down to within the neighbourhood, and induce your total map. this is independent of basis because f locally respects scalar multiplication and addition"

[Edward van de Meent]

or i guess you don't even need the basis, you can just immediately scale into some open ball around 0 and contained in your neighbourhood...

[Scott Carnahan]

There is a topology on formal Laurent series (in one variable over a fixed CommRing) such that the “formal Taylor series” form an open subspace. You can talk about the set of continuous linear extensions of a continuous linear function, but there is no really distinguished choice, especially if you want invariance under change of coordinates.

[Igor Khavkine]

Here's a version of the statement that I wanted (Kenny Lau was on the right track). I managed to prove compatibility with scalar multiplication and additivity should be fairly similar. Unfortunately, I had to restrict to the Real case. Didn't quite see my way out of manipulating the smul expressions with terms coming simultaneously from Real, field k and vector space V. Didn't use continuity yet, that would make sense for a ContinuousLinearMap extension.

Also, some more automation would have been nice, but I couldn't figure out which tactics would find the needed algebraic manipulations. Suggestions welcome!

Edit: The proof is now sorry free, though still only for LinearMap.

import Mathlib

open TopologicalSpace Metric

variable {V W : Type*}
  [NormedAddCommGroup V] [NormedSpace ℝ V]
  [NormedAddCommGroup W] [NormedSpace ℝ W]
  {U : Set V} (hU : U ∈ nhds 0) (f : V → W) (hf : ContinuousOn f U)
  (hfadd : ∀ x ∈ U, ∀ y ∈ U, x + y ∈ U → f (x + y) = f x + f y)
  (hfsmul : ∀ c : ℝ, ∀ x ∈ U, c • x ∈ U → f (c • x) = c • f x)

open Classical in
omit hf in
noncomputable def extend_linearMap_of_nhd_zero : V →ₗ[ℝ] W := by
  replace hU := Metric.mem_nhds_iff.mp hU
  have ⟨hε, hball⟩ := hU.choose_spec
  set ε := hU.choose
  have rmemU {r : ℝ} (hr : |r| ≤ 1) (z : V) {C : ℝ} (hC : ‖z‖ ≤ C) : r • (ε / 2 * C⁻¹) • z ∈ U := by
    apply Set.mem_of_mem_of_subset _ hball
    simp only [mem_ball, dist_zero_right]
    simp only [norm_smul, norm_mul, norm_inv, Real.norm_eq_abs, mul_assoc _ _ ‖z‖, ← mul_assoc |r|,
      abs_div, Nat.abs_ofNat, abs_of_pos hε]
    nth_rw 2 [← mul_one ε]
    apply mul_lt_mul_of_nonneg_of_pos
      (LE.le.trans_lt (mul_le_of_le_one_left (div_nonneg hε.le zero_le_two) hr) <| div_two_lt_of_pos hε)
      _
      (mul_nonneg (abs_nonneg _) <| div_nonneg hε.le zero_le_two)
      zero_lt_one
    apply (mul_le_mul_of_nonneg_left hC (inv_nonneg.mpr <| abs_nonneg C)).trans
    apply LE.le.trans _ (inv_mul_le_one (a := |C|))
    apply mul_le_mul_of_nonneg_left _ (inv_nonneg.mpr <| abs_nonneg C)
    exact le_abs_self C
  have memU (z : V) {C : ℝ} (hC : ‖z‖ ≤ C) : (ε / 2 * C⁻¹) • z ∈ U := by
    rw [← one_smul ℝ (_ • _)]
    exact rmemU abs_one.le _ hC
  exact {
    toFun := by
      exact fun x => ((ε / 2) * ‖x‖⁻¹)⁻¹ • f (((ε / 2) * ‖x‖⁻¹) • x),
    map_add' := by
      intro x y
      by_cases hxy : x ≠ 0 ∧ y ≠ 0
      case neg =>
        simp only [ne_eq, not_and_iff_not_or_not, Decidable.not_not] at hxy
        rcases hxy with hx | hy
        · cases hx
          simp
        · cases hy
          simp
      case pos =>
        have hx := norm_ne_zero_iff.mpr hxy.1
        have hy := norm_ne_zero_iff.mpr hxy.2
        by_cases hxy0 : x + y ≠ 0
        case neg =>
          simp only [ne_eq, Decidable.not_not] at hxy0
          simp only [hxy0, norm_zero, inv_zero, mul_zero, smul_zero, zero_smul]
          replace hxy0 : y = -x := (neg_eq_of_add_eq_zero_right hxy0).symm
          simp only [hxy0, norm_neg, smul_neg]
          rw [← neg_one_smul ℝ]
          rw [hfsmul (-1:ℝ) _ (memU x le_rfl) _]
          simp only [mul_inv_rev, inv_inv, inv_div, neg_smul, one_smul, smul_neg, add_neg_cancel]
          apply rmemU _ _ le_rfl
          norm_num
        let L := ‖x‖ ⊔ ‖y‖ ⊔ ‖x+y‖
        have hL : L ≠ 0 := by
          apply Ne.symm <| LT.lt.ne _
          apply lt_max_of_lt_left <| lt_max_of_lt_left _
          exact norm_pos_iff.mpr hxy.1
        have smuleq (z : V) : z = ‖z‖ • ‖z‖⁻¹ • z := by
          by_cases hz : z ≠ 0
          case neg =>
            simp only [ne_eq, Decidable.not_not] at hz
            cases hz
            simp
          case pos =>
            simp only [smul_smul, mul_inv_cancel₀ (norm_ne_zero_iff.mpr hz), one_smul]
        calc
          (ε / 2 * ‖x + y‖⁻¹)⁻¹ • f ((ε / 2 * ‖x + y‖⁻¹) • (x + y))
            = (ε / 2 * ‖x + y‖⁻¹)⁻¹ • f ((‖x + y‖⁻¹ * L) • (ε / 2 * L⁻¹) • (x + y)) := by
              congr 2
              simp only [smul_smul]
              congr 1
              ring_nf
              simp only [mul_assoc _ L _, mul_inv_cancel₀ hL, mul_one]
          _ = (ε / 2 * ‖x + y‖⁻¹)⁻¹ • (‖x + y‖⁻¹ * L) • f ((ε / 2 * L⁻¹) • (x + y)) := by
              congr 1
              apply hfsmul
              · apply memU (x + y)
                unfold L
                exact le_max_right ..
              · simp only [smul_smul, mul_comm _ L⁻¹, mul_assoc _ L]
                rw [← mul_assoc L, mul_inv_cancel₀ hL, one_mul, mul_comm]
                apply memU (x + y) le_rfl
          _ = (ε / 2 * L⁻¹)⁻¹ • f ((ε / 2 * L⁻¹) • x + (ε / 2 * L⁻¹) • y) := by
              simp only [smul_smul, smul_add]
              congr
              simp only [mul_inv, inv_inv]
              ring_nf
              simp only [mul_assoc ε⁻¹, mul_inv_cancel₀ (norm_ne_zero_iff.mpr hxy0), one_mul]
          _ = (ε / 2 * L⁻¹)⁻¹ • (f ((ε / 2 * L⁻¹) • x) + f ((ε / 2 * L⁻¹) • y)) := by
              congr
              apply hfadd _ (memU ..) _ (memU ..) _
              · unfold L
                apply (le_max_left _ _ ).trans <| le_max_left _ _
              · unfold L
                apply (le_max_right _ _ ).trans <| le_max_left _ _
              · rw [← smul_add]
                apply memU _ (le_max_right ..)
          _ =   (ε / 2 * L⁻¹)⁻¹ • f ((ε / 2 * L⁻¹) • x)
              + (ε / 2 * L⁻¹)⁻¹ • f ((ε / 2 * L⁻¹) • y) := by
              simp only [smul_add]
          _ =   (ε / 2 * ‖x‖⁻¹)⁻¹ • (‖x‖⁻¹ * L) • f ((ε / 2 * L⁻¹) • x)
              + (ε / 2 * ‖y‖⁻¹)⁻¹ • (‖y‖⁻¹ * L) • f ((ε / 2 * L⁻¹) • y) := by
              simp only [smul_smul]
              congr
              all_goals
              simp only [mul_inv, inv_inv]
              ring_nf
              simp only [mul_assoc _ ‖_‖ _, mul_inv_cancel₀ hx, mul_inv_cancel₀ hy, mul_one]
          _ =   (ε / 2 * ‖x‖⁻¹)⁻¹ • f ((‖x‖⁻¹ * L) • (ε / 2 * L⁻¹) • x)
              + (ε / 2 * ‖y‖⁻¹)⁻¹ • f ((‖y‖⁻¹ * L) • (ε / 2 * L⁻¹) • y) := by
              congr <;> apply Eq.symm <| hfsmul ..
              · apply memU
                unfold L
                apply (le_max_left _ _ ).trans <| le_max_left _ _
              · rw [smul_smul, mul_comm _ L⁻¹, mul_assoc _ L, ← mul_assoc L, mul_inv_cancel₀ hL, one_mul,
                  mul_comm]
                exact memU _ le_rfl
              · apply memU
                unfold L
                apply (le_max_right _ _ ).trans <| le_max_left _ _
              · rw [smul_smul, mul_comm _ L⁻¹, mul_assoc _ L, ← mul_assoc L, mul_inv_cancel₀ hL, one_mul,
                  mul_comm]
                exact memU _ le_rfl
          _ =   (ε / 2 * ‖x‖⁻¹)⁻¹ • f ((ε / 2 * ‖x‖⁻¹) • x)
              + (ε / 2 * ‖y‖⁻¹)⁻¹ • f ((ε / 2 * ‖y‖⁻¹) • y) := by
              congr 3
              all_goals
              rw [smul_smul, mul_comm _ L⁻¹, mul_assoc _ L, ← mul_assoc L, mul_inv_cancel₀ hL, one_mul]
              ring_nf
      ,
    map_smul' := by
      intros c x
      have hxε : (ε / 2 * ‖x‖⁻¹) • x ∈ ball 0 ε := by
        simp only [mem_ball, dist_zero_right]
        simp only [norm_smul, norm_mul, norm_inv, norm_norm, Real.norm_eq_abs (ε / 2), mul_assoc,
          abs_div, Nat.abs_ofNat, abs_of_pos hε]
        nth_rw 2 [← mul_one ε]
        exact mul_lt_mul_of_nonneg_of_pos
          (div_two_lt_of_pos hε) inv_mul_le_one (div_nonneg hε.le zero_le_two) zero_lt_one
      have hx : (ε / 2 * ‖x‖⁻¹) • x ∈ U := by
        apply Set.mem_of_mem_of_subset hxε hball
      have hcx : (|c|⁻¹ * c) • (ε / 2 * ‖x‖⁻¹) • x ∈ U := by
        apply Set.mem_of_mem_of_subset _ hball
        simp only [mem_ball, dist_zero_right] at *
        rw [norm_smul, Real.norm_eq_abs, abs_mul, abs_inv, abs_abs]
        nth_rw 2 [← one_mul ε]
        exact mul_lt_mul_of_le_of_lt_of_nonneg_of_pos inv_mul_le_one hxε (norm_nonneg _) zero_lt_one
      simp only [RingHom.id_apply]
      rw [norm_smul, Real.norm_eq_abs, mul_inv |c|, ← mul_assoc, mul_comm (ε / 2), mul_assoc, mul_inv, inv_inv]
      rw [smul_smul _ c _, mul_comm _ c, ← mul_assoc, mul_comm c _, ← smul_smul (|c|⁻¹ * c)]
      rw [hfsmul _ _ hx hcx, smul_smul _ (_ * c), mul_assoc, mul_comm _ (_ * c), ← mul_assoc, ← smul_smul]
      congr
      rw [← mul_assoc]
      by_cases hc : c ≠ 0
      · rw [mul_inv_cancel₀ (abs_ne_zero.mpr hc)]
        ring
      · simp only [ne_eq, Decidable.not_not] at hc
        simp [hc, mul_zero]
  }

[Anatole Dedecker]

I expect that you can make this work for any Hausdorff topological vector space over a docs#NontriviallyNormedField, precisely because non triviality allows you to scale things as small as you want while staying non-zero.

[Igor Khavkine]

For reference, I've completed the proof over ℝ. It's edited into my earlier post. It's a bit annoying how tedious it was. :man_shrugging: Perhaps the proof could be made much shorter by handling the algebraic manipulations in a different way, but I don't know what that could be.

Probably in its current form it is not general enough to be PR'd into Mathlib. I'll leave this thread as a possible inspiration for someone to start refactoring and generalizing the result. :)