Non-degenerate bilinear form and von Neumann boundedness

Stream: Is there code for X?

[Michael Rothgang]

Context: I'm trying to construct a Riemannian metric; this is one of the necessary properties.

The following MWE is what I want: I'm really interested in foo'; I know a proof of foo which is weaker, and I can imagine all of this is true in much greater generality. Can somebody enlighten me what I should be looking for?

import Mathlib

lemma foo (E : Type*) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    (φ : E →L[ℝ] E →L[ℝ] ℝ) (hpos : ∀ v : E, v ≠ 0 → 0 < φ v v) :
    Bornology.IsVonNBounded ℝ {v | (φ v) v < 1} := by
  -- Proof sketch: choose a basis {b_i} of E.
  -- Each `φ b_i b_i` is non-zero by hypothesis, hence has positive norm.
  -- By finite-dimensionality of `G`, we have `0 < r := min ‖φ b_i b_i‖`,
  -- thus B(r, 0) is contained in the image of the unit ball under v ↦ φ v v.
  sorry

-- TODO: is this version also true?
lemma foo' (E : Type*) [AddCommGroup E] [TopologicalSpace E] [Module ℝ E] [FiniteDimensional ℝ E]
    (φ : E →L[ℝ] E →L[ℝ] ℝ) (hpos : ∀ v : E, v ≠ 0 → 0 < φ v v) :
    Bornology.IsVonNBounded ℝ {v | (φ v) v < 1} := by
  sorry

[Ben Eltschig]

I'm sure it's true for finite-dimensional topological vector spaces - are you working with one of those, or actually just with a finite-dimensional vector space with some topology?

[Ben Eltschig]

because on a finite-dimensional real vector space, the "standard" topology coming from any norm is the finest topology that makes it a topological vector space, every other topology is coarser. And I think having a coarser topology just means that more sets are bounded, right?

[Michael Rothgang]

I'd like to apply this to each fibre E x of a vector bundle. The standard fibre is a normed space; the trivialisation at each point is a homeomorphism between F and E x (but not necessarily linear).

[Michael Rothgang]

I could ask for the fibers to be topological vector spaces if necessary.

[Eric Wieser]

I'm a little worried that in foo' you'll run into the weirdness alluded to in #maths > Strong topology on linear maps, especially

• continuous bilinear maps are NOT the same as our curried bilinear maps

[Sébastien Gouëzel]

Assume you're in a topological vector space. Phi gives you a norm, which defines the same topology as the initial one (as in finite dimension there is a single topological vector space structure). The unit ball for the norm is von Neumann bounded wrt the topology defined by the norm (we have this in mathlib), so also for the initial topology.

[Ben Eltschig]

Michael Rothgang said:

I'd like to apply this to each fibre E x of a vector bundle. The standard fibre is a normed space; the trivialisation at each point is a homeomorphism between F and E x (but not necessarily linear).

I'm surprised to hear that you don't have a linear trivialisation at hand. I'm sorry if I'm misunderstanding something, I haven't looked at this part of the library in a while - but isn't linearily of the trivialisations part of the definition of docs#VectorBundle, as docs#VectorBundle.trivialization_linear' ?

[Michael Rothgang]

You're right :man_facepalming:, thanks!

[Michael Rothgang]

(On a general fibre bundle, you don't have linearity: but here you do.)

[Michael Rothgang]

Thanks, that is very helpful. I have formalised the second half (see below). I wonder, though: does mathlib have

Sébastien Gouëzel said:

in finite dimension there is a single topological vector space structure

I find docs#unique_topology_of_t2, docs#LinearMap.continuous_of_finiteDimensional and docs#FiniteDimensional.nonempty_continuousLinearEquiv_of_finrank_eq. This statement is certainly contained in the convex hull of them. If you have opinions on how to spell it the right way, these are welcome!

[Michael Rothgang]

Here's my formalisation so far, by the way:

import Mathlib

section aux

variable {G : Type*} [AddCommGroup G] [TopologicalSpace G] [Module ℝ G]
  [ContinuousAdd G] [ContinuousSMul ℝ G] [FiniteDimensional ℝ G]

-- XXX: this is also a norm, not just a seminorm!
noncomputable def mynorm (φ : G →L[ℝ] G →L[ℝ] ℝ) : Seminorm ℝ G where
  toFun v := Real.sqrt (φ v v)
  map_zero' := by simp
  add_le' r s := by sorry -- shouldn't be difficult
  neg' r := by simp
  smul' a v := by simp [← mul_assoc, ← Real.sqrt_mul_self_eq_abs, Real.sqrt_mul (mul_self_nonneg a)]

noncomputable def aux (φ : G →L[ℝ] G →L[ℝ] ℝ) : SeminormFamily ℝ G (Fin 1) := fun _ ↦ mynorm φ

lemma bar (φ : G →L[ℝ] G →L[ℝ] ℝ) (hpos : ∀ v : G, v ≠ 0 → 0 < φ v v) : WithSeminorms (aux φ) :=
  -- In finite dimension there is a single topological vector space structure...
  -- and mynorm defines a norm, hence a TVS structure.
  sorry

end aux

-- golfing suggestions welcome
lemma qux {α : Type*} [Unique α] (s : Finset α) : s = ∅ ∨ s = {default} := by
  by_cases h : s = ∅
  · simp [h]
  · rw [Finset.eq_singleton_iff_nonempty_unique_mem]
    refine Or.inr ⟨Finset.nonempty_iff_ne_empty.mpr h, fun x hx ↦ Unique.uniq _ _⟩

lemma aux_tvs (G : Type*) [AddCommGroup G] [TopologicalSpace G] [Module ℝ G]
    [ContinuousAdd G] [ContinuousSMul ℝ G] [FiniteDimensional ℝ G]
    (φ : G →L[ℝ] G →L[ℝ] ℝ) (hpos : ∀ v : G, v ≠ 0 → 0 < φ v v) :
    Bornology.IsVonNBounded ℝ {v | (φ v) v < 1} := by
  -- Proof sketch (courtesy of Sébastien  Gouezel):
  -- Phi gives you a norm, which defines the same topology as the initial one
  -- (as in finite dimension there is a single topological vector space structure).
  -- The unit ball for the norm is von Neumann bounded wrt the topology defined by the norm
  -- (we have this in mathlib), so also for the initial topology.
  rw [WithSeminorms.isVonNBounded_iff_finset_seminorm_bounded (p := aux φ) (bar φ hpos)]
  intro I
  letI J : Finset (Fin 1) := {1}
  suffices ∃ r > 0, ∀ x ∈ {v | (φ v) v < 1}, (J.sup (aux φ)) x < r by
    obtain (rfl | h) := qux I
    · use 1; simp
    · convert this
  simp only [Set.mem_setOf_eq, Finset.sup_singleton, J]
  refine ⟨1, by norm_num, fun x h ↦ ?_⟩
  simp only [aux, mynorm]
  change Real.sqrt (φ x x) < 1
  rw [Real.sqrt_lt' (by norm_num)]
  simp [h]

[Sébastien Gouëzel]

My preferred version is docs#LinearMap.continuous_of_finiteDimensional applied to the identity between your original vector space, and a type synonym endowed with the norm coming from the scalar product.

[Michael Rothgang]

:+1: That's what I was also tending towards.

[Dominic Steinitz]

I have almost completed a proof of the existence of a Riemannian metric using your suggestions above.

noncomputable
def riemannian_metric_exists'
    (f : SmoothPartitionOfUnity B IB B)
    (h_sub : f.IsSubordinate (fun x ↦ (extChartAt IB x).source)) :
    ContMDiffRiemannianMetric (IB := IB) (n := ∞) (F := EB)
     (E := @TangentSpace ℝ _ _ _ _ _ _ IB B _ _) :=
  { inner := g_global_bilin f
    symm := riemannian_metric_symm f
    pos := riemannian_metric_pos_def f h_sub
    isVonNBounded := riemannian_unit_ball_bounded f h_sub
    contMDiff := (g_global_smooth_section' f h_sub).contMDiff_toFun
     }

I have

lemma riemannian_unit_ball_bounded (f : SmoothPartitionOfUnity B IB B)
  (h_sub : f.IsSubordinate (fun x ↦ (extChartAt IB x).source)) :
  ∀ (b : B), Bornology.IsVonNBounded ℝ
    {v  : TangentSpace IB b | ((g_global_bilin f b).toFun v).toFun v < 1} := by
  intro b
  have h1 : ∀ (v : TangentSpace IB b), 0 ≤ ((g_global_bilin f b).toFun v).toFun v := by
    intro v
    rcases eq_or_ne v 0 with rfl | hv
    · simp
    · exact le_of_lt (riemannian_metric_pos_def f h_sub b v hv)
  have h2 : ∀ (u v : TangentSpace IB b),
    ((g_global_bilin f b).toFun u).toFun v = ((g_global_bilin f b).toFun v).toFun u := by
    exact fun u v ↦ riemannian_metric_symm f b u v
  exact aux_tvs (g_global_bilin f b) h1 h2

which refers to

lemma aux_tvs {x : B} (φ : TangentSpace IB x →L[ℝ] TangentSpace IB x →L[ℝ] ℝ)
   (hpos : ∀ v, 0 ≤ φ v v) (hsymm : ∀ u v, φ u v = φ v u) :
    Bornology.IsVonNBounded ℝ {v | (φ v) v < 1} := by
  rw [WithSeminorms.isVonNBounded_iff_finset_seminorm_bounded
        (p := aux φ hpos hsymm) (bbr φ hpos hsymm)]
  intro I
  letI J : Finset (Fin 1) := {1}
  suffices ∃ r > 0, ∀ x ∈ {v | (φ v) v < 1}, (J.sup (aux φ hpos hsymm)) x < r by
    obtain (rfl | h) := qux I
    · use 1; simp
    · convert this
  simp only [Set.mem_setOf_eq, Finset.sup_singleton, J]
  refine ⟨1, by norm_num, fun x h ↦ ?_⟩
  simp only [aux, mynorm]
  change Real.sqrt (φ x x) < 1
  rw [Real.sqrt_lt' (by norm_num)]
  simp [h]

which in turn refers to

lemma bbr {x : B} (φ : TangentSpace IB x →L[ℝ] TangentSpace IB x →L[ℝ] ℝ)
 (hpos : ∀ v, 0 ≤ φ v v) (hsymm : ∀ u v, φ u v = φ v u) :
   WithSeminorms (aux φ hpos hsymm) := by
  -- In finite dimension there is a single topological vector space structure...
  -- and mynorm defines a norm, hence a TVS structure.
  exact sorry

But here I am stuck. Does anyone have any suggestions on how prove this remaining sorry?

[Dominic Steinitz]

I am going down the path of @Sébastien Gouëzel and @Michael Rothgang suggestion and defining a custom datatype which is just the original one wrapped and then defining a topology via its norm and showing the 2 topologies are the same.

I have many questions about why all this is necessary but first I would like to finish my proof.

[Dominic Steinitz]

Maybe I misunderstood what you both were saying. I have created this minimum example to illustrate the problem I am running into.

import Mathlib

-- Setup: finite-dimensional normed space
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]

-- We have two norms on E
variable (norm1 norm2 : Seminorm ℝ E)

-- Question: How do we prove that the topologies induced by norm1 and norm2 are equal?
--
-- The suggestion was to use a type synonym with one norm,
-- and LinearMap.continuous_of_finiteDimensional to show the identity is continuous both ways.

structure EAux (E : Type*) where
  point : E

namespace EAux

@[ext]
lemma ext {E : Type*} (a b : EAux E) (h : a.point = b.point) : a = b := by
  cases a; cases b; simp_all

-- Lift algebraic structure
instance {E : Type*} [Zero E] : Zero (EAux E) where zero := ⟨0⟩
instance {E : Type*} [Add E] : Add (EAux E) where add a b := ⟨a.point + b.point⟩
instance {E : Type*} [Neg E] : Neg (EAux E) where neg a := ⟨-a.point⟩
instance {E : Type*} [SMul ℝ E] : SMul ℝ (EAux E) where smul r a := ⟨r • a.point⟩

instance {E : Type*} [AddCommGroup E] : AddCommGroup (EAux E) where
  add_assoc := by sorry
  zero_add := by sorry
  add_zero := by sorry
  add_comm := by sorry
  nsmul := nsmulRec
  zsmul := zsmulRec
  neg_add_cancel := by sorry

instance {E : Type*} [AddCommGroup E] : AddCommMonoid (EAux E) := inferInstance

instance {E : Type*} [AddCommGroup E] [Module ℝ E] : Module ℝ (EAux E) where
  one_smul := by sorry
  mul_smul := by sorry
  smul_zero := by sorry
  smul_add := by sorry
  add_smul := by sorry
  zero_smul := by sorry

instance {E : Type*} [AddCommGroup E] [Module ℝ E] [FiniteDimensional ℝ E] :
    FiniteDimensional ℝ (EAux E) := by sorry

end EAux

-- Define norm1 lifted to EAux E
def norm1Aux (norm1 : Seminorm ℝ E) : Seminorm ℝ (EAux E) where
  toFun a := norm1 a.point
  map_zero' := by sorry
  add_le' := by sorry
  neg' := by sorry
  smul' := by sorry

set_option trace.Meta.synthInstance true
set_option maxHeartbeats 500000

-- Now we want to prove the topologies are equal
example :
    norm1.toSeminormedAddCommGroup.toUniformSpace.toTopologicalSpace =
    norm2.toSeminormedAddCommGroup.toUniformSpace.toTopologicalSpace := by
  -- Install norm1 topology on EAux E
  letI : TopologicalSpace (EAux E) :=
    (norm1Aux norm1).toSeminormedAddCommGroup.toUniformSpace.toTopologicalSpace

  -- Define identity as linear map
  let f : EAux E →ₗ[ℝ] E := {
    toFun := fun a => a.point
    map_add' := by intros; rfl
    map_smul' := by intros; rfl
  }

  -- This times out trying to synthesize IsTopologicalAddGroup, ContinuousSMul, T2Space
  -- if I am reading the trace correctly
  have : Continuous f := LinearMap.continuous_of_finiteDimensional f
  sorry

[Michael Rothgang]

Thanks for making an #mwe, this really helps. I would have imagined something different from what you're doing - this might explain your issues already. In particular,

• you don't need to assume E is a normed space (a TVS suffices; you can copy the variables from my mwe). This might matter because of the below, but it's good to fix regardless.
• you have made a one-field structure; that's not the same as a type synonym. See docs#WithLp for an example of a type synonym: you make a def with the same type as E, and define it as E --- but Lean will treat it differently. Then you can add a normed space instance on the type synonym.
• you don't want to prove that (edit: the topologies induced by) norm1 and norm2 are equal, but that the identity between E and EAux is continuous in either direction.

[Michael Rothgang]

• talking about the equality of two topologies is a bit of a code smell: saying "the identity map is continuous" is often a nicer way to put it.

[Michael Rothgang]

• as for your error: my untested guess is that norm1 and norm2 are norms on E --- so the statement of your example never actually mentions EAux, hence trying to use it in the proof errors. In other words, the first change should probably be to try to prove the right statement.

[Aaron Liu]

Michael Rothgang said:

• talking about the equality of two topologies is a bit of a code smell: saying "the identity map is continuous" is often a nicer way to put it.

Really? I feel like this couldn't possibly be a problem.

[Aaron Liu]

For example, we have docs#induced_iInf stating the equality of two topologies

[Michael Rothgang]

To be clear, that's not a "problem" in this example (but I would still state things differently).

[Dominic Steinitz]

Michael Rothgang said:

Thanks for making an #mwe, this really helps. I would have imagined something different from what you're doing - this might explain your issues already.

Thanks very much for this. I don't have time to work on this today. Can you give a bit more detail on what you imagined rather than what I inferred (incorrectly?).

[Dominic Steinitz]

Is this what you had in mind? EDITED.

import Mathlib

variable {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G] [FiniteDimensional ℝ G]

-- A norm defined from a bilinear form
noncomputable def mynorm (φ : G →L[ℝ] G →L[ℝ] ℝ) : Seminorm ℝ G where
  toFun v := Real.sqrt (φ v v)
  map_zero' := by simp
  add_le' r s := by sorry
  neg' r := by simp
  smul' a v := by simp [← mul_assoc, ← Real.sqrt_mul_self_eq_abs, Real.sqrt_mul (mul_self_nonneg a)]

@[nolint unusedArguments]
def GAux (G : Type*) [AddCommGroup G] [TopologicalSpace G] [Module ℝ G] [FiniteDimensional ℝ G]
   (φ : G →L[ℝ] G →L[ℝ] ℝ) : Type _ := G

instance {φ : G →L[ℝ] G →L[ℝ] ℝ} : AddCommGroup (GAux G φ) := inferInstanceAs (AddCommGroup G)
instance {φ : G →L[ℝ] G →L[ℝ] ℝ} : Module ℝ (GAux G φ) := inferInstanceAs (Module ℝ G)

#check (by infer_instance : TopologicalSpace G)
#synth TopologicalSpace G

variable (φ : G →L[ℝ] G →L[ℝ] ℝ)

noncomputable instance mySbACG {φ : G →L[ℝ] G →L[ℝ] ℝ} : SeminormedAddCommGroup (GAux G φ) :=
  (mynorm φ).toSeminormedAddCommGroup

-- If I comment out the instance `mySbACG` then these fail
-- so I think it is safe to assume the topology on GAux G φ
-- is the one induced by the norm
#check (by infer_instance : TopologicalSpace (GAux G φ))
#synth TopologicalSpace (GAux G φ)

-- Is this useful?
noncomputable instance myNS {φ : G →L[ℝ] G →L[ℝ] ℝ} :
    NormedSpace ℝ (GAux G φ) where
  norm_smul_le a v := by
    have h1 : ‖a • v‖ = Real.sqrt (φ (a • v) (a • v)) := rfl
    have h2 : ‖v‖ = Real.sqrt (φ v v) := rfl
    rw [h1, h2]
    have : φ (a • v) (a • v) = a * a * φ v v := by
      simp
      exact Eq.symm (mul_assoc a a ((φ v) v))
    rw [this]
    simp
    rw [← Real.sqrt_mul_self_eq_abs a, ← Real.sqrt_mul]
    exact mul_self_nonneg a

-- We would like to be able to say???
example : Continuous (id : G → GAux G φ) :=
  LinearMap.continuous_of_finiteDimensional (E := G)
  (F' := GAux G φ) (LinearMap.id : G →ₗ[ℝ] GAux G φ)

example : Continuous (id : GAux G φ → G) :=
  LinearMap.continuous_of_finiteDimensional
  (E := GAux G φ) (F' := G) (LinearMap.id : GAux G φ →ₗ[ℝ] G)

[Michael Rothgang]

I think so, yes!

[Michael Rothgang]

Does this suffice for your application about Riemannian metrics?

[Dominic Steinitz]

No it does not suffice - I get the very interesting type error

Type mismatch
  LinearMap.continuous_of_finiteDimensional LinearMap.id
has type
  @Continuous G (GAux G φ) PseudoMetricSpace.toUniformSpace.toTopologicalSpace
    (@UniformSpace.toTopologicalSpace (GAux G φ)
      (@PseudoMetricSpace.toUniformSpace (GAux G φ) (@SeminormedAddCommGroup.toPseudoMetricSpace (GAux G φ) mySbACG)))
    ⇑LinearMap.id
but is expected to have type
  @Continuous G G PseudoMetricSpace.toUniformSpace.toTopologicalSpace
    (@UniformSpace.toTopologicalSpace G
      (@PseudoMetricSpace.toUniformSpace G
        (@SeminormedAddCommGroup.toPseudoMetricSpace G NormedAddCommGroup.toSeminormedAddCommGroup)))
    id

I think somehow Lean is still inferring both instances - I know it can't really but I can see

(@SeminormedAddCommGroup.toPseudoMetricSpace (GAux G φ) mySbACG)

and

@SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup

Do you not think it is best to avoid a type synonym so nothing extra can be inferred unless I explicitly say so?

Also

example : Continuous (id : GAux G φ → G) :=
  LinearMap.continuous_of_finiteDimensional
  (E := GAux G φ) (F' := G) (LinearMap.id : GAux G φ →ₗ[ℝ] G)

just times out - I imagine it going round in circles.

[Aaron Liu]

It's a bad idea to write (id : GAux G φ → G) since it doesn't typecheck at reducible transparency