Pulling back continuous bilinear maps, and their quadratic maps

A continuous linear map u : W →L[𝕜] V pulls a continuous bilinear map B on V back to the bilinear map B (u ·) (u ·) on W. This operation is itself continuous and linear in B (ContinuousLinearMap.pullbackBilinL), so that it commutes with derivatives of families of bilinear maps, such as the coordinate expressions of metrics. In particular, pulling back each value of a continuous family of multilinear maps valued in bilinear maps, along u in every argument, gives a continuous family (Continuous.pullbackBilinL_compContinuousMultilinearMap). Pulling back along a bijection preserves nondegeneracy (ContinuousLinearMap.injective_bilinearComp).

The quadratic map x ↦ B x x of a continuous bilinear map is Lipschitz on every ball, with a constant proportional to the radius: ‖B x x - B y y‖ ≤ ‖B‖ (‖x‖ + ‖y‖) ‖x - y‖ (ContinuousLinearMap.norm_apply_apply_sub_apply_apply_le). This is the quadratic estimate on the nonlinear terms of an equation that is quadratic in its unknown.

Pulling back along continuous linear equivalences keeps a bilinear map B₀ : V →L V' →L G invertible as a map to the dual (ContinuousLinearMap.IsInvertible.bilinearComp), and it conjugates the comparison operator B₀⁻¹ ∘ B of two such maps by the equivalence in the first slot (ContinuousLinearMap.inverse_bilinearComp_comp_bilinearComp). This is how operators built from a pair of bilinear forms, such as the Morse congruence of a form with a reference form, transform under a linear change of coordinates.

An invertible bilinear map B₀ : V →L V →L G determines adjoints of operators on V: the adjoint ContinuousLinearMap.pairingAdjoint B₀ X is characterized by B₀ (adj X w) w' = B₀ w (X w') (ContinuousLinearMap.IsInvertible.pairingAdjoint_apply). It reverses products, fixes the identity, and tends to the identity as B₀ stays near an invertible map and X tends to the identity. On Banach spaces the comparison operator B₀⁻¹ ∘ B also tends to the identity as both maps tend to the same invertible map (ContinuousLinearMap.IsInvertible.tendsto_inverse_comp).

noncomputable def ContinuousLinearMap.pullbackBilinL {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {V : Type u_2} {W : Type u_3} {G : Type u_4} [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [SeminormedAddCommGroup W] [NormedSpace 𝕜 W] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (u : W →L[𝕜] V) : (V →L[𝕜] V →L[𝕜] G) →L[𝕜] W →L[𝕜] W →L[𝕜] G

Pulling a continuous bilinear map back along a continuous linear map u, B ↦ B (u ·) (u ·), as a continuous linear map in B.

@[simp]

theorem ContinuousLinearMap.pullbackBilinL_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {V : Type u_2} {W : Type u_3} {G : Type u_4} [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [SeminormedAddCommGroup W] [NormedSpace 𝕜 W] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (u : W →L[𝕜] V) (B : V →L[𝕜] V →L[𝕜] G) (v w : W) : ((u.pullbackBilinL B) v) w = (B (u v)) (u w)

theorem ContinuousLinearMap.pullbackBilinL_eq_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {V : Type u_2} {W : Type u_3} {G : Type u_4} [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [SeminormedAddCommGroup W] [NormedSpace 𝕜 W] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (u : W →L[𝕜] V) : u.pullbackBilinL = (compL 𝕜 W (V →L[𝕜] G) (W →L[𝕜] G)) ((compL 𝕜 W V G).flip u) ∘SL (compL 𝕜 W V (V →L[𝕜] G)).flip u

pullbackBilinL u precomposes a bilinear map with u, and then each of its values with u. In this form it is visibly built from u by continuous linear operations, so that, for instance, its regularity in u follows from that of the precomposition maps compL.

theorem ContinuousLinearMap.norm_apply_apply_sub_apply_apply_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {V : Type u_2} {G : Type u_4} [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (B : V →L[𝕜] V →L[𝕜] G) (x y : V) : ‖(B x) x - (B y) y‖ ≤ ‖B‖ * (‖x‖ + ‖y‖) * ‖x - y‖

The quadratic map x ↦ B x x of a continuous bilinear map B satisfies ‖B x x - B y y‖ ≤ ‖B‖ (‖x‖ + ‖y‖) ‖x - y‖.

theorem ContinuousLinearMap.injective_bilinearComp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {V : Type u_2} {W : Type u_3} {G : Type u_4} [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [SeminormedAddCommGroup W] [NormedSpace 𝕜 W] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {B : V →L[𝕜] V →L[𝕜] G} (hB : Function.Injective ⇑B) {u : W →L[𝕜] V} (hu : Function.Bijective ⇑u) : Function.Injective ⇑(B.bilinearComp u u)

Pulling a nondegenerate bilinear map back along a bijective continuous linear map keeps it nondegenerate.

theorem ContinuousLinearMap.IsInvertible.bilinearComp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {V : Type u_2} {W : Type u_3} {G : Type u_4} [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [SeminormedAddCommGroup W] [NormedSpace 𝕜 W] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {V' : Type u_5} {W' : Type u_6} [SeminormedAddCommGroup V'] [NormedSpace 𝕜 V'] [SeminormedAddCommGroup W'] [NormedSpace 𝕜 W'] {B₀ : V →L[𝕜] V' →L[𝕜] G} (hB₀ : B₀.IsInvertible) (e₁ : W ≃L[𝕜] V) (e₂ : W' ≃L[𝕜] V') : (B₀.bilinearComp ↑e₁ ↑e₂).IsInvertible

Pulling a bilinear map that is invertible, as a map to the space of linear maps on its second argument, back along continuous linear equivalences in both arguments keeps it invertible.

theorem ContinuousLinearMap.inverse_bilinearComp_comp_bilinearComp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {V : Type u_2} {W : Type u_3} {G : Type u_4} [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [SeminormedAddCommGroup W] [NormedSpace 𝕜 W] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {V' : Type u_5} {W' : Type u_6} [SeminormedAddCommGroup V'] [NormedSpace 𝕜 V'] [SeminormedAddCommGroup W'] [NormedSpace 𝕜 W'] {B₀ : V →L[𝕜] V' →L[𝕜] G} (hB₀ : B₀.IsInvertible) (B : V →L[𝕜] V' →L[𝕜] G) (e₁ : W ≃L[𝕜] V) (e₂ : W' ≃L[𝕜] V') : (B₀.bilinearComp ↑e₁ ↑e₂).inverse ∘SL B.bilinearComp ↑e₁ ↑e₂ = ↑e₁.symm ∘SL (B₀.inverse ∘SL B) ∘SL ↑e₁

Pulling two bilinear maps back along continuous linear equivalences conjugates their comparison operator B₀⁻¹ ∘ B by the equivalence e₁ in the first argument.

noncomputable def ContinuousLinearMap.pairingAdjoint {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {V : Type u_2} {G : Type u_4} [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (B₀ : V →L[𝕜] V →L[𝕜] G) (X : V →L[𝕜] V) : V →L[𝕜] V

The adjoint of an operator X on V for the pairing B₀, B₀⁻¹ ∘ (· ∘ X) ∘ B₀. When B₀ is invertible it is characterized by B₀ (adj X w) w' = B₀ w (X w') (ContinuousLinearMap.IsInvertible.pairingAdjoint_apply).

theorem ContinuousLinearMap.pairingAdjoint_def {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {V : Type u_2} {G : Type u_4} [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (B₀ : V →L[𝕜] V →L[𝕜] G) (X : V →L[𝕜] V) : B₀.pairingAdjoint X = B₀.inverse ∘SL (compL 𝕜 V V G).flip X ∘SL B₀

The adjoint for the pairing B₀ is B₀⁻¹ ∘ (· ∘ X) ∘ B₀.

@[simp]

theorem ContinuousLinearMap.IsInvertible.pairingAdjoint_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {V : Type u_2} {G : Type u_4} [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {B₀ : V →L[𝕜] V →L[𝕜] G} (hB₀ : B₀.IsInvertible) (X : V →L[𝕜] V) (w w' : V) : (B₀ ((B₀.pairingAdjoint X) w)) w' = (B₀ w) (X w')

The defining property of the adjoint for an invertible pairing.

theorem ContinuousLinearMap.IsInvertible.ext_of_pairing {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {V : Type u_2} {G : Type u_4} [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {B₀ : V →L[𝕜] V →L[𝕜] G} (hB₀ : B₀.IsInvertible) {X Y : V →L[𝕜] V} (h : ∀ (w w' : V), (B₀ (X w)) w' = (B₀ (Y w)) w') : X = Y

Operators are determined by their pairings against an invertible bilinear map.

theorem ContinuousLinearMap.IsInvertible.pairingAdjoint_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {V : Type u_2} {G : Type u_4} [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {B₀ : V →L[𝕜] V →L[𝕜] G} (hB₀ : B₀.IsInvertible) (X Y : V →L[𝕜] V) : B₀.pairingAdjoint (X * Y) = B₀.pairingAdjoint Y * B₀.pairingAdjoint X

The adjoint for an invertible pairing reverses products.

@[simp]

theorem ContinuousLinearMap.IsInvertible.pairingAdjoint_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {V : Type u_2} {G : Type u_4} [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {B₀ : V →L[𝕜] V →L[𝕜] G} (hB₀ : B₀.IsInvertible) : B₀.pairingAdjoint 1 = 1

The adjoint of the identity for an invertible pairing is the identity.

theorem ContinuousLinearMap.IsInvertible.tendsto_inverse_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_5} {F : Type u_6} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {e : E →L[𝕜] F} (he : e.IsInvertible) : Filter.Tendsto (fun (p : (E →L[𝕜] F) × (E →L[𝕜] F)) => p.1.inverse ∘SL p.2) (nhds (e, e)) (nhds 1)

The comparison operator e₀⁻¹ ∘ e tends to the identity as both maps tend to the same invertible map.

theorem ContinuousLinearMap.IsInvertible.tendsto_pairingAdjoint {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_5} {H : Type u_7} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup H] [NormedSpace 𝕜 H] {B₀ : E →L[𝕜] E →L[𝕜] H} (hB₀ : B₀.IsInvertible) : Filter.Tendsto (fun (q : (E →L[𝕜] E →L[𝕜] H) × (E →L[𝕜] E)) => q.1.pairingAdjoint q.2) (nhds (B₀, 1)) (nhds 1)

The adjoint of X for the pairing B₀ tends to the identity as B₀ tends to an invertible pairing and X tends to the identity.

theorem Continuous.pullbackBilinL_compContinuousMultilinearMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {V : Type u_2} {W : Type u_3} {G : Type u_4} [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [SeminormedAddCommGroup W] [NormedSpace 𝕜 W] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {X : Type u_5} {ι : Type u_6} [TopologicalSpace X] {f : X → ContinuousMultilinearMap 𝕜 (fun (x : ι) => V) (V →L[𝕜] V →L[𝕜] G)} (hf : Continuous f) (u : W →L[𝕜] V) : Continuous fun (x : X) => u.pullbackBilinL.compContinuousMultilinearMap ((f x).compContinuousLinearMap fun (x : ι) => u)

Pulling back each value of a continuous family f of multilinear maps valued in bilinear maps, both in its arguments and in its values, along a continuous linear map u gives a continuous family. Applied to iterated derivatives of a family of bilinear forms, this is the pullback of all their coordinate derivatives along u.