Continuity of curried linear function

Stream: Is there code for X?

[Dominic Steinitz]

As part my attempt to prove the existence of a Riemannian metric, I have ended up with this problem which I reproduce below as a MWE.

import Mathlib.Geometry.Manifold.Instances.Real
import Mathlib.Geometry.Manifold.MFDeriv.Atlas

set_option linter.unusedSectionVars false

open Manifold

variable
  {EB : Type*} [NormedAddCommGroup EB] [NormedSpace ℝ EB] [InnerProductSpace ℝ EB]
  {HB : Type*} [TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞}
  {B : Type*} [TopologicalSpace B] [ChartedSpace HB B]

noncomputable def g (i : B) (p : B) (v w : (@TangentSpace ℝ _ _ _ _ _ _ IB B _ _) p) : ℝ :=
  letI dψ := mfderiv IB 𝓘(ℝ, EB) (extChartAt IB i) p
  @Inner.inner ℝ EB _ (dψ v) (dψ w)

lemma g_add' (i p : B) (x y v : TangentSpace IB p) :
  g i p v (x + y) = g i p v x + g i p v y := by
  unfold g
  let dψ := mfderiv IB 𝓘(ℝ, EB) (extChartAt IB i) p
  have h_map : dψ (x + y) = dψ x + dψ y := ContinuousLinearMap.map_add dψ x y
  rw [h_map]
  exact @inner_add_right ℝ EB _ _ _ _ _ _

lemma g_smul' (i p : B) (x v : TangentSpace IB p) (m : ℝ) :
  g i p v (m • x) = (RingHom.id ℝ) m • g i p v x := by
  unfold g
  let dψ := mfderiv IB 𝓘(ℝ, EB) (extChartAt IB i) p
  have : dψ (m • x) = m • dψ x := ContinuousLinearMap.map_smul_of_tower dψ m x
  rw [this]
  have : @Inner.inner ℝ EB _ (dψ v) (m • (dψ x)) = m • @Inner.inner ℝ EB _ (dψ v) (dψ x) :=
    @inner_smul_right_eq_smul ℝ EB _ _ _ _ _ _ _ _ _ _ (dψ v) (dψ x) m
  exact this

lemma g_cont (i p : B) (v : TangentSpace IB p) :
  Continuous (fun w ↦ g i p v w) := by
  unfold g

  have continuous_inner_left {v : EB} : Continuous (fun w ↦ @Inner.inner ℝ EB _ v w) :=
    continuous_inner.comp (continuous_const.prodMk continuous_id)

  have h_desired : Continuous fun w ↦
  @Inner.inner ℝ EB _ ((mfderiv IB 𝓘(ℝ, EB) (↑(extChartAt IB i)) p) v)
    ((mfderiv IB 𝓘(ℝ, EB) (↑(extChartAt IB i)) p) w) := by
    exact continuous_inner_left |>.comp (mfderiv IB 𝓘(ℝ, EB) (↑(extChartAt IB i)) p).continuous

  exact h_desired

lemma g_cont' (i p : B) :
  Continuous (fun (v : (@TangentSpace ℝ _ _ _ _ _ _ IB B _ _) p ) ↦ ContinuousLinearMap.mk
    { toFun := fun w ↦ g i p v w
      map_add' := fun x y ↦ g_add' i p x y v
      map_smul' := fun m x ↦ g_smul' i p x v m }
    (g_cont i p v)) := by
  exact sorry

[Michael Rothgang]

Here a golfed version, that proves a very similar statement to the one you want g'_cont:

import Mathlib.Geometry.Manifold.Instances.Real
import Mathlib.Geometry.Manifold.Notation
import Mathlib.Geometry.Manifold.MFDeriv.Atlas

set_option linter.unusedSectionVars false

open Manifold

variable
  {EB : Type*} [NormedAddCommGroup EB] [NormedSpace ℝ EB] [InnerProductSpace ℝ EB]
  {HB : Type*} [TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞}
  {B : Type*} [TopologicalSpace B] [ChartedSpace HB B]

noncomputable def g (i : B) (p : B) (v w : TangentSpace IB p) : ℝ :=
  letI dψ := mfderiv% (extChartAt IB i) p
  @Inner.inner ℝ EB _ (dψ v) (dψ w)

variable (IB) in
noncomputable def g' (i p : B) : TangentSpace IB p → TangentSpace IB p → ℝ := fun v w ↦
  letI dψ := mfderiv% (extChartAt IB i) p
  @Inner.inner ℝ EB _ (dψ v) (dψ w)

lemma g_add' (i p : B) (x y v : TangentSpace IB p) : g i p v (x + y) = g i p v x + g i p v y := by
  unfold g
  rw [(mfderiv% (extChartAt IB i) p).map_add x y]
  exact inner_add_right ..

lemma g_smul' (i p : B) (x v : TangentSpace IB p) (m : ℝ) : g i p v (m • x) = (RingHom.id ℝ) m • g i p v x := by
  unfold g
  rw [(mfderiv% (extChartAt IB i) p).map_smul_of_tower m x]
  exact inner_smul_right_eq_smul ..

lemma g_cont (i p : B) (v : TangentSpace IB p) : Continuous (fun w ↦ g i p v w) := by
  unfold g
  fun_prop

-- Do you want to prove this instead?
lemma g'_cont2 (i p : B) : Continuous (g' IB i p) := by
  unfold g'
  fun_prop

lemma g_cont' (i p : B) :
  Continuous (fun (v : (@TangentSpace ℝ _ _ _ _ _ _ IB B _ _) p ) ↦ ContinuousLinearMap.mk
    { toFun := fun w ↦ g i p v w
      map_add' := fun x y ↦ g_add' i p x y v
      map_smul' := fun m x ↦ g_smul' i p x v m }
    (g_cont i p v)) := by
  -- g'_cont2 does not apply, but the reasons seem missing API lemmas.
  exact sorry

[Michael Rothgang]

I also made some clean-ups to your code, including using the new mfderiv% elaborator.

[Michael Rothgang]

(I presume you'll also find the other changes useful. Let me know if you'd like me to make a list.)

[Michael Rothgang]

Note that g_cont can in fact be proven by fun_prop, as can g'_cont

[Michael Rothgang]

Barring that, I'd write it like so

Click to expand

lemma g_cont (i p : B) (v : TangentSpace IB p) : Continuous (fun w ↦ g i p v w) := by
unfold g
have continuous_inner_left {v : EB} : Continuous (fun w ↦ @Inner.inner ℝ EB _ v w) := by fun_prop
have h_desired : Continuous
fun w ↦ @Inner.inner ℝ EB _ ((mfderiv% (extChartAt IB i) p) v) ((mfderiv% (extChartAt IB i) p) w) :=
continuous_inner_left |>.comp (mfderiv% (extChartAt IB i) p).continuous
exact h_desired

[Michael Rothgang]

Does that answer your question? The sorry in your minimal example is a bit strange; while g'_contdoes not prove it right away, my first instinct would be to make this its own definition first and add enough API to make sure the problem is clearly not "some missing simp lemmas or similar".

[Dominic Steinitz]

Thanks very much but on my working branch I don't have

import Mathlib.Geometry.Manifold.Notation

I seem to have

import Mathlib.Geometry.Manifold.Elaborators

but I still get errors.

lemma g_add' (i p : B) (x y v : TangentSpace IB p) : g i p v (x + y) = g i p v x + g i p v y := by
  unfold g
  rw [(mfderiv% (extChartAt IB i) p).map_add x y]
  exact inner_add_right ..

Invalid rewrite argument: Expected an equality or iff proof or definition name, but `?m.137` is a value of type
  ?m.136

Where should I get Mathlib.Geometry.Manifold.Notation from?

[Ruben Van de Velde]

Merge master into your branch

[Dominic Steinitz]

Ruben Van de Velde said:

Merge master into your branch

I fear many merge conflicts await

[Michael Rothgang]

You could take the file on current master (that's what the playground uses, i.e. good enough), add it to your branch and import that instead.

[Michael Rothgang]

Given that your tangent bundle file doesn't import any of the unmerged code Patrick and I wrote, you could probably even re-create a branch based on current master.

[Michael Rothgang]

Or you rebase on Patrick and my branch; all your changes were to different files, right? (So there should be no conflicts.)

[Michael Rothgang]

In case you need local frames, #30083 should have everything you need (and it's based on current master).

[Michael Rothgang]

Dominic Steinitz said:

Thanks very much but on my working branch I don't have

import Mathlib.Geometry.Manifold.Notation

I seem to have

import Mathlib.Geometry.Manifold.Elaborators

but I still get errors.

lemma g_add' (i p : B) (x y v : TangentSpace IB p) : g i p v (x + y) = g i p v x + g i p v y := by
  unfold g
  rw [(mfderiv% (extChartAt IB i) p).map_add x y]
  exact inner_add_right ..

Invalid rewrite argument: Expected an equality or iff proof or definition name, but `?m.137` is a value of type
  ?m.136

Where should I get Mathlib.Geometry.Manifold.Notation from?

Ah, I presume that was before #30307 landed. (That PR is required to support extCharts as the argument to e.g. mfderiv. You need a never version of the file, e.g. the one on master.)

[Dominic Steinitz]

I made my MWE too minimal but now I am worrying my approach is wrong somehow. I keep thinking surely if I have a continuous map and I show it is linear then I have a linear continuous map but apparently Lean does not agree :-( or at least I cannot find a way of making it agree.

import Mathlib.Geometry.Manifold.Instances.Real
import Mathlib.Geometry.Manifold.MFDeriv.Atlas
import Mathlib.Geometry.Manifold.Notation

open Manifold Bundle

variable
  {EB : Type*} [NormedAddCommGroup EB] [NormedSpace ℝ EB] [InnerProductSpace ℝ EB]
  {HB : Type*} [TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞}
  {B : Type*} [TopologicalSpace B] [ChartedSpace HB B]

variable (IB) in
noncomputable def g (i p : B) : TangentSpace IB p → TangentSpace IB p → ℝ := fun v w ↦
  letI dψ := mfderiv% (extChartAt IB i) p
  @Inner.inner ℝ EB _ (dψ v) (dψ w)

lemma g_add' (i p : B) (x y v : TangentSpace IB p) :
  g IB i p v (x + y) = g IB i p v x + g IB i p v y := by
  unfold g
  rw [(mfderiv% (extChartAt IB i) p).map_add x y]
  exact inner_add_right ..

lemma g_add'' (i p : B) (x y v : TangentSpace IB p) :
  g IB i p (x + y) v = g IB i p x v + g IB i p y v := by
  unfold g
  let dψ := mfderiv IB 𝓘(ℝ, EB) (extChartAt IB i) p
  have h_map : dψ (x + y) = dψ x + dψ y := ContinuousLinearMap.map_add dψ x y
  rw [h_map]
  exact @inner_add_left ℝ EB _ _ _ _ _ _

lemma g_smul' (i p : B) (x v : TangentSpace IB p) (m : ℝ) :
  g IB i p v (m • x) = (RingHom.id ℝ) m • g IB i p v x := by
  unfold g
  rw [(mfderiv% (extChartAt IB i) p).map_smul_of_tower m x]
  exact inner_smul_right_eq_smul ..

lemma g_smul'' (i p : B) (x v : TangentSpace IB p) (m : ℝ) :
  g IB i p (m • v) x = (RingHom.id ℝ) m • g IB i p v x := by
  unfold g
  let dψ := mfderiv IB 𝓘(ℝ, EB) (extChartAt IB i) p
  have : dψ (m • v) = m • dψ v := ContinuousLinearMap.map_smul_of_tower dψ m v
  rw [this]
  have : @Inner.inner ℝ EB _ (m • (dψ v)) (dψ x) = m • @Inner.inner ℝ EB _ (dψ v) (dψ x) :=
    @inner_smul_left_eq_smul ℝ EB _ _ _ _ _ _ _ _ _ _ _ (dψ v) (dψ x) m
  exact this

lemma g_cont (i p : B) (v : TangentSpace IB p) : Continuous (fun w ↦ g IB i p v w) := by
  unfold g
  fun_prop

-- Do you want to prove this instead?
lemma g'_cont2 (i p : B) : Continuous (g IB i p) := by
  unfold g
  fun_prop

lemma g_cont' (i p : B) :
  Continuous (fun (v : (@TangentSpace ℝ _ _ _ _ _ _ IB B _ _) p ) ↦ ContinuousLinearMap.mk
    { toFun := fun w ↦ g IB i p v w
      map_add' := fun x y ↦ g_add' i p x y v
      map_smul' := fun m x ↦ g_smul' i p x v m }
    (g_cont i p v)) := by
  -- g'_cont2 does not apply, but the reasons seem missing API lemmas.
  exact sorry

noncomputable
def g_bilinear (i p : B) :
   (@TangentSpace ℝ _ _ _ _ _ _ IB B _ _) p →L[ℝ]
    ((@TangentSpace ℝ _ _ _ _ _ _ IB B _ _) p →L[ℝ] Trivial B ℝ p) :=
  ContinuousLinearMap.mk
    { toFun := fun v ↦
        ContinuousLinearMap.mk
          { toFun := fun w ↦ g IB i p v w
            map_add' := fun x y ↦ g_add' i p x y v
            map_smul' := fun m x ↦ g_smul' i p x v m }
          (g_cont i p v)
      map_add' := fun x y ↦ by
                    apply ContinuousLinearMap.ext
                    intro w
                    exact g_add'' i p x y w
      map_smul' := fun m x ↦ by
                    apply ContinuousLinearMap.ext
                    intro w
                    exact g_smul'' i p w x m }
    (g_cont' i p) -- g'_cont2 is the wrong type

[Michael Rothgang]

Let me look into this. There are definitely things I don't understand (as in: they fail for reasons I don't understand yet), I'll ask in my office and get back to you.

[Michael Rothgang]

My current WIP, by the way:

import Mathlib.Geometry.Manifold.Instances.Real
import Mathlib.Geometry.Manifold.MFDeriv.Atlas
import Mathlib.Geometry.Manifold.Notation

open Manifold Bundle

variable
  {EB : Type*} [NormedAddCommGroup EB] [NormedSpace ℝ EB] [InnerProductSpace ℝ EB]
  {HB : Type*} [TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞}
  {B : Type*} [TopologicalSpace B] [ChartedSpace HB B]

variable (IB) in
noncomputable def g (i p : B) : TangentSpace IB p → TangentSpace IB p → ℝ := fun v w ↦
  letI dψ := mfderiv% (extChartAt IB i) p
  @Inner.inner ℝ EB _ (dψ v) (dψ w)

lemma g_add' (i p : B) (x y v : TangentSpace IB p) :
    g IB i p v (x + y) = g IB i p v x + g IB i p v y := by
  unfold g
  rw [(mfderiv% (extChartAt IB i) p).map_add x y]
  exact inner_add_right ..

lemma g_add'' (i p : B) (x y v : TangentSpace IB p) :
    g IB i p (x + y) v = g IB i p x v + g IB i p y v := by
  unfold g
  let dψ := mfderiv% (extChartAt IB i) p
  rw [dψ.map_add]
  exact inner_add_left ..

lemma g_smul' (i p : B) (x v : TangentSpace IB p) (m : ℝ) :
    g IB i p v (m • x) = (RingHom.id ℝ) m • g IB i p v x := by
  unfold g
  rw [(mfderiv% (extChartAt IB i) p).map_smul_of_tower m x]
  exact inner_smul_right_eq_smul ..

lemma g_smul'' (i p : B) (x v : TangentSpace IB p) (m : ℝ) :
    g IB i p (m • v) x = (RingHom.id ℝ) m • g IB i p v x := by
  unfold g
  let dψ := mfderiv IB 𝓘(ℝ, EB) (extChartAt IB i) p
  rw [dψ.map_smul_of_tower]
  exact inner_smul_left_eq_smul ..

lemma g_cont (i p : B) (v : TangentSpace IB p) : Continuous (fun w ↦ g IB i p v w) := by
  unfold g
  fun_prop

-- Do you want to prove this instead?
variable (IB) in
lemma g'_cont2 (i p : B) : Continuous (g IB i p) := by
  unfold g
  fun_prop

@[simps]
noncomputable def foo (i p : B) (v : TangentSpace IB p) : TangentSpace IB p →ₗ[ℝ] ℝ where
  toFun := fun w ↦ g IB i p v w
  map_add' := fun x y ↦ g_add' i p x y v
  map_smul' := fun m x ↦ g_smul' i p x v m

@[simp]
lemma coe_foo (i p : B) (v : TangentSpace IB p) :
    (foo i p v : TangentSpace IB p → ℝ) = fun w ↦ g IB i p v w := rfl

@[simps!]
noncomputable def bar (i p : B) (v : TangentSpace IB p) : TangentSpace IB p →L[ℝ] ℝ :=
  ContinuousLinearMap.mk (foo i p v) (g_cont i p v)

@[simp]
lemma coe_bar (i p : B) (v : TangentSpace IB p) :
    (bar i p v : TangentSpace IB p → ℝ) = fun w ↦ g IB i p v w := rfl

lemma g_cont' (i p : B) : Continuous (fun (v : TangentSpace IB p) ↦ bar i p v) := by
  suffices Continuous fun v w ↦ g IB i p v w by
    -- XXX: why is this step so difficult? none of the simp lemmas above seem to help...
    have : Continuous fun v ↦ fun w ↦ g IB i p v w := sorry
    --simp
    --rw [coe_foo]
    --dsimp
    --convert this
    sorry
  exact g'_cont2 IB i p

noncomputable
def g_bilinear (i p : B) :
   TangentSpace IB p →L[ℝ] (TangentSpace IB p →L[ℝ] Trivial B ℝ p) :=
  ContinuousLinearMap.mk
    { toFun := fun v ↦ bar i p v
      map_add' := fun x y ↦ by ext w; exact g_add'' i p x y w
      map_smul' := fun m x ↦ by ext w; exact g_smul'' i p w x m }
    (g_cont' i p) -- g'_cont2 is the wrong type

[Michael Rothgang]

Here's a hunch: are you sure you are proving the right statement? In the medium term, you also want to construct a smooth Riemannian metric, and to prove smoothness of your construction.

[Michael Rothgang]

To speak about smoothness of a section, you need to convert it from a dependent function into a non-dependent function on the total space. Perhaps you need to do the same for continuity.

[Michael Rothgang]

So, I'd suggest proving a different statement: firstly, try proving smoothness (or, at least, stating it: this will guide you towards what you actually want to prove). Secondly, this will require you to apply the T% elaborator (which is just a short-hand for TotalSpace.mk').

[Michael Rothgang]

I can well imagine that stating the right smoothness statement and making it typecheck will be a painful process. But since you want to get there anyway... I'm not sure how much avoiding it helps.