Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

IsBoundedLinearMap structure

(𝕜 : Type*) [NormedField 𝕜] {E : Type*} [SeminormedAddCommGroup E]
    [NormedSpace 𝕜 E] {F : Type*} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) : Prop
    extends IsLinearMap 𝕜 f

Full source

/-- A function `f` satisfies `IsBoundedLinearMap 𝕜 f` if it is linear and satisfies the
inequality `‖f x‖ ≤ M * ‖x‖` for some positive constant `M`. -/
structure IsBoundedLinearMap (𝕜 : Type*) [NormedField 𝕜] {E : Type*} [SeminormedAddCommGroup E]
    [NormedSpace 𝕜 E] {F : Type*} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) : Prop
    extends IsLinearMap 𝕜 f where
  bound : ∃ M, 0 < M ∧ ∀ x : E, ‖f x‖ ≤ M * ‖x‖

Bounded Linear Map

Informal description

A function $ f : E \to F $ between seminormed vector spaces over a normed field $ \mathbb{K} $ is called a *bounded linear map* if it is linear and there exists a positive constant $ M $ such that for all $ x \in E $, the inequality $ \|f(x)\| \leq M \cdot \|x\| $ holds.

isBoundedLinearMap_iff theorem

 {f : E → F} : IsBoundedLinearMap 𝕜 f ↔ IsLinearMap 𝕜 f ∧ ∃ M, 0 < M ∧ ∀ x : E, ‖f x‖ ≤ M * ‖x‖

Full source

lemma isBoundedLinearMap_iff {f : E → F} :
    IsBoundedLinearMapIsBoundedLinearMap 𝕜 f ↔ IsLinearMap 𝕜 f ∧ ∃ M, 0 < M ∧ ∀ x : E, ‖f x‖ ≤ M * ‖x‖ :=
  ⟨fun hf ↦ ⟨hf.toIsLinearMap, hf.bound⟩, fun ⟨hl, hm⟩ ↦ ⟨hl, hm⟩⟩

Characterization of Bounded Linear Maps via Norm Bounds

Informal description

A function $ f : E \to F $ between seminormed vector spaces over a normed field $ \mathbb{K} $ is a bounded linear map if and only if it is linear and there exists a positive constant $ M $ such that for all $ x \in E $, the inequality $ \|f(x)\| \leq M \|x\| $ holds.

IsLinearMap.with_bound theorem

 {f : E → F} (hf : IsLinearMap 𝕜 f) (M : ℝ) (h : ∀ x : E, ‖f x‖ ≤ M * ‖x‖) : IsBoundedLinearMap 𝕜 f

Full source

theorem IsLinearMap.with_bound {f : E → F} (hf : IsLinearMap 𝕜 f) (M : ℝ)
    (h : ∀ x : E, ‖f x‖ ≤ M * ‖x‖) : IsBoundedLinearMap 𝕜 f :=
  ⟨hf,
    by_cases
      (fun (this : M ≤ 0) =>
        ⟨1, zero_lt_one, fun x =>
          (h x).trans <| mul_le_mul_of_nonneg_right (this.trans zero_le_one) (norm_nonneg x)⟩)
      fun (this : ¬M ≤ 0) => ⟨M, lt_of_not_ge this, h⟩⟩

Boundedness Criterion for Linear Maps: $\|f(x)\| \leq M\|x\| \implies$ Boundedness

Informal description

Let $E$ and $F$ be seminormed vector spaces over a normed field $\mathbb{K}$. Given a linear map $f \colon E \to F$ and a constant $M \in \mathbb{R}$, if for every $x \in E$ the norm $\|f(x)\|$ is bounded by $M\|x\|$, then $f$ is a bounded linear map.

ContinuousLinearMap.isBoundedLinearMap theorem

(f : E →L[𝕜] F) : IsBoundedLinearMap 𝕜 f

Full source

/-- A continuous linear map satisfies `IsBoundedLinearMap` -/
theorem ContinuousLinearMap.isBoundedLinearMap (f : E →L[𝕜] F) : IsBoundedLinearMap 𝕜 f :=
  { f.toLinearMap.isLinear with bound := f.bound }

Continuous Linear Maps are Bounded

Informal description

Let $E$ and $F$ be seminormed vector spaces over a normed field $\mathbb{K}$. Every continuous linear map $f \colon E \to F$ is a bounded linear map, meaning there exists a constant $M > 0$ such that for all $x \in E$, the inequality $\|f(x)\| \leq M \|x\|$ holds.

IsBoundedLinearMap.toLinearMap definition

(f : E → F) (h : IsBoundedLinearMap 𝕜 f) : E →ₗ[𝕜] F

Full source

/-- Construct a linear map from a function `f` satisfying `IsBoundedLinearMap 𝕜 f`. -/
def toLinearMap (f : E → F) (h : IsBoundedLinearMap 𝕜 f) : E →ₗ[𝕜] F :=
  IsLinearMap.mk' _ h.toIsLinearMap

Linear map associated to a bounded linear map

Informal description

Given a function $ f : E \to F $ between seminormed vector spaces over a normed field $ \mathbb{K} $ that is a bounded linear map, this constructs the corresponding linear map $ E \to F $ in the algebraic sense (without the norm information).

IsBoundedLinearMap.toContinuousLinearMap definition

{f : E → F} (hf : IsBoundedLinearMap 𝕜 f) : E →L[𝕜] F

Full source

/-- Construct a continuous linear map from `IsBoundedLinearMap`. -/
def toContinuousLinearMap {f : E → F} (hf : IsBoundedLinearMap 𝕜 f) : E →L[𝕜] F :=
  { toLinearMap f hf with
    cont :=
      let ⟨C, _, hC⟩ := hf.bound
      AddMonoidHomClass.continuous_of_bound (toLinearMap f hf) C hC }

Continuous linear map associated to a bounded linear map

Informal description

Given a function $ f : E \to F $ between seminormed vector spaces over a normed field $ \mathbb{K} $ that is a bounded linear map (i.e., linear and satisfies $ \|f(x)\| \leq M \cdot \|x\| $ for some constant $ M > 0 $), this constructs the corresponding continuous linear map $ E \to F $.

IsBoundedLinearMap.zero theorem

: IsBoundedLinearMap 𝕜 fun _ : E => (0 : F)

Full source

theorem zero : IsBoundedLinearMap 𝕜 fun _ : E => (0 : F) :=
  (0 : E →ₗ[𝕜] F).isLinear.with_bound 0 <| by simp [le_refl]

Boundedness of the Zero Linear Map

Informal description

The zero map from a seminormed vector space $E$ to a seminormed vector space $F$ over a normed field $\mathbb{K}$, defined by $x \mapsto 0$ for all $x \in E$, is a bounded linear map.

IsBoundedLinearMap.id theorem

: IsBoundedLinearMap 𝕜 fun x : E => x

Full source

theorem id : IsBoundedLinearMap 𝕜 fun x : E => x :=
  LinearMap.id.isLinear.with_bound 1 <| by simp [le_refl]

Boundedness of the Identity Map: $\|\operatorname{id}(x)\| \leq \|x\|$

Informal description

The identity map $\operatorname{id} \colon E \to E$ on a seminormed vector space $E$ over a normed field $\mathbb{K}$ is a bounded linear map. That is, $\operatorname{id}$ is linear and satisfies $\|\operatorname{id}(x)\| \leq 1 \cdot \|x\|$ for all $x \in E$.

IsBoundedLinearMap.fst theorem

: IsBoundedLinearMap 𝕜 fun x : E × F => x.1

Full source

theorem fst : IsBoundedLinearMap 𝕜 fun x : E × F => x.1 := by
  refine (LinearMap.fst 𝕜 E F).isLinear.with_bound 1 fun x => ?_
  rw [one_mul]
  exact le_max_left _ _

Boundedness of the First Projection Map on Seminormed Vector Spaces

Informal description

The first projection map $(x, y) \mapsto x$ from the product $E \times F$ of two seminormed vector spaces over a normed field $\mathbb{K}$ to $E$ is a bounded linear map.

IsBoundedLinearMap.snd theorem

: IsBoundedLinearMap 𝕜 fun x : E × F => x.2

Full source

theorem snd : IsBoundedLinearMap 𝕜 fun x : E × F => x.2 := by
  refine (LinearMap.snd 𝕜 E F).isLinear.with_bound 1 fun x => ?_
  rw [one_mul]
  exact le_max_right _ _

Boundedness of the Second Projection Map on Seminormed Vector Spaces

Informal description

The second projection map $(x, y) \mapsto y$ from the product $E \times F$ of two seminormed vector spaces over a normed field $\mathbb{K}$ to $F$ is a bounded linear map.

IsBoundedLinearMap.smul theorem

(c : 𝕜) (hf : IsBoundedLinearMap 𝕜 f) : IsBoundedLinearMap 𝕜 (c • f)

Full source

theorem smul (c : 𝕜) (hf : IsBoundedLinearMap 𝕜 f) : IsBoundedLinearMap 𝕜 (c • f) :=
  let ⟨hlf, M, _, hM⟩ := hf
  (c • hlf.mk' f).isLinear.with_bound (‖c‖ * M) fun x =>
    calc
      ‖c • f x‖ = ‖c‖ * ‖f x‖ := norm_smul c (f x)
      _ ≤ ‖c‖ * (M * ‖x‖) := mul_le_mul_of_nonneg_left (hM _) (norm_nonneg _)
      _ = ‖c‖ * M * ‖x‖ := (mul_assoc _ _ _).symm

Scalar Multiplication Preserves Bounded Linear Maps

Informal description

Let $\mathbb{K}$ be a normed field, and let $E$ and $F$ be seminormed vector spaces over $\mathbb{K}$. Given a scalar $c \in \mathbb{K}$ and a bounded linear map $f \colon E \to F$, the scalar multiple $c \cdot f$ is also a bounded linear map from $E$ to $F$.

IsBoundedLinearMap.neg theorem

(hf : IsBoundedLinearMap 𝕜 f) : IsBoundedLinearMap 𝕜 fun e => -f e

Full source

theorem neg (hf : IsBoundedLinearMap 𝕜 f) : IsBoundedLinearMap 𝕜 fun e => -f e := by
  rw [show (fun e => -f e) = fun e => (-1 : 𝕜) • f e by funext; simp]
  exact smul (-1) hf

Negation Preserves Bounded Linear Maps

Informal description

Let $E$ and $F$ be seminormed vector spaces over a normed field $\mathbb{K}$. If $f \colon E \to F$ is a bounded linear map, then the negation $-f$, defined by $(-f)(e) = -f(e)$ for all $e \in E$, is also a bounded linear map.

IsBoundedLinearMap.add theorem

(hf : IsBoundedLinearMap 𝕜 f) (hg : IsBoundedLinearMap 𝕜 g) : IsBoundedLinearMap 𝕜 fun e => f e + g e

Full source

theorem add (hf : IsBoundedLinearMap 𝕜 f) (hg : IsBoundedLinearMap 𝕜 g) :
    IsBoundedLinearMap 𝕜 fun e => f e + g e :=
  let ⟨hlf, Mf, _, hMf⟩ := hf
  let ⟨hlg, Mg, _, hMg⟩ := hg
  (hlf.mk' _ + hlg.mk' _).isLinear.with_bound (Mf + Mg) fun x =>
    calc
      ‖f x + g x‖ ≤ Mf * ‖x‖ + Mg * ‖x‖ := norm_add_le_of_le (hMf x) (hMg x)
      _ ≤ (Mf + Mg) * ‖x‖ := by rw [add_mul]

Sum of Bounded Linear Maps is Bounded

Informal description

Let $E$ and $F$ be seminormed vector spaces over a normed field $\mathbb{K}$. If $f, g \colon E \to F$ are bounded linear maps, then their sum $f + g$, defined by $(f + g)(e) = f(e) + g(e)$ for all $e \in E$, is also a bounded linear map.

IsBoundedLinearMap.sub theorem

(hf : IsBoundedLinearMap 𝕜 f) (hg : IsBoundedLinearMap 𝕜 g) : IsBoundedLinearMap 𝕜 fun e => f e - g e

Full source

theorem sub (hf : IsBoundedLinearMap 𝕜 f) (hg : IsBoundedLinearMap 𝕜 g) :
    IsBoundedLinearMap 𝕜 fun e => f e - g e := by simpa [sub_eq_add_neg] using add hf (neg hg)

Difference of Bounded Linear Maps is Bounded

Informal description

Let $E$ and $F$ be seminormed vector spaces over a normed field $\mathbb{K}$. If $f, g \colon E \to F$ are bounded linear maps, then their difference $f - g$, defined by $(f - g)(e) = f(e) - g(e)$ for all $e \in E$, is also a bounded linear map.

IsBoundedLinearMap.comp theorem

{g : F → G} (hg : IsBoundedLinearMap 𝕜 g) (hf : IsBoundedLinearMap 𝕜 f) : IsBoundedLinearMap 𝕜 (g ∘ f)

Full source

theorem comp {g : F → G} (hg : IsBoundedLinearMap 𝕜 g) (hf : IsBoundedLinearMap 𝕜 f) :
    IsBoundedLinearMap 𝕜 (g ∘ f) :=
  (hg.toContinuousLinearMap.comp hf.toContinuousLinearMap).isBoundedLinearMap

Composition of Bounded Linear Maps is Bounded

Informal description

Let $E$, $F$, and $G$ be seminormed vector spaces over a normed field $\mathbb{K}$. If $f \colon E \to F$ and $g \colon F \to G$ are bounded linear maps, then their composition $g \circ f \colon E \to G$ is also a bounded linear map.

IsBoundedLinearMap.tendsto theorem

(x : E) (hf : IsBoundedLinearMap 𝕜 f) : Tendsto f (𝓝 x) (𝓝 (f x))

Full source

protected theorem tendsto (x : E) (hf : IsBoundedLinearMap 𝕜 f) : Tendsto f (𝓝 x) (𝓝 (f x)) :=
  let ⟨hf, M, _, hM⟩ := hf
  tendsto_iff_norm_sub_tendsto_zero.2 <|
    squeeze_zero (fun _ => norm_nonneg _)
      (fun e =>
        calc
          ‖f e - f x‖ = ‖hf.mk' f (e - x)‖ := by rw [(hf.mk' _).map_sub e x]; rfl
          _ ≤ M * ‖e - x‖ := hM (e - x)
          )
      (suffices Tendsto (fun e : E => M * ‖e - x‖) (𝓝 x) (𝓝 (M * 0)) by simpa
      tendsto_const_nhds.mul (tendsto_norm_sub_self _))

Continuity of Bounded Linear Maps

Informal description

Let $E$ and $F$ be seminormed vector spaces over a normed field $\mathbb{K}$, and let $f : E \to F$ be a bounded linear map. Then for any point $x \in E$, the function $f$ is continuous at $x$, meaning that $f(y)$ tends to $f(x)$ as $y$ tends to $x$.

IsBoundedLinearMap.continuous theorem

(hf : IsBoundedLinearMap 𝕜 f) : Continuous f

Full source

theorem continuous (hf : IsBoundedLinearMap 𝕜 f) : Continuous f :=
  continuous_iff_continuousAt.2 fun _ => hf.tendsto _

Continuity of Bounded Linear Maps

Informal description

Let $E$ and $F$ be seminormed vector spaces over a normed field $\mathbb{K}$, and let $f : E \to F$ be a bounded linear map. Then $f$ is continuous.

IsBoundedLinearMap.isLinearMap_and_continuous_iff_isBoundedLinearMap theorem

(f : E → F) : IsLinearMap 𝕜 f ∧ Continuous f ↔ IsBoundedLinearMap 𝕜 f

Full source

/-- A map between normed spaces is linear and continuous if and only if it is bounded. -/
theorem isLinearMap_and_continuous_iff_isBoundedLinearMap (f : E → F) :
    IsLinearMapIsLinearMap 𝕜 f ∧ Continuous fIsLinearMap 𝕜 f ∧ Continuous f ↔ IsBoundedLinearMap 𝕜 f :=
  ⟨fun ⟨hlin, hcont⟩ ↦ ContinuousLinearMap.isBoundedLinearMap
      ⟨⟨⟨f, IsLinearMap.map_add hlin⟩, IsLinearMap.map_smul hlin⟩, hcont⟩,
        fun h_bdd ↦ ⟨h_bdd.toIsLinearMap, h_bdd.continuous⟩⟩

Characterization of Bounded Linear Maps: Linearity and Continuity $\iff$ Boundedness

Informal description

Let $E$ and $F$ be seminormed vector spaces over a normed field $\mathbb{K}$. A function $f : E \to F$ is linear and continuous if and only if it is a bounded linear map, i.e., there exists a constant $M > 0$ such that $\|f(x)\| \leq M \|x\|$ for all $x \in E$.

IsBoundedLinearMap.lim_zero_bounded_linear_map theorem

(hf : IsBoundedLinearMap 𝕜 f) : Tendsto f (𝓝 0) (𝓝 0)

Full source

theorem lim_zero_bounded_linear_map (hf : IsBoundedLinearMap 𝕜 f) : Tendsto f (𝓝 0) (𝓝 0) :=
  (hf.1.mk' _).map_zero ▸ continuous_iff_continuousAt.1 hf.continuous 0

Bounded Linear Maps Preserve Limits at Zero

Informal description

Let $E$ and $F$ be seminormed vector spaces over a normed field $\mathbb{K}$, and let $f : E \to F$ be a bounded linear map. Then $f$ tends to $0$ as $x$ tends to $0$, i.e., $\lim_{x \to 0} f(x) = 0$.

IsBoundedLinearMap.isBigO_id theorem

{f : E → F} (h : IsBoundedLinearMap 𝕜 f) (l : Filter E) : f =O[l] fun x => x

Full source

theorem isBigO_id {f : E → F} (h : IsBoundedLinearMap 𝕜 f) (l : Filter E) : f =O[l] fun x => x :=
  let ⟨_, _, hM⟩ := h.bound
  IsBigO.of_bound _ (mem_of_superset univ_mem fun x _ => hM x)

Bounded Linear Maps are Asymptotically Dominated by the Identity Function

Informal description

Let $E$ and $F$ be seminormed vector spaces over a normed field $\mathbb{K}$, and let $f : E \to F$ be a bounded linear map. Then for any filter $l$ on $E$, the function $f$ is asymptotically bounded by the identity function, i.e., $f(x) = O(\|x\|)$ as $x$ tends along $l$.

IsBoundedLinearMap.isBigO_comp theorem

{E : Type*} {g : F → G} (hg : IsBoundedLinearMap 𝕜 g) {f : E → F} (l : Filter E) : (fun x' => g (f x')) =O[l] f

Full source

theorem isBigO_comp {E : Type*} {g : F → G} (hg : IsBoundedLinearMap 𝕜 g) {f : E → F}
    (l : Filter E) : (fun x' => g (f x')) =O[l] f :=
  (hg.isBigO_id ⊤).comp_tendsto le_top

Composition with Bounded Linear Map Preserves Asymptotic Boundedness

Informal description

Let $E$, $F$, and $G$ be seminormed vector spaces over a normed field $\mathbb{K}$, and let $g : F \to G$ be a bounded linear map. Then for any function $f : E \to F$ and any filter $l$ on $E$, the composition $g \circ f$ is asymptotically bounded by $f$, i.e., $\|g(f(x))\| = O(\|f(x)\|)$ as $x$ tends along $l$.

IsBoundedLinearMap.isBigO_sub theorem

{f : E → F} (h : IsBoundedLinearMap 𝕜 f) (l : Filter E) (x : E) : (fun x' => f (x' - x)) =O[l] fun x' => x' - x

Full source

theorem isBigO_sub {f : E → F} (h : IsBoundedLinearMap 𝕜 f) (l : Filter E) (x : E) :
    (fun x' => f (x' - x)) =O[l] fun x' => x' - x :=
  isBigO_comp h l

Asymptotic Bound for Bounded Linear Maps under Translation

Informal description

Let $E$ and $F$ be seminormed vector spaces over a normed field $\mathbb{K}$, and let $f : E \to F$ be a bounded linear map. Then for any filter $l$ on $E$ and any point $x \in E$, the function $x' \mapsto f(x' - x)$ is asymptotically bounded by $x' \mapsto x' - x$ as $x'$ tends along $l$, i.e., $\|f(x' - x)\| = O(\|x' - x\|)$.

isBoundedLinearMap_prod_multilinear theorem

 {E : ι → Type*} [∀ i, SeminormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)] :
  IsBoundedLinearMap 𝕜 fun p : ContinuousMultilinearMap 𝕜 E F × ContinuousMultilinearMap 𝕜 E G => p.1.prod p.2

Full source

/-- Taking the cartesian product of two continuous multilinear maps is a bounded linear
operation. -/
theorem isBoundedLinearMap_prod_multilinear {E : ι → Type*} [∀ i, SeminormedAddCommGroup (E i)]
    [∀ i, NormedSpace 𝕜 (E i)] :
    IsBoundedLinearMap 𝕜 fun p : ContinuousMultilinearMapContinuousMultilinearMap 𝕜 E F × ContinuousMultilinearMap 𝕜 E G =>
      p.1.prod p.2 :=
  (ContinuousMultilinearMap.prodL 𝕜 E F G).toContinuousLinearEquiv
    |>.toContinuousLinearMap.isBoundedLinearMap

Bounded Linearity of the Cartesian Product Operation on Continuous Multilinear Maps

Informal description

Let $\mathbb{K}$ be a normed field, and let $E_i$ be a family of seminormed vector spaces over $\mathbb{K}$ indexed by $\iota$. For any two continuous multilinear maps $f \colon \prod_{i \in \iota} E_i \to F$ and $g \colon \prod_{i \in \iota} E_i \to G$, the operation that takes the pair $(f, g)$ to the continuous multilinear map $f \times g \colon \prod_{i \in \iota} E_i \to F \times G$ defined by $(f \times g)(x) = (f(x), g(x))$ is a bounded linear map.

isBoundedLinearMap_continuousMultilinearMap_comp_linear theorem

 (g : G →L[𝕜] E) :
  IsBoundedLinearMap 𝕜 fun f : ContinuousMultilinearMap 𝕜 (fun _ : ι => E) F => f.compContinuousLinearMap fun _ => g

Full source

/-- Given a fixed continuous linear map `g`, associating to a continuous multilinear map `f` the
continuous multilinear map `f (g m₁, ..., g mₙ)` is a bounded linear operation. -/
theorem isBoundedLinearMap_continuousMultilinearMap_comp_linear (g : G →L[𝕜] E) :
    IsBoundedLinearMap 𝕜 fun f : ContinuousMultilinearMap 𝕜 (fun _ : ι => E) F =>
      f.compContinuousLinearMap fun _ => g :=
  (ContinuousMultilinearMap.compContinuousLinearMapL (ι := ι) (G := F) (fun _ ↦ g))
    |>.isBoundedLinearMap

Bounded Linearity of Precomposition with a Fixed Continuous Linear Map in Multilinear Maps

Informal description

Let $\mathbb{K}$ be a normed field, $G$ and $E$ be normed vector spaces over $\mathbb{K}$, and $F$ be a seminormed vector space over $\mathbb{K}$. Given a fixed continuous linear map $g \colon G \to E$, the operation that associates to each continuous multilinear map $f \colon \prod_{i \in \iota} E \to F$ the composition $f \circ (g \times \cdots \times g)$ is a bounded linear map from the space of continuous multilinear maps $\prod_{i \in \iota} E \to F$ to the space of continuous multilinear maps $\prod_{i \in \iota} G \to F$.

ContinuousLinearMap.map_add₂ theorem

(f : M →SL[ρ₁₂] F →SL[σ₁₂] G') (x x' : M) (y : F) : f (x + x') y = f x y + f x' y

Full source

theorem map_add₂ (f : M →SL[ρ₁₂] F →SL[σ₁₂] G') (x x' : M) (y : F) :
    f (x + x') y = f x y + f x' y := by rw [f.map_add, add_apply]

Additivity in First Argument for Continuous Bilinear Maps

Informal description

Let $M$, $F$, and $G'$ be normed vector spaces over fields with ring homomorphisms $\rho_{12} \colon R \to S$ and $\sigma_{12} \colon S' \to S''$. For any continuous bilinear map $f \colon M \to_{\mathcal{L}} (F \to_{\mathcal{L}} G')$ and vectors $x, x' \in M$, $y \in F$, we have: \[ f(x + x', y) = f(x, y) + f(x', y). \]

ContinuousLinearMap.map_zero₂ theorem

(f : M →SL[ρ₁₂] F →SL[σ₁₂] G') (y : F) : f 0 y = 0

Full source

theorem map_zero₂ (f : M →SL[ρ₁₂] F →SL[σ₁₂] G') (y : F) : f 0 y = 0 := by
  rw [f.map_zero, zero_apply]

Bilinear map vanishes when first argument is zero

Informal description

Let $M$, $F$, and $G'$ be normed vector spaces over fields with ring homomorphisms $\rho_{12} \colon R \to S$ and $\sigma_{12} \colon S' \to S''$. For any continuous bilinear map $f \colon M \to_{\mathcal{L}} (F \to_{\mathcal{L}} G')$ and vector $y \in F$, we have: \[ f(0, y) = 0. \]

ContinuousLinearMap.map_smulₛₗ₂ theorem

(f : M →SL[ρ₁₂] F →SL[σ₁₂] G') (c : R) (x : M) (y : F) : f (c • x) y = ρ₁₂ c • f x y

Full source

theorem map_smulₛₗ₂ (f : M →SL[ρ₁₂] F →SL[σ₁₂] G') (c : R) (x : M) (y : F) :
    f (c • x) y = ρ₁₂ c • f x y := by rw [f.map_smulₛₗ, smul_apply]

Scalar Multiplication Property of Continuous Bilinear Maps

Informal description

Let $M$, $F$, and $G'$ be normed vector spaces over fields with ring homomorphisms $\rho_{12} : R \to S$ and $\sigma_{12} : S' \to S''$. For any continuous bilinear map $f : M \to_{\mathcal{L}} (F \to_{\mathcal{L}} G')$, scalar $c \in R$, and vectors $x \in M$, $y \in F$, we have: \[ f(c \cdot x)(y) = \rho_{12}(c) \cdot f(x)(y) \]

ContinuousLinearMap.map_sub₂ theorem

(f : M →SL[ρ₁₂] F →SL[σ₁₂] G') (x x' : M) (y : F) : f (x - x') y = f x y - f x' y

Full source

theorem map_sub₂ (f : M →SL[ρ₁₂] F →SL[σ₁₂] G') (x x' : M) (y : F) :
    f (x - x') y = f x y - f x' y := by rw [f.map_sub, sub_apply]

Subtraction property of continuous bilinear maps

Informal description

Let $M$, $F$, and $G'$ be normed vector spaces over fields with appropriate ring homomorphisms $\rho_{12}$ and $\sigma_{12}$. For any continuous bilinear map $f: M \to_{\mathcal{L}} (F \to_{\mathcal{L}} G')$ and vectors $x, x' \in M$, $y \in F$, we have: \[ f(x - x')(y) = f(x)(y) - f(x')(y) \]

ContinuousLinearMap.map_neg₂ theorem

(f : M →SL[ρ₁₂] F →SL[σ₁₂] G') (x : M) (y : F) : f (-x) y = -f x y

Full source

theorem map_neg₂ (f : M →SL[ρ₁₂] F →SL[σ₁₂] G') (x : M) (y : F) : f (-x) y = -f x y := by
  rw [f.map_neg, neg_apply]

Negation property of continuous bilinear maps

Informal description

Let $M$, $F$, and $G'$ be normed vector spaces over fields with appropriate ring homomorphisms $\rho_{12}$ and $\sigma_{12}$. For any continuous bilinear map $f: M \to_{\mathcal{L}} (F \to_{\mathcal{L}} G')$, vector $x \in M$, and vector $y \in F$, we have: \[ f(-x)(y) = -f(x)(y) \]

ContinuousLinearMap.map_smul₂ theorem

(f : E →L[𝕜] F →L[𝕜] G) (c : 𝕜) (x : E) (y : F) : f (c • x) y = c • f x y

Full source

theorem map_smul₂ (f : E →L[𝕜] F →L[𝕜] G) (c : 𝕜) (x : E) (y : F) : f (c • x) y = c • f x y := by
  rw [f.map_smul, smul_apply]

Scalar multiplication property of continuous bilinear maps

Informal description

Let $E$, $F$, and $G$ be normed vector spaces over a field $\mathbb{K}$, and let $f: E \to_{\mathcal{L}} (F \to_{\mathcal{L}} G)$ be a continuous bilinear map. Then for any scalar $c \in \mathbb{K}$ and vectors $x \in E$, $y \in F$, we have the scalar multiplication property: \[ f(c \cdot x)(y) = c \cdot f(x)(y) \]

IsBoundedBilinearMap structure

(f : E × F → G)

Full source

/-- A map `f : E × F → G` satisfies `IsBoundedBilinearMap 𝕜 f` if it is bilinear and
continuous. -/
structure IsBoundedBilinearMap (f : E × F → G) : Prop where
  add_left : ∀ (x₁ x₂ : E) (y : F), f (x₁ + x₂, y) = f (x₁, y) + f (x₂, y)
  smul_left : ∀ (c : 𝕜) (x : E) (y : F), f (c • x, y) = c • f (x, y)
  add_right : ∀ (x : E) (y₁ y₂ : F), f (x, y₁ + y₂) = f (x, y₁) + f (x, y₂)
  smul_right : ∀ (c : 𝕜) (x : E) (y : F), f (x, c • y) = c • f (x, y)
  bound : ∃ C > 0, ∀ (x : E) (y : F), ‖f (x, y)‖ ≤ C * ‖x‖ * ‖y‖

Bounded bilinear map

Informal description

A bilinear map $ f : E \times F \to G $ between normed vector spaces is called *bounded* if there exists a constant $ C $ such that for all $ x \in E $ and $ y \in F $, the norm of $ f(x, y) $ is bounded by $ C \|x\| \|y\| $. This condition implies that $ f $ is continuous.

ContinuousLinearMap.isBoundedBilinearMap theorem

(f : E →L[𝕜] F →L[𝕜] G) : IsBoundedBilinearMap 𝕜 fun x : E × F => f x.1 x.2

Full source

theorem ContinuousLinearMap.isBoundedBilinearMap (f : E →L[𝕜] F →L[𝕜] G) :
    IsBoundedBilinearMap 𝕜 fun x : E × F => f x.1 x.2 :=
  { add_left := f.map_add₂
    smul_left := f.map_smul₂
    add_right := fun x => (f x).map_add
    smul_right := fun c x => (f x).map_smul c
    bound :=
      ⟨max ‖f‖ 1, zero_lt_one.trans_le (le_max_right _ _), fun x y =>
        (f.le_opNorm₂ x y).trans <| by
          apply_rules [mul_le_mul_of_nonneg_right, norm_nonneg, le_max_left] ⟩ }

Continuous Bilinear Maps Induce Bounded Bilinear Maps

Informal description

Let $E$, $F$, and $G$ be normed vector spaces over a field $\mathbb{K}$. For any continuous bilinear map $f \colon E \to_{\mathcal{L}} (F \to_{\mathcal{L}} G)$, the associated map $\tilde{f} \colon E \times F \to G$ defined by $\tilde{f}(x,y) = f(x)(y)$ is a bounded bilinear map. That is, there exists a constant $C > 0$ such that for all $x \in E$ and $y \in F$, we have $\|\tilde{f}(x,y)\| \leq C \|x\| \|y\|$.

IsBoundedBilinearMap.toContinuousLinearMap definition

(hf : IsBoundedBilinearMap 𝕜 f) : E →L[𝕜] F →L[𝕜] G

Full source

/-- A bounded bilinear map `f : E × F → G` defines a continuous linear map
`f : E →L[𝕜] F →L[𝕜] G`. -/
def IsBoundedBilinearMap.toContinuousLinearMap (hf : IsBoundedBilinearMap 𝕜 f) :
    E →L[𝕜] F →L[𝕜] G :=
  LinearMap.mkContinuousOfExistsBound₂
    (LinearMap.mk₂ _ f.curry hf.add_left hf.smul_left hf.add_right hf.smul_right) <|
    hf.bound.imp fun _ ↦ And.right

Continuous linear map induced by a bounded bilinear map

Informal description

Given a bounded bilinear map $ f : E \times F \to G $ between normed vector spaces over a field $\mathbb{K}$, the function `IsBoundedBilinearMap.toContinuousLinearMap` constructs a continuous linear map $ E \to_{L[\mathbb{K}]} (F \to_{L[\mathbb{K}]} G) $. This map sends each $ x \in E $ to the continuous linear map $ f(x, \cdot) : F \to G $, and similarly for $ y \in F $.

IsBoundedBilinearMap.isBigO theorem

(h : IsBoundedBilinearMap 𝕜 f) : f =O[⊤] fun p : E × F => ‖p.1‖ * ‖p.2‖

Full source

protected theorem IsBoundedBilinearMap.isBigO (h : IsBoundedBilinearMap 𝕜 f) :
    f =O[⊤] fun p : E × F => ‖p.1‖ * ‖p.2‖ :=
  let ⟨C, _, hC⟩ := h.bound
  Asymptotics.IsBigO.of_bound C <|
    Filter.Eventually.of_forall fun ⟨x, y⟩ => by simpa [mul_assoc] using hC x y

Norm Bound for Bounded Bilinear Maps

Informal description

Let $E$, $F$, and $G$ be normed vector spaces over a field $\mathbb{K}$, and let $f : E \times F \to G$ be a bounded bilinear map. Then there exists a constant $C > 0$ such that for all $(x, y) \in E \times F$, the norm of $f(x, y)$ satisfies $\|f(x, y)\| \leq C \|x\| \|y\|$.

IsBoundedBilinearMap.isBigO_comp theorem

 {α : Type*} (H : IsBoundedBilinearMap 𝕜 f) {g : α → E} {h : α → F} {l : Filter α} :
  (fun x => f (g x, h x)) =O[l] fun x => ‖g x‖ * ‖h x‖

Full source

theorem IsBoundedBilinearMap.isBigO_comp {α : Type*} (H : IsBoundedBilinearMap 𝕜 f) {g : α → E}
    {h : α → F} {l : Filter α} : (fun x => f (g x, h x)) =O[l] fun x => ‖g x‖ * ‖h x‖ :=
  H.isBigO.comp_tendsto le_top

Asymptotic bound for composition with bounded bilinear map

Informal description

Let $E$, $F$, and $G$ be normed vector spaces over a field $\mathbb{K}$, and let $f : E \times F \to G$ be a bounded bilinear map. For any type $\alpha$ and functions $g : \alpha \to E$, $h : \alpha \to F$, the composition $(x \mapsto f(g(x), h(x)))$ is asymptotically bounded by $(x \mapsto \|g(x)\| \cdot \|h(x)\|)$ with respect to any filter $l$ on $\alpha$.

IsBoundedBilinearMap.isBigO' theorem

(h : IsBoundedBilinearMap 𝕜 f) : f =O[⊤] fun p : E × F => ‖p‖ * ‖p‖

Full source

protected theorem IsBoundedBilinearMap.isBigO' (h : IsBoundedBilinearMap 𝕜 f) :
    f =O[⊤] fun p : E × F => ‖p‖ * ‖p‖ :=
  h.isBigO.trans <|
    (@Asymptotics.isBigO_fst_prod' _ E F _ _ _ _).norm_norm.mul
      (@Asymptotics.isBigO_snd_prod' _ E F _ _ _ _).norm_norm

Norm Bound for Bounded Bilinear Maps in Terms of Product Norm

Informal description

Let $E$, $F$, and $G$ be normed vector spaces over a field $\mathbb{K}$, and let $f : E \times F \to G$ be a bounded bilinear map. Then there exists a constant $C > 0$ such that for all $(x, y) \in E \times F$, the norm of $f(x, y)$ satisfies $\|f(x, y)\| \leq C \|(x, y)\|^2$.

IsBoundedBilinearMap.map_sub_left theorem

(h : IsBoundedBilinearMap 𝕜 f) {x y : E} {z : F} : f (x - y, z) = f (x, z) - f (y, z)

Full source

theorem IsBoundedBilinearMap.map_sub_left (h : IsBoundedBilinearMap 𝕜 f) {x y : E} {z : F} :
    f (x - y, z) = f (x, z) - f (y, z) :=
  (h.toContinuousLinearMap.flip z).map_sub x y

Linearity in the first argument for bounded bilinear maps: $f(x - y, z) = f(x, z) - f(y, z)$

Informal description

Let $E$, $F$, and $G$ be normed vector spaces over a field $\mathbb{K}$, and let $f : E \times F \to G$ be a bounded bilinear map. Then for any $x, y \in E$ and $z \in F$, the map $f$ satisfies the linearity condition in its first argument: \[ f(x - y, z) = f(x, z) - f(y, z). \]

IsBoundedBilinearMap.map_sub_right theorem

(h : IsBoundedBilinearMap 𝕜 f) {x : E} {y z : F} : f (x, y - z) = f (x, y) - f (x, z)

Full source

theorem IsBoundedBilinearMap.map_sub_right (h : IsBoundedBilinearMap 𝕜 f) {x : E} {y z : F} :
    f (x, y - z) = f (x, y) - f (x, z) :=
  (h.toContinuousLinearMap x).map_sub y z

Linearity in the second argument for bounded bilinear maps: $f(x, y - z) = f(x, y) - f(x, z)$

Informal description

Let $E$, $F$, and $G$ be normed vector spaces over a field $\mathbb{K}$, and let $f : E \times F \to G$ be a bounded bilinear map. Then for any $x \in E$ and $y, z \in F$, the map $f$ satisfies the linearity condition in its second argument: \[ f(x, y - z) = f(x, y) - f(x, z). \]

IsBoundedBilinearMap.continuous theorem

(h : IsBoundedBilinearMap 𝕜 f) : Continuous f

Full source

/-- Useful to use together with `Continuous.comp₂`. -/
theorem IsBoundedBilinearMap.continuous (h : IsBoundedBilinearMap 𝕜 f) : Continuous f := by
  refine continuous_iff_continuousAt.2 fun x ↦ tendsto_sub_nhds_zero_iff.1 ?_
  suffices Tendsto (fun y : E × F ↦ f (y.1 - x.1, y.2) + f (x.1, y.2 - x.2)) (𝓝 x) (𝓝 (0 + 0)) by
    simpa only [h.map_sub_left, h.map_sub_right, sub_add_sub_cancel, zero_add] using this
  apply Tendsto.add
  · rw [← isLittleO_one_iff ℝ, ← one_mul 1]
    refine h.isBigO_comp.trans_isLittleO ?_
    refine (IsLittleO.norm_left ?_).mul_isBigO (IsBigO.norm_left ?_)
    · exact (isLittleO_one_iff _).2 (tendsto_sub_nhds_zero_iff.2 (continuous_fst.tendsto _))
    · exact (continuous_snd.tendsto _).isBigO_one ℝ
  · refine Continuous.tendsto' ?_ _ _ (by rw [h.map_sub_right, sub_self])
    exact ((h.toContinuousLinearMap x.1).continuous).comp (continuous_snd.sub continuous_const)

Continuity of bounded bilinear maps

Informal description

Let $E$, $F$, and $G$ be normed vector spaces over a field $\mathbb{K}$, and let $f : E \times F \to G$ be a bounded bilinear map. Then $f$ is continuous.

IsBoundedBilinearMap.continuous_left theorem

(h : IsBoundedBilinearMap 𝕜 f) {e₂ : F} : Continuous fun e₁ => f (e₁, e₂)

Full source

theorem IsBoundedBilinearMap.continuous_left (h : IsBoundedBilinearMap 𝕜 f) {e₂ : F} :
    Continuous fun e₁ => f (e₁, e₂) :=
  h.continuous.comp (continuous_id.prodMk continuous_const)

Continuity in first argument for bounded bilinear maps

Informal description

Let $E$, $F$, and $G$ be normed vector spaces over a field $\mathbb{K}$, and let $f : E \times F \to G$ be a bounded bilinear map. Then for any fixed $e_2 \in F$, the function $e_1 \mapsto f(e_1, e_2)$ is continuous as a function from $E$ to $G$.

IsBoundedBilinearMap.continuous_right theorem

(h : IsBoundedBilinearMap 𝕜 f) {e₁ : E} : Continuous fun e₂ => f (e₁, e₂)

Full source

theorem IsBoundedBilinearMap.continuous_right (h : IsBoundedBilinearMap 𝕜 f) {e₁ : E} :
    Continuous fun e₂ => f (e₁, e₂) :=
  h.continuous.comp (continuous_const.prodMk continuous_id)

Continuity of bounded bilinear maps in the second argument

Informal description

Let $E$, $F$, and $G$ be normed vector spaces over a field $\mathbb{K}$, and let $f : E \times F \to G$ be a bounded bilinear map. For any fixed $e_1 \in E$, the map $e_2 \mapsto f(e_1, e_2)$ is continuous.

ContinuousLinearMap.continuous₂ theorem

(f : E →L[𝕜] F →L[𝕜] G) : Continuous (Function.uncurry fun x y => f x y)

Full source

/-- Useful to use together with `Continuous.comp₂`. -/
theorem ContinuousLinearMap.continuous₂ (f : E →L[𝕜] F →L[𝕜] G) :
    Continuous (Function.uncurry fun x y => f x y) :=
  f.isBoundedBilinearMap.continuous

Continuity of Bilinear Map Associated to Continuous Linear Map

Informal description

Let $E$, $F$, and $G$ be normed vector spaces over a field $\mathbb{K}$. For any continuous bilinear map $f \colon E \to_{\mathcal{L}} (F \to_{\mathcal{L}} G)$, the associated map $\tilde{f} \colon E \times F \to G$ defined by $\tilde{f}(x,y) = f(x)(y)$ is continuous.

IsBoundedBilinearMap.isBoundedLinearMap_left theorem

(h : IsBoundedBilinearMap 𝕜 f) (y : F) : IsBoundedLinearMap 𝕜 fun x => f (x, y)

Full source

theorem IsBoundedBilinearMap.isBoundedLinearMap_left (h : IsBoundedBilinearMap 𝕜 f) (y : F) :
    IsBoundedLinearMap 𝕜 fun x => f (x, y) :=
  (h.toContinuousLinearMap.flip y).isBoundedLinearMap

Left Partial Application of Bounded Bilinear Map is Bounded Linear

Informal description

Let $E$, $F$, and $G$ be normed vector spaces over a normed field $\mathbb{K}$, and let $f : E \times F \to G$ be a bounded bilinear map. For any fixed $y \in F$, the map $x \mapsto f(x, y)$ is a bounded linear map from $E$ to $G$.

IsBoundedBilinearMap.isBoundedLinearMap_right theorem

(h : IsBoundedBilinearMap 𝕜 f) (x : E) : IsBoundedLinearMap 𝕜 fun y => f (x, y)

Full source

theorem IsBoundedBilinearMap.isBoundedLinearMap_right (h : IsBoundedBilinearMap 𝕜 f) (x : E) :
    IsBoundedLinearMap 𝕜 fun y => f (x, y) :=
  (h.toContinuousLinearMap x).isBoundedLinearMap

Right Partial Application of Bounded Bilinear Map is Bounded Linear

Informal description

Let $E$, $F$, and $G$ be normed vector spaces over a normed field $\mathbb{K}$, and let $f : E \times F \to G$ be a bounded bilinear map. For any fixed $x \in E$, the map $y \mapsto f(x, y)$ is a bounded linear map from $F$ to $G$.

isBoundedBilinearMap_smul theorem

 {𝕜' : Type*} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {E : Type*} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
  [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] : IsBoundedBilinearMap 𝕜 fun p : 𝕜' × E => p.1 • p.2

Full source

theorem isBoundedBilinearMap_smul {𝕜' : Type*} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {E : Type*}
    [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] :
    IsBoundedBilinearMap 𝕜 fun p : 𝕜' × E => p.1 • p.2 :=
  (lsmul 𝕜 𝕜' : 𝕜' →L[𝕜] E →L[𝕜] E).isBoundedBilinearMap

Boundedness of Scalar Multiplication in Normed Spaces

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be normed fields with $\mathbb{K}'$ a normed algebra over $\mathbb{K}$. Let $E$ be a seminormed additive commutative group and a normed space over both $\mathbb{K}$ and $\mathbb{K}'$, with the scalar multiplication operations compatible via the scalar tower property. Then the scalar multiplication map $(λ, x) \mapsto λ \cdot x$ from $\mathbb{K}' \times E$ to $E$ is a bounded bilinear map. That is, there exists a constant $C > 0$ such that for all $λ \in \mathbb{K}'$ and $x \in E$, we have $\|λ \cdot x\|_E \leq C \|λ\|_{\mathbb{K}'} \|x\|_E$.

isBoundedBilinearMap_mul theorem

: IsBoundedBilinearMap 𝕜 fun p : 𝕜 × 𝕜 => p.1 * p.2

Full source

theorem isBoundedBilinearMap_mul : IsBoundedBilinearMap 𝕜 fun p : 𝕜 × 𝕜 => p.1 * p.2 := by
  simp_rw [← smul_eq_mul]
  exact isBoundedBilinearMap_smul

Boundedness of Field Multiplication in Normed Fields

Informal description

The multiplication operation $(x, y) \mapsto x * y$ on a normed field $\mathbb{K}$ is a bounded bilinear map. That is, there exists a constant $C > 0$ such that for all $x, y \in \mathbb{K}$, we have $\|x * y\| \leq C \|x\| \|y\|$.

isBoundedBilinearMap_comp theorem

: IsBoundedBilinearMap 𝕜 fun p : (F →L[𝕜] G) × (E →L[𝕜] F) => p.1.comp p.2

Full source

theorem isBoundedBilinearMap_comp :
    IsBoundedBilinearMap 𝕜 fun p : (F →L[𝕜] G) × (E →L[𝕜] F) => p.1.comp p.2 :=
  (compL 𝕜 E F G).isBoundedBilinearMap

Boundedness of Composition of Continuous Linear Maps

Informal description

Let $E$, $F$, and $G$ be normed vector spaces over a field $\mathbb{K}$. The composition map $(g, f) \mapsto g \circ f$ from $(F \to_{\mathcal{L}} G) \times (E \to_{\mathcal{L}} F)$ to $(E \to_{\mathcal{L}} G)$ is a bounded bilinear map. That is, there exists a constant $C > 0$ such that for all continuous linear maps $g \colon F \to G$ and $f \colon E \to F$, we have $\|g \circ f\| \leq C \|g\| \|f\|$.

ContinuousLinearMap.isBoundedLinearMap_comp_left theorem

(g : F →L[𝕜] G) : IsBoundedLinearMap 𝕜 fun f : E →L[𝕜] F => ContinuousLinearMap.comp g f

Full source

theorem ContinuousLinearMap.isBoundedLinearMap_comp_left (g : F →L[𝕜] G) :
    IsBoundedLinearMap 𝕜 fun f : E →L[𝕜] F => ContinuousLinearMap.comp g f :=
  isBoundedBilinearMap_comp.isBoundedLinearMap_right _

Left Composition with Continuous Linear Map is Bounded Linear

Informal description

Let $E$, $F$, and $G$ be normed vector spaces over a normed field $\mathbb{K}$. For any continuous linear map $g \colon F \to G$, the map $f \mapsto g \circ f$ from the space of continuous linear maps $E \to F$ to the space of continuous linear maps $E \to G$ is a bounded linear map. That is, there exists a constant $M > 0$ such that for all $f \colon E \to F$, we have $\|g \circ f\| \leq M \|f\|$.

ContinuousLinearMap.isBoundedLinearMap_comp_right theorem

(f : E →L[𝕜] F) : IsBoundedLinearMap 𝕜 fun g : F →L[𝕜] G => ContinuousLinearMap.comp g f

Full source

theorem ContinuousLinearMap.isBoundedLinearMap_comp_right (f : E →L[𝕜] F) :
    IsBoundedLinearMap 𝕜 fun g : F →L[𝕜] G => ContinuousLinearMap.comp g f :=
  isBoundedBilinearMap_comp.isBoundedLinearMap_left _

Right Composition with Fixed Continuous Linear Map is Bounded Linear

Informal description

Let $E$, $F$, and $G$ be normed vector spaces over a normed field $\mathbb{K}$. For any fixed continuous linear map $f \colon E \to F$, the map $g \mapsto g \circ f$ from the space of continuous linear maps $F \to G$ to the space of continuous linear maps $E \to G$ is a bounded linear map. That is, there exists a constant $C > 0$ such that for all $g \colon F \to G$, we have $\|g \circ f\| \leq C \|g\|$.

isBoundedBilinearMap_apply theorem

: IsBoundedBilinearMap 𝕜 fun p : (E →L[𝕜] F) × E => p.1 p.2

Full source

theorem isBoundedBilinearMap_apply : IsBoundedBilinearMap 𝕜 fun p : (E →L[𝕜] F) × E => p.1 p.2 :=
  (ContinuousLinearMap.flip (apply 𝕜 F : E →L[𝕜] (E →L[𝕜] F) →L[𝕜] F)).isBoundedBilinearMap

Boundedness of the Evaluation Map for Continuous Linear Operators

Informal description

The evaluation map $(f, x) \mapsto f(x)$ from $(E \to_{\mathcal{L}} F) \times E$ to $F$ is a bounded bilinear map, where $E$ and $F$ are normed vector spaces over a field $\mathbb{K}$. That is, there exists a constant $C > 0$ such that for all $f \in E \to_{\mathcal{L}} F$ and $x \in E$, we have $\|f(x)\| \leq C \|f\| \|x\|$.

isBoundedBilinearMap_smulRight theorem

 : IsBoundedBilinearMap 𝕜 fun p => (ContinuousLinearMap.smulRight : (E →L[𝕜] 𝕜) → F → E →L[𝕜] F) p.1 p.2

Full source

/-- The function `ContinuousLinearMap.smulRight`, associating to a continuous linear map
`f : E → 𝕜` and a scalar `c : F` the tensor product `f ⊗ c` as a continuous linear map from `E` to
`F`, is a bounded bilinear map. -/
theorem isBoundedBilinearMap_smulRight :
    IsBoundedBilinearMap 𝕜 fun p =>
      (ContinuousLinearMap.smulRight : (E →L[𝕜] 𝕜) → F → E →L[𝕜] F) p.1 p.2 :=
  (smulRightL 𝕜 E F).isBoundedBilinearMap

Boundedness of the Tensor Product Operation $\mathrm{smulRight}$

Informal description

Let $E$ and $F$ be normed vector spaces over a field $\mathbb{K}$. The operation $\mathrm{smulRight} \colon (E \to_{\mathcal{L}} \mathbb{K}) \times F \to (E \to_{\mathcal{L}} F)$, which associates to a continuous linear map $f \colon E \to \mathbb{K}$ and a vector $c \in F$ the tensor product $f \otimes c$ (interpreted as the continuous linear map $x \mapsto f(x) \cdot c$), is a bounded bilinear map. That is, there exists a constant $C > 0$ such that for all $f \in E \to_{\mathcal{L}} \mathbb{K}$ and $c \in F$, we have $\|\mathrm{smulRight}(f, c)\| \leq C \|f\| \|c\|$.

isBoundedBilinearMap_compMultilinear theorem

 {ι : Type*} {E : ι → Type*} [Fintype ι] [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)] :
  IsBoundedBilinearMap 𝕜 fun p : (F →L[𝕜] G) × ContinuousMultilinearMap 𝕜 E F => p.1.compContinuousMultilinearMap p.2

Full source

/-- The composition of a continuous linear map with a continuous multilinear map is a bounded
bilinear operation. -/
theorem isBoundedBilinearMap_compMultilinear {ι : Type*} {E : ι → Type*} [Fintype ι]
    [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)] :
    IsBoundedBilinearMap 𝕜 fun p : (F →L[𝕜] G) × ContinuousMultilinearMap 𝕜 E F =>
      p.1.compContinuousMultilinearMap p.2 :=
  (compContinuousMultilinearMapL 𝕜 E F G).isBoundedBilinearMap

Bounded Bilinearity of Continuous Linear-Multilinear Composition

Informal description

Let $\mathbb{K}$ be a field, and let $E_i$ for $i \in \iota$ and $F$, $G$ be normed vector spaces over $\mathbb{K}$, where $\iota$ is a finite index set. The composition operation \[ (f, g) \mapsto f \circ g \] for $f \in F \to_{\mathcal{L}} G$ (continuous linear maps from $F$ to $G$) and $g \in \text{ContinuousMultilinearMap}_{\mathbb{K}}(E, F)$ (continuous multilinear maps from $\prod_{i \in \iota} E_i$ to $F$) is a bounded bilinear map. That is, there exists a constant $C > 0$ such that for all such $f$ and $g$, \[ \|f \circ g\| \leq C \|f\| \|g\|. \]

IsBoundedBilinearMap.linearDeriv definition

(h : IsBoundedBilinearMap 𝕜 f) (p : E × F) : E × F →ₗ[𝕜] G

Full source

/-- Definition of the derivative of a bilinear map `f`, given at a point `p` by
`q ↦ f(p.1, q.2) + f(q.1, p.2)` as in the standard formula for the derivative of a product.
We define this function here as a linear map `E × F →ₗ[𝕜] G`, then `IsBoundedBilinearMap.deriv`
strengthens it to a continuous linear map `E × F →L[𝕜] G`.
-/
def IsBoundedBilinearMap.linearDeriv (h : IsBoundedBilinearMap 𝕜 f) (p : E × F) : E × FE × F →ₗ[𝕜] G :=
  (h.toContinuousLinearMap.deriv₂ p).toLinearMap

Linear derivative of a bounded bilinear map

Informal description

Given a bounded bilinear map $ f : E \times F \to G $ between normed vector spaces over a field $\mathbb{K}$ and a point $ p \in E \times F $, the linear derivative of $ f $ at $ p $ is the linear map $ E \times F \to G $ defined by $ (x, y) \mapsto f(p_1, y) + f(x, p_2) $, where $ p = (p_1, p_2) $. This represents the derivative of $ f $ in the sense of linear approximations.

IsBoundedBilinearMap.deriv definition

(h : IsBoundedBilinearMap 𝕜 f) (p : E × F) : E × F →L[𝕜] G

Full source

/-- The derivative of a bounded bilinear map at a point `p : E × F`, as a continuous linear map
from `E × F` to `G`. The statement that this is indeed the derivative of `f` is
`IsBoundedBilinearMap.hasFDerivAt` in `Analysis.Calculus.FDeriv`. -/
def IsBoundedBilinearMap.deriv (h : IsBoundedBilinearMap 𝕜 f) (p : E × F) : E × FE × F →L[𝕜] G :=
  h.toContinuousLinearMap.deriv₂ p

Derivative of a bounded bilinear map

Informal description

Given a bounded bilinear map $ f : E \times F \to G $ between normed vector spaces over a field $\mathbb{K}$, the derivative of $ f $ at a point $ p \in E \times F $ is the continuous linear map $ E \times F \to_{L[\mathbb{K}]} G $ defined by $ (x, y) \mapsto f(x, p.2) + f(p.1, y) $.

IsBoundedBilinearMap.deriv_apply theorem

(h : IsBoundedBilinearMap 𝕜 f) (p q : E × F) : h.deriv p q = f (p.1, q.2) + f (q.1, p.2)

Full source

@[simp]
theorem IsBoundedBilinearMap.deriv_apply (h : IsBoundedBilinearMap 𝕜 f) (p q : E × F) :
    h.deriv p q = f (p.1, q.2) + f (q.1, p.2) :=
  rfl

Derivative Evaluation Formula for Bounded Bilinear Maps

Informal description

Let $E$, $F$, and $G$ be normed vector spaces over a field $\mathbb{K}$, and let $f \colon E \times F \to G$ be a bounded bilinear map. For any points $p = (p_1, p_2)$ and $q = (q_1, q_2)$ in $E \times F$, the derivative of $f$ at $p$ evaluated at $q$ satisfies \[ h.\mathrm{deriv}\, p\, q = f(p_1, q_2) + f(q_1, p_2), \] where $h$ is the proof that $f$ is a bounded bilinear map.

ContinuousLinearMap.mulLeftRight_isBoundedBilinear theorem

 (𝕜' : Type*) [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] :
  IsBoundedBilinearMap 𝕜 fun p : 𝕜' × 𝕜' => ContinuousLinearMap.mulLeftRight 𝕜 𝕜' p.1 p.2

Full source

/-- The function `ContinuousLinearMap.mulLeftRight : 𝕜' × 𝕜' → (𝕜' →L[𝕜] 𝕜')` is a bounded
bilinear map. -/
theorem ContinuousLinearMap.mulLeftRight_isBoundedBilinear (𝕜' : Type*) [SeminormedRing 𝕜']
    [NormedAlgebra 𝕜 𝕜'] :
    IsBoundedBilinearMap 𝕜 fun p : 𝕜' × 𝕜' => ContinuousLinearMap.mulLeftRight 𝕜 𝕜' p.1 p.2 :=
  (ContinuousLinearMap.mulLeftRight 𝕜 𝕜').isBoundedBilinearMap

Bounded Bilinearity of the Left-Right Multiplication Operator

Informal description

Let $\mathbb{K}$ be a normed field and $\mathbb{K}'$ be a seminormed ring with a normed algebra structure over $\mathbb{K}$. The map $\mathrm{mulLeftRight} \colon \mathbb{K}' \times \mathbb{K}' \to (\mathbb{K}' \to_{\mathcal{L}} \mathbb{K}')$ defined by $\mathrm{mulLeftRight}(a, b)(x) = a \cdot x \cdot b$ is a bounded bilinear map. That is, there exists a constant $C > 0$ such that for all $a, b \in \mathbb{K}'$, the operator norm satisfies $\|\mathrm{mulLeftRight}(a, b)\| \leq C \|a\| \|b\|$.

IsBoundedBilinearMap.isBoundedLinearMap_deriv theorem

(h : IsBoundedBilinearMap 𝕜 f) : IsBoundedLinearMap 𝕜 fun p : E × F => h.deriv p

Full source

/-- Given a bounded bilinear map `f`, the map associating to a point `p` the derivative of `f` at
`p` is itself a bounded linear map. -/
theorem IsBoundedBilinearMap.isBoundedLinearMap_deriv (h : IsBoundedBilinearMap 𝕜 f) :
    IsBoundedLinearMap 𝕜 fun p : E × F => h.deriv p :=
  h.toContinuousLinearMap.deriv₂.isBoundedLinearMap

Bounded Linearity of the Derivative Map for Bounded Bilinear Maps

Informal description

Let $ E $, $ F $, and $ G $ be normed vector spaces over a normed field $ \mathbb{K} $, and let $ f : E \times F \to G $ be a bounded bilinear map. Then the map that associates to each point $ p \in E \times F $ the derivative $ h.deriv(p) $ of $ f $ at $ p $ is itself a bounded linear map from $ E \times F $ to the space of continuous linear maps $ E \times F \to_{L[\mathbb{K}]} G $.

Continuous.clm_comp theorem

 {X} [TopologicalSpace X] {g : X → F →L[𝕜] G} {f : X → E →L[𝕜] F} (hg : Continuous g) (hf : Continuous f) :
  Continuous fun x => (g x).comp (f x)

Full source

@[continuity, fun_prop]
theorem Continuous.clm_comp {X} [TopologicalSpace X] {g : X → F →L[𝕜] G} {f : X → E →L[𝕜] F}
    (hg : Continuous g) (hf : Continuous f) : Continuous fun x => (g x).comp (f x) :=
  (compL 𝕜 E F G).continuous₂.comp₂ hg hf

Continuity of Composition of Continuous Linear Maps

Informal description

Let $X$ be a topological space, and let $E$, $F$, and $G$ be normed vector spaces over a field $\mathbb{K}$. Given continuous functions $g \colon X \to (F \to_{\mathcal{L}} G)$ and $f \colon X \to (E \to_{\mathcal{L}} F)$, the function $x \mapsto g(x) \circ f(x)$ from $X$ to $(E \to_{\mathcal{L}} G)$ is continuous.

ContinuousOn.clm_comp theorem

 {X} [TopologicalSpace X] {g : X → F →L[𝕜] G} {f : X → E →L[𝕜] F} {s : Set X} (hg : ContinuousOn g s)
  (hf : ContinuousOn f s) : ContinuousOn (fun x => (g x).comp (f x)) s

Full source

theorem ContinuousOn.clm_comp {X} [TopologicalSpace X] {g : X → F →L[𝕜] G} {f : X → E →L[𝕜] F}
    {s : Set X} (hg : ContinuousOn g s) (hf : ContinuousOn f s) :
    ContinuousOn (fun x => (g x).comp (f x)) s :=
  (compL 𝕜 E F G).continuous₂.comp_continuousOn (hg.prodMk hf)

Continuity of composition of continuous linear maps on a subset

Informal description

Let $X$ be a topological space, and let $E$, $F$, and $G$ be normed vector spaces over a field $\mathbb{K}$. Given continuous functions $g \colon X \to (F \to_{\mathcal{L}} G)$ and $f \colon X \to (E \to_{\mathcal{L}} F)$ defined on a subset $s \subseteq X$, the function $x \mapsto (g x) \circ (f x)$ is continuous on $s$.

Continuous.clm_apply theorem

 {X} [TopologicalSpace X] {f : X → (E →L[𝕜] F)} {g : X → E} (hf : Continuous f) (hg : Continuous g) :
  Continuous (fun x ↦ (f x) (g x))

Full source

@[continuity, fun_prop]
theorem Continuous.clm_apply {X} [TopologicalSpace X] {f : X → (E →L[𝕜] F)} {g : X → E}
    (hf : Continuous f) (hg : Continuous g) : Continuous (fun x ↦ (f x) (g x)) :=
  isBoundedBilinearMap_apply.continuous.comp₂ hf hg

Continuity of Pointwise Application of Continuous Linear Maps

Informal description

Let $X$ be a topological space, $E$ and $F$ be normed vector spaces over a field $\mathbb{K}$, and let $f \colon X \to (E \to_{\mathcal{L}} F)$ and $g \colon X \to E$ be continuous functions. Then the function $x \mapsto f(x)(g(x))$ from $X$ to $F$ is continuous.

ContinuousOn.clm_apply theorem

 {X} [TopologicalSpace X] {f : X → (E →L[𝕜] F)} {g : X → E} {s : Set X} (hf : ContinuousOn f s)
  (hg : ContinuousOn g s) : ContinuousOn (fun x ↦ f x (g x)) s

Full source

theorem ContinuousOn.clm_apply {X} [TopologicalSpace X] {f : X → (E →L[𝕜] F)} {g : X → E}
    {s : Set X} (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
    ContinuousOn (fun x ↦ f x (g x)) s :=
  isBoundedBilinearMap_apply.continuous.comp_continuousOn (hf.prodMk hg)

Continuity of the evaluation map on a subset

Informal description

Let $X$ be a topological space, and let $f \colon X \to (E \to_{\mathcal{L}} F)$ and $g \colon X \to E$ be functions. If $f$ is continuous on a subset $s \subseteq X$ and $g$ is continuous on $s$, then the function $x \mapsto f(x)(g(x))$ is continuous on $s$.

ContinuousLinearEquiv.isOpen theorem

[CompleteSpace E] : IsOpen (range ((↑) : (E ≃L[𝕜] F) → E →L[𝕜] F))

Full source

protected theorem isOpen [CompleteSpace E] : IsOpen (range ((↑) : (E ≃L[𝕜] F) → E →L[𝕜] F)) := by
  rw [isOpen_iff_mem_nhds, forall_mem_range]
  refine fun e => IsOpen.mem_nhds ?_ (mem_range_self _)
  let O : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (e.symm : F →L[𝕜] E).comp f
  have h_O : Continuous O := isBoundedBilinearMap_comp.continuous_right
  convert show IsOpen (O ⁻¹' { x | IsUnit x }) from Units.isOpen.preimage h_O using 1
  ext f'
  constructor
  · rintro ⟨e', rfl⟩
    exact ⟨(e'.trans e.symm).toUnit, rfl⟩
  · rintro ⟨w, hw⟩
    use (unitsEquiv 𝕜 E w).trans e
    ext x
    simp [O, hw]

Openness of Continuous Linear Equivalences Between Banach Spaces

Informal description

Let $E$ and $F$ be Banach spaces over a field $\mathbb{K}$. The set of continuous linear equivalences from $E$ to $F$, considered as a subset of the space of continuous linear maps from $E$ to $F$, is open in the operator norm topology.

ContinuousLinearEquiv.nhds theorem

 [CompleteSpace E] (e : E ≃L[𝕜] F) : range ((↑) : (E ≃L[𝕜] F) → E →L[𝕜] F) ∈ 𝓝 (e : E →L[𝕜] F)

Full source

protected theorem nhds [CompleteSpace E] (e : E ≃L[𝕜] F) :
    rangerange ((↑) : (E ≃L[𝕜] F) → E →L[𝕜] F) ∈ 𝓝 (e : E →L[𝕜] F) :=
  IsOpen.mem_nhds ContinuousLinearEquiv.isOpen (by simp)

Continuous Linear Equivalences Form a Neighborhood in Operator Space

Informal description

Let $E$ and $F$ be Banach spaces over a field $\mathbb{K}$. For any continuous linear equivalence $e \colon E \simeq_{\mathcal{L}} F$, the set of all continuous linear equivalences from $E$ to $F$ is a neighborhood of $e$ in the space of continuous linear maps from $E$ to $F$ with the operator norm topology.

Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

Main definitions

Main theorems

Notes