Documentation

SphereEversion.ToMathlib.Analysis.NormedSpace.OperatorNorm.Prod

source
theorem ContinuousLinearMap.le_opNorm_of_le' {π•œ : Type u_8} {π•œβ‚‚ : Type u_9} {E : Type u_10} {F : Type u_11} [NormedAddCommGroup E] [SeminormedAddCommGroup F] [NontriviallyNormedField π•œ] [NontriviallyNormedField π•œβ‚‚] [NormedSpace π•œ E] [NormedSpace π•œβ‚‚ F] {σ₁₂ : π•œ β†’+* π•œβ‚‚} [RingHomIsometric σ₁₂] (f : E β†’SL[σ₁₂] F) {x : E} (hx : x β‰  0) {C : ℝ} (h : C * β€–xβ€– ≀ β€–f xβ€–) :
C ≀ β€–fβ€–
source
@[simp]
theorem ContinuousLinearMap.toSpanSingleton_zero (π•œ : Type u_8) {E : Type u_9} [SeminormedAddCommGroup E] [NontriviallyNormedField π•œ] [NormedSpace π•œ E] :
toSpanSingleton π•œ 0 = 0
source
@[simp]
theorem ContinuousLinearMap.comp_toSpanSingleton_apply {E : Type u_8} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_9} [NormedAddCommGroup F] [NormedSpace ℝ F] (Ο† : E β†’L[ℝ] ℝ) (v : E) (u : F) :
((toSpanSingleton ℝ u).comp Ο†) v = Ο† v β€’ u
source
def LinearMap.coprodβ‚— (R : Type u₁) (M : Type uβ‚‚) (Mβ‚‚ : Type u₃) (M₃ : Type uβ‚„) [CommRing R] [AddCommMonoid M] [AddCommMonoid Mβ‚‚] [AddCommMonoid M₃] [Module R M] [Module R Mβ‚‚] [Module R M₃] :
(M β†’β‚—[R] M₃) Γ— (Mβ‚‚ β†’β‚—[R] M₃) β†’β‚—[R] M Γ— Mβ‚‚ β†’β‚—[R] M₃

The natural linear map (M β†’β‚—[R] M₃) Γ— (Mβ‚‚ β†’β‚—[R] M₃) β†’β‚—[R] M Γ— Mβ‚‚ β†’β‚—[R] M₃ for R-modules M, Mβ‚‚, M₃ over a commutative ring R.

If f : M β†’β‚—[R] M₃ and g : Mβ‚‚ β†’β‚—[R] M₃ then linear_map.coprodβ‚— (f, g) is the map (m, n) ↦ f m + g n.

Equations
Instances For
    source
    theorem isBoundedLinearMap_coprod (π•œ : Type u_8) [NontriviallyNormedField π•œ] (E : Type u_9) [NormedAddCommGroup E] [NormedSpace π•œ E] (F : Type u_10) [NormedAddCommGroup F] [NormedSpace π•œ F] (G : Type u_11) [NormedAddCommGroup G] [NormedSpace π•œ G] :
    IsBoundedLinearMap π•œ fun (p : (E β†’L[π•œ] G) Γ— (F β†’L[π•œ] G)) => p.1.coprod p.2
    source
    def ContinuousLinearMap.coprodL {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField π•œ] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [NormedSpace π•œ E] [NormedSpace π•œ F] [NormedSpace π•œ G] :
    (E β†’L[π•œ] G) Γ— (F β†’L[π•œ] G) β†’L[π•œ] E Γ— F β†’L[π•œ] G

    The natural continuous linear map ((E β†’L[π•œ] G) Γ— (F β†’L[π•œ] G)) β†’L[π•œ] (E Γ— F β†’L[π•œ] G) for normed spaces E, F, G over a normed field π•œ.

    If g₁ : E β†’L[π•œ] G and gβ‚‚ : F β†’L[π•œ] G then continuous_linear_map.coprodL (g₁, gβ‚‚) is the map (e, f) ↦ g₁ e + gβ‚‚ f.

    Equations
    Instances For
      source
      theorem Continuous.coprodL {π•œ : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {X : Type u_7} [NontriviallyNormedField π•œ] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G] [NormedSpace π•œ E] [NormedSpace π•œ F] [NormedSpace π•œ G] [TopologicalSpace X] {f : X β†’ E β†’L[π•œ] G} {g : X β†’ F β†’L[π•œ] G} (hf : Continuous f) (hg : Continuous g) :
      Continuous fun (x : X) => (f x).coprod (g x)
      source
      theorem Continuous.prodL' {π•œ : Type u_8} {E : Type u_9} {Fβ‚— : Type u_10} {Gβ‚— : Type u_11} [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fβ‚—] [SeminormedAddCommGroup Gβ‚—] [NontriviallyNormedField π•œ] [NormedSpace π•œ E] [NormedSpace π•œ Fβ‚—] [NormedSpace π•œ Gβ‚—] {X : Type u_12} [TopologicalSpace X] {f : X β†’ E β†’L[π•œ] Fβ‚—} {g : X β†’ E β†’L[π•œ] Gβ‚—} (hf : Continuous f) (hg : Continuous g) :
      Continuous fun (x : X) => (f x).prod (g x)
      source
      theorem Continuous.prodL {π•œ : Type u_8} {E : Type u_9} {Fβ‚— : Type u_10} {Gβ‚— : Type u_11} [SeminormedAddCommGroup E] [SeminormedAddCommGroup Fβ‚—] [SeminormedAddCommGroup Gβ‚—] [NontriviallyNormedField π•œ] [NormedSpace π•œ E] [NormedSpace π•œ Fβ‚—] [NormedSpace π•œ Gβ‚—] {X : Type u_12} [TopologicalSpace X] {f : X β†’ E β†’L[π•œ] Fβ‚—} {g : X β†’ E β†’L[π•œ] Gβ‚—} (hf : Continuous f) (hg : Continuous g) :
      Continuous fun (x : X) => (f x).prod (g x)
      source
      theorem ContinuousAt.compL {π•œ : Type u_1} {E : Type u_2} {Fβ‚— : Type u_5} {Gβ‚— : Type u_6} {X : Type u_7} [NontriviallyNormedField π•œ] [NormedAddCommGroup E] [NormedAddCommGroup Fβ‚—] [NormedAddCommGroup Gβ‚—] [NormedSpace π•œ E] [NormedSpace π•œ Fβ‚—] [NormedSpace π•œ Gβ‚—] [TopologicalSpace X] {f : X β†’ Fβ‚— β†’L[π•œ] Gβ‚—} {g : X β†’ E β†’L[π•œ] Fβ‚—} {xβ‚€ : X} (hf : ContinuousAt f xβ‚€) (hg : ContinuousAt g xβ‚€) :
      ContinuousAt (fun (x : X) => (f x).comp (g x)) xβ‚€
      source
      theorem Continuous.compL {π•œ : Type u_1} {E : Type u_2} {Fβ‚— : Type u_5} {Gβ‚— : Type u_6} {X : Type u_7} [NontriviallyNormedField π•œ] [NormedAddCommGroup E] [NormedAddCommGroup Fβ‚—] [NormedAddCommGroup Gβ‚—] [NormedSpace π•œ E] [NormedSpace π•œ Fβ‚—] [NormedSpace π•œ Gβ‚—] [TopologicalSpace X] {f : X β†’ Fβ‚— β†’L[π•œ] Gβ‚—} {g : X β†’ E β†’L[π•œ] Fβ‚—} (hf : Continuous f) (hg : Continuous g) :
      Continuous fun (x : X) => (f x).comp (g x)