analysis.normed.group.hom

source

structure normed_add_group_hom (V : Type u_1) (W : Type u_2) [seminormed_add_comm_group V] [seminormed_add_comm_group W] :

Type (max u_1 u_2)

to_fun : V → W
map_add' : ∀ (v₁ v₂ : V), self.to_fun (v₁ + v₂) = self.to_fun v₁ + self.to_fun v₂
bound' : ∃ (C : ℝ), ∀ (v : V), ‖self.to_fun v‖ ≤ C * ‖v‖

A morphism of seminormed abelian groups is a bounded group homomorphism.

Instances for normed_add_group_hom

source

def add_monoid_hom.mk_normed_add_group_hom {V : Type u_1} {W : Type u_2} [seminormed_add_comm_group V] [seminormed_add_comm_group W] (f : V →+ W) (C : ℝ) (h : ∀ (v : V), ‖⇑f v‖ ≤ C * ‖v‖) :

normed_add_group_hom V W

Associate to a group homomorphism a bounded group homomorphism under a norm control condition.

See add_monoid_hom.mk_normed_add_group_hom' for a version that uses ℝ≥0 for the bound.

Equations

f.mk_normed_add_group_hom C h = {to_fun := f.to_fun, map_add' := _, bound' := _}

source

def add_monoid_hom.mk_normed_add_group_hom' {V : Type u_1} {W : Type u_2} [seminormed_add_comm_group V] [seminormed_add_comm_group W] (f : V →+ W) (C : nnreal) (hC : ∀ (x : V), ‖⇑f x‖₊ ≤ C * ‖x‖₊) :

normed_add_group_hom V W

Associate to a group homomorphism a bounded group homomorphism under a norm control condition.

See add_monoid_hom.mk_normed_add_group_hom for a version that uses ℝ for the bound.

Equations

f.mk_normed_add_group_hom' C hC = {to_fun := f.to_fun, map_add' := _, bound' := _}

source

theorem exists_pos_bound_of_bound {V : Type u_1} {W : Type u_2} [seminormed_add_comm_group V] [seminormed_add_comm_group W] {f : V → W} (M : ℝ) (h : ∀ (x : V), ‖f x‖ ≤ M * ‖x‖) :

∃ (N : ℝ), 0 < N ∧ ∀ (x : V), ‖f x‖ ≤ N * ‖x‖

source

@[protected, instance]

def normed_add_group_hom.has_coe_to_fun {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] :

has_coe_to_fun (normed_add_group_hom V₁ V₂) (λ (_x : normed_add_group_hom V₁ V₂), V₁ → V₂)

Equations

normed_add_group_hom.has_coe_to_fun = {coe := normed_add_group_hom.to_fun _inst_3}

source

theorem normed_add_group_hom.coe_inj {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {f g : normed_add_group_hom V₁ V₂} (H : ⇑f = ⇑g) :

f = g

source

theorem normed_add_group_hom.coe_injective {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] :

function.injective coe_fn

source

theorem normed_add_group_hom.coe_inj_iff {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {f g : normed_add_group_hom V₁ V₂} :

f = g ↔ ⇑f = ⇑g

source

@[ext]

theorem normed_add_group_hom.ext {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {f g : normed_add_group_hom V₁ V₂} (H : ∀ (x : V₁), ⇑f x = ⇑g x) :

f = g

source

theorem normed_add_group_hom.ext_iff {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {f g : normed_add_group_hom V₁ V₂} :

f = g ↔ ∀ (x : V₁), ⇑f x = ⇑g x

source

@[simp]

theorem normed_add_group_hom.to_fun_eq_coe {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) :

f.to_fun = ⇑f

source

@[simp]

theorem normed_add_group_hom.coe_mk {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : V₁ → V₂) (h₁ : ∀ (v₁ v₂ : V₁), f (v₁ + v₂) = f v₁ + f v₂) (h₂ : ℝ) (h₃ : ∀ (v : V₁), ‖f v‖ ≤ h₂ * ‖v‖) :

⇑{to_fun := f, map_add' := h₁, bound' := _} = f

source

@[simp]

theorem normed_add_group_hom.coe_mk_normed_add_group_hom {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : V₁ →+ V₂) (C : ℝ) (hC : ∀ (v : V₁), ‖⇑f v‖ ≤ C * ‖v‖) :

⇑(f.mk_normed_add_group_hom C hC) = ⇑f

source

@[simp]

theorem normed_add_group_hom.coe_mk_normed_add_group_hom' {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : V₁ →+ V₂) (C : nnreal) (hC : ∀ (x : V₁), ‖⇑f x‖₊ ≤ C * ‖x‖₊) :

⇑(f.mk_normed_add_group_hom' C hC) = ⇑f

source

def normed_add_group_hom.to_add_monoid_hom {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) :

V₁ →+ V₂

The group homomorphism underlying a bounded group homomorphism.

Equations

f.to_add_monoid_hom = add_monoid_hom.mk' ⇑f _

source

@[simp]

theorem normed_add_group_hom.coe_to_add_monoid_hom {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) :

⇑(f.to_add_monoid_hom) = ⇑f

source

theorem normed_add_group_hom.to_add_monoid_hom_injective {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] :

function.injective normed_add_group_hom.to_add_monoid_hom

source

@[simp]

theorem normed_add_group_hom.mk_to_add_monoid_hom {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : V₁ → V₂) (h₁ : ∀ (v₁ v₂ : V₁), f (v₁ + v₂) = f v₁ + f v₂) (h₂ : ∃ (C : ℝ), ∀ (v : V₁), ‖f v‖ ≤ C * ‖v‖) :

{to_fun := f, map_add' := h₁, bound' := h₂}.to_add_monoid_hom = add_monoid_hom.mk' f h₁

source

@[protected, instance]

def normed_add_group_hom.add_monoid_hom_class {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] :

add_monoid_hom_class (normed_add_group_hom V₁ V₂) V₁ V₂

Equations

normed_add_group_hom.add_monoid_hom_class = {coe := coe_fn normed_add_group_hom.has_coe_to_fun, coe_injective' := _, map_add := _, map_zero := _}

source

theorem normed_add_group_hom.bound {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) :

∃ (C : ℝ), 0 < C ∧ ∀ (x : V₁), ‖⇑f x‖ ≤ C * ‖x‖

source

theorem normed_add_group_hom.antilipschitz_of_norm_ge {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) {K : nnreal} (h : ∀ (x : V₁), ‖x‖ ≤ ↑K * ‖⇑f x‖) :

antilipschitz_with K ⇑f

source

def normed_add_group_hom.surjective_on_with {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) (K : add_subgroup V₂) (C : ℝ) :

Prop

A normed group hom is surjective on the subgroup K with constant C if every element x of K has a preimage whose norm is bounded above by C*‖x‖. This is a more abstract version of f having a right inverse defined on K with operator norm at most C.

Equations

f.surjective_on_with K C = ∀ (h : V₂), h ∈ K → (∃ (g : V₁), ⇑f g = h ∧ ‖g‖ ≤ C * ‖h‖)

source

theorem normed_add_group_hom.surjective_on_with.mono {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {f : normed_add_group_hom V₁ V₂} {K : add_subgroup V₂} {C C' : ℝ} (h : f.surjective_on_with K C) (H : C ≤ C') :

f.surjective_on_with K C'

source

theorem normed_add_group_hom.surjective_on_with.exists_pos {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {f : normed_add_group_hom V₁ V₂} {K : add_subgroup V₂} {C : ℝ} (h : f.surjective_on_with K C) :

∃ (C' : ℝ) (H : C' > 0), f.surjective_on_with K C'

source

theorem normed_add_group_hom.surjective_on_with.surj_on {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {f : normed_add_group_hom V₁ V₂} {K : add_subgroup V₂} {C : ℝ} (h : f.surjective_on_with K C) :

set.surj_on ⇑f set.univ ↑K

source

noncomputable def normed_add_group_hom.op_norm {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) :

ℝ

The operator norm of a seminormed group homomorphism is the inf of all its bounds.

Equations

f.op_norm = has_Inf.Inf {c : ℝ | 0 ≤ c ∧ ∀ (x : V₁), ‖⇑f x‖ ≤ c * ‖x‖}

source

@[protected, instance]

noncomputable def normed_add_group_hom.has_op_norm {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] :

has_norm (normed_add_group_hom V₁ V₂)

Equations

normed_add_group_hom.has_op_norm = {norm := normed_add_group_hom.op_norm _inst_3}

source

theorem normed_add_group_hom.norm_def {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) :

‖f‖ = has_Inf.Inf {c : ℝ | 0 ≤ c ∧ ∀ (x : V₁), ‖⇑f x‖ ≤ c * ‖x‖}

source

theorem normed_add_group_hom.bounds_nonempty {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {f : normed_add_group_hom V₁ V₂} :

∃ (c : ℝ), c ∈ {c : ℝ | 0 ≤ c ∧ ∀ (x : V₁), ‖⇑f x‖ ≤ c * ‖x‖}

source

theorem normed_add_group_hom.bounds_bdd_below {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {f : normed_add_group_hom V₁ V₂} :

bdd_below {c : ℝ | 0 ≤ c ∧ ∀ (x : V₁), ‖⇑f x‖ ≤ c * ‖x‖}

source

theorem normed_add_group_hom.op_norm_nonneg {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) :

0 ≤ ‖f‖

source

theorem normed_add_group_hom.le_op_norm {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) (x : V₁) :

‖⇑f x‖ ≤ ‖f‖ * ‖x‖

The fundamental property of the operator norm: ‖f x‖ ≤ ‖f‖ * ‖x‖.

source

theorem normed_add_group_hom.le_op_norm_of_le {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) {c : ℝ} {x : V₁} (h : ‖x‖ ≤ c) :

‖⇑f x‖ ≤ ‖f‖ * c

source

theorem normed_add_group_hom.le_of_op_norm_le {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) {c : ℝ} (h : ‖f‖ ≤ c) (x : V₁) :

‖⇑f x‖ ≤ c * ‖x‖

source

theorem normed_add_group_hom.lipschitz {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) :

lipschitz_with ⟨‖f‖, _⟩ ⇑f

continuous linear maps are Lipschitz continuous.

source

@[protected]

theorem normed_add_group_hom.uniform_continuous {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) :

uniform_continuous ⇑f

source

@[protected, continuity]

theorem normed_add_group_hom.continuous {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) :

continuous ⇑f

source

theorem normed_add_group_hom.ratio_le_op_norm {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) (x : V₁) :

‖⇑f x‖ / ‖x‖ ≤ ‖f‖

source

theorem normed_add_group_hom.op_norm_le_bound {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) {M : ℝ} (hMp : 0 ≤ M) (hM : ∀ (x : V₁), ‖⇑f x‖ ≤ M * ‖x‖) :

‖f‖ ≤ M

If one controls the norm of every f x, then one controls the norm of f.

source

theorem normed_add_group_hom.op_norm_eq_of_bounds {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) {M : ℝ} (M_nonneg : 0 ≤ M) (h_above : ∀ (x : V₁), ‖⇑f x‖ ≤ M * ‖x‖) (h_below : ∀ (N : ℝ), N ≥ 0 → (∀ (x : V₁), ‖⇑f x‖ ≤ N * ‖x‖) → M ≤ N) :

‖f‖ = M

source

theorem normed_add_group_hom.op_norm_le_of_lipschitz {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {f : normed_add_group_hom V₁ V₂} {K : nnreal} (hf : lipschitz_with K ⇑f) :

‖f‖ ≤ ↑K

source

theorem normed_add_group_hom.mk_normed_add_group_hom_norm_le {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : V₁ →+ V₂) {C : ℝ} (hC : 0 ≤ C) (h : ∀ (x : V₁), ‖⇑f x‖ ≤ C * ‖x‖) :

‖f.mk_normed_add_group_hom C h‖ ≤ C

If a bounded group homomorphism map is constructed from a group homomorphism via the constructor mk_normed_add_group_hom, then its norm is bounded by the bound given to the constructor if it is nonnegative.

source

theorem normed_add_group_hom.mk_normed_add_group_hom_norm_le' {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : V₁ →+ V₂) {C : ℝ} (h : ∀ (x : V₁), ‖⇑f x‖ ≤ C * ‖x‖) :

‖f.mk_normed_add_group_hom C h‖ ≤ linear_order.max C 0

If a bounded group homomorphism map is constructed from a group homomorphism via the constructor mk_normed_add_group_hom, then its norm is bounded by the bound given to the constructor or zero if this bound is negative.

source

theorem add_monoid_hom.mk_normed_add_group_hom_norm_le {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : V₁ →+ V₂) {C : ℝ} (hC : 0 ≤ C) (h : ∀ (x : V₁), ‖⇑f x‖ ≤ C * ‖x‖) :

‖f.mk_normed_add_group_hom C h‖ ≤ C

Alias of normed_add_group_hom.mk_normed_add_group_hom_norm_le.

source

theorem add_monoid_hom.mk_normed_add_group_hom_norm_le' {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : V₁ →+ V₂) {C : ℝ} (h : ∀ (x : V₁), ‖⇑f x‖ ≤ C * ‖x‖) :

‖f.mk_normed_add_group_hom C h‖ ≤ linear_order.max C 0

Alias of normed_add_group_hom.mk_normed_add_group_hom_norm_le'.

source

@[protected, instance]

noncomputable def normed_add_group_hom.has_add {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] :

has_add (normed_add_group_hom V₁ V₂)

Addition of normed group homs.

Equations

normed_add_group_hom.has_add = {add := λ (f g : normed_add_group_hom V₁ V₂), (f.to_add_monoid_hom + g.to_add_monoid_hom).mk_normed_add_group_hom (‖f‖ + ‖g‖) _}

source

theorem normed_add_group_hom.op_norm_add_le {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f g : normed_add_group_hom V₁ V₂) :

‖f + g‖ ≤ ‖f‖ + ‖g‖

The operator norm satisfies the triangle inequality.

source

def library_note.addition on function coercions :

unit

Terms containing @has_add.add (has_coe_to_fun.F ...) pi.has_add seem to cause leanchecker to crash due to an out-of-memory condition. As a workaround, we add a type annotation: (f + g : V₁ → V₂)

source

@[simp]

theorem normed_add_group_hom.coe_add {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f g : normed_add_group_hom V₁ V₂) :

⇑(f + g) = ⇑f + ⇑g

source

@[simp]

theorem normed_add_group_hom.add_apply {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f g : normed_add_group_hom V₁ V₂) (v : V₁) :

⇑(f + g) v = ⇑f v + ⇑g v

source

@[protected, instance]

def normed_add_group_hom.has_zero {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] :

has_zero (normed_add_group_hom V₁ V₂)

Equations

normed_add_group_hom.has_zero = {zero := 0.mk_normed_add_group_hom 0 normed_add_group_hom.has_zero._proof_1}

source

@[protected, instance]

def normed_add_group_hom.inhabited {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] :

inhabited (normed_add_group_hom V₁ V₂)

Equations

normed_add_group_hom.inhabited = {default := 0}

source

theorem normed_add_group_hom.op_norm_zero {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] :

‖0‖ = 0

The norm of the 0 operator is 0.

source

theorem normed_add_group_hom.op_norm_zero_iff {V₁ : Type u_1} {V₂ : Type u_2} [normed_add_comm_group V₁] [normed_add_comm_group V₂] {f : normed_add_group_hom V₁ V₂} :

‖f‖ = 0 ↔ f = 0

For normed groups, an operator is zero iff its norm vanishes.

source

@[simp]

theorem normed_add_group_hom.coe_zero {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] :

⇑0 = 0

source

@[simp]

theorem normed_add_group_hom.zero_apply {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (v : V₁) :

⇑0 v = 0

source

@[simp]

theorem normed_add_group_hom.id_apply (V : Type u_1) [seminormed_add_comm_group V] (ᾰ : V) :

⇑(normed_add_group_hom.id V) ᾰ = ᾰ

source

def normed_add_group_hom.id (V : Type u_1) [seminormed_add_comm_group V] :

normed_add_group_hom V V

The identity as a continuous normed group hom.

Equations

normed_add_group_hom.id V = (add_monoid_hom.id V).mk_normed_add_group_hom 1 _

source

theorem normed_add_group_hom.norm_id_le (V : Type u_1) [seminormed_add_comm_group V] :

‖normed_add_group_hom.id V‖ ≤ 1

The norm of the identity is at most 1. It is in fact 1, except when the norm of every element vanishes, where it is 0. (Since we are working with seminorms this can happen even if the space is non-trivial.) It means that one can not do better than an inequality in general.

source

theorem normed_add_group_hom.norm_id_of_nontrivial_seminorm (V : Type u_1) [seminormed_add_comm_group V] (h : ∃ (x : V), ‖x‖ ≠ 0) :

‖normed_add_group_hom.id V‖ = 1

If there is an element with norm different from 0, then the norm of the identity equals 1. (Since we are working with seminorms supposing that the space is non-trivial is not enough.)

source

theorem normed_add_group_hom.norm_id {V : Type u_1} [normed_add_comm_group V] [nontrivial V] :

‖normed_add_group_hom.id V‖ = 1

If a normed space is non-trivial, then the norm of the identity equals 1.

source

theorem normed_add_group_hom.coe_id (V : Type u_1) [seminormed_add_comm_group V] :

⇑(normed_add_group_hom.id V) = id

source

@[protected, instance]

noncomputable def normed_add_group_hom.has_neg {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] :

has_neg (normed_add_group_hom V₁ V₂)

Opposite of a normed group hom.

Equations

normed_add_group_hom.has_neg = {neg := λ (f : normed_add_group_hom V₁ V₂), (-f.to_add_monoid_hom).mk_normed_add_group_hom ‖f‖ _}

source

@[simp]

theorem normed_add_group_hom.coe_neg {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) :

⇑-f = -⇑f

source

@[simp]

theorem normed_add_group_hom.neg_apply {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) (v : V₁) :

(⇑-f) v = -⇑f v

source

theorem normed_add_group_hom.op_norm_neg {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) :

‖-f‖ = ‖f‖

source

@[protected, instance]

def normed_add_group_hom.has_sub {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] :

has_sub (normed_add_group_hom V₁ V₂)

Subtraction of normed group homs.

Equations

normed_add_group_hom.has_sub = {sub := λ (f g : normed_add_group_hom V₁ V₂), {to_fun := (f.to_add_monoid_hom - g.to_add_monoid_hom).to_fun, map_add' := _, bound' := _}}

source

@[simp]

theorem normed_add_group_hom.coe_sub {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f g : normed_add_group_hom V₁ V₂) :

⇑(f - g) = ⇑f - ⇑g

source

@[simp]

theorem normed_add_group_hom.sub_apply {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f g : normed_add_group_hom V₁ V₂) (v : V₁) :

⇑(f - g) v = ⇑f v - ⇑g v

source

@[protected, instance]

def normed_add_group_hom.has_smul {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {R : Type u_5} [monoid_with_zero R] [distrib_mul_action R V₂] [pseudo_metric_space R] [has_bounded_smul R V₂] :

has_smul R (normed_add_group_hom V₁ V₂)

Equations

normed_add_group_hom.has_smul = {smul := λ (r : R) (f : normed_add_group_hom V₁ V₂), {to_fun := r • ⇑f, map_add' := _, bound' := _}}

source

@[simp]

theorem normed_add_group_hom.coe_smul {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {R : Type u_5} [monoid_with_zero R] [distrib_mul_action R V₂] [pseudo_metric_space R] [has_bounded_smul R V₂] (r : R) (f : normed_add_group_hom V₁ V₂) :

⇑(r • f) = r • ⇑f

source

@[simp]

theorem normed_add_group_hom.smul_apply {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {R : Type u_5} [monoid_with_zero R] [distrib_mul_action R V₂] [pseudo_metric_space R] [has_bounded_smul R V₂] (r : R) (f : normed_add_group_hom V₁ V₂) (v : V₁) :

⇑(r • f) v = r • ⇑f v

source

@[protected, instance]

def normed_add_group_hom.smul_comm_class {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {R : Type u_5} {R' : Type u_6} [monoid_with_zero R] [distrib_mul_action R V₂] [pseudo_metric_space R] [has_bounded_smul R V₂] [monoid_with_zero R'] [distrib_mul_action R' V₂] [pseudo_metric_space R'] [has_bounded_smul R' V₂] [smul_comm_class R R' V₂] :

smul_comm_class R R' (normed_add_group_hom V₁ V₂)

source

@[protected, instance]

def normed_add_group_hom.is_scalar_tower {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {R : Type u_5} {R' : Type u_6} [monoid_with_zero R] [distrib_mul_action R V₂] [pseudo_metric_space R] [has_bounded_smul R V₂] [monoid_with_zero R'] [distrib_mul_action R' V₂] [pseudo_metric_space R'] [has_bounded_smul R' V₂] [has_smul R R'] [is_scalar_tower R R' V₂] :

is_scalar_tower R R' (normed_add_group_hom V₁ V₂)

source

@[protected, instance]

def normed_add_group_hom.is_central_scalar {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {R : Type u_5} [monoid_with_zero R] [distrib_mul_action R V₂] [pseudo_metric_space R] [has_bounded_smul R V₂] [distrib_mul_action Rᵐᵒᵖ V₂] [is_central_scalar R V₂] :

is_central_scalar R (normed_add_group_hom V₁ V₂)

source

@[protected, instance]

def normed_add_group_hom.has_nat_scalar {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] :

has_smul ℕ (normed_add_group_hom V₁ V₂)

Equations

normed_add_group_hom.has_nat_scalar = {smul := λ (n : ℕ) (f : normed_add_group_hom V₁ V₂), {to_fun := n • ⇑f, map_add' := _, bound' := _}}

source

@[simp]

theorem normed_add_group_hom.coe_nsmul {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (r : ℕ) (f : normed_add_group_hom V₁ V₂) :

⇑(r • f) = r • ⇑f

source

@[simp]

theorem normed_add_group_hom.nsmul_apply {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (r : ℕ) (f : normed_add_group_hom V₁ V₂) (v : V₁) :

⇑(r • f) v = r • ⇑f v

source

@[protected, instance]

def normed_add_group_hom.has_int_scalar {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] :

has_smul ℤ (normed_add_group_hom V₁ V₂)

Equations

normed_add_group_hom.has_int_scalar = {smul := λ (z : ℤ) (f : normed_add_group_hom V₁ V₂), {to_fun := z • ⇑f, map_add' := _, bound' := _}}

source

@[simp]

theorem normed_add_group_hom.coe_zsmul {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (r : ℤ) (f : normed_add_group_hom V₁ V₂) :

⇑(r • f) = r • ⇑f

source

@[simp]

theorem normed_add_group_hom.zsmul_apply {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (r : ℤ) (f : normed_add_group_hom V₁ V₂) (v : V₁) :

⇑(r • f) v = r • ⇑f v

source

@[protected, instance]

noncomputable def normed_add_group_hom.add_comm_group {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] :

add_comm_group (normed_add_group_hom V₁ V₂)

Homs between two given normed groups form a commutative additive group.

Equations

normed_add_group_hom.add_comm_group = function.injective.add_comm_group coe_fn normed_add_group_hom.coe_injective normed_add_group_hom.add_comm_group._proof_1 normed_add_group_hom.add_comm_group._proof_2 normed_add_group_hom.add_comm_group._proof_3 normed_add_group_hom.add_comm_group._proof_4 normed_add_group_hom.add_comm_group._proof_5 normed_add_group_hom.add_comm_group._proof_6

source

@[protected, instance]

noncomputable def normed_add_group_hom.to_seminormed_add_comm_group {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] :

seminormed_add_comm_group (normed_add_group_hom V₁ V₂)

Normed group homomorphisms themselves form a seminormed group with respect to the operator norm.

Equations

normed_add_group_hom.to_seminormed_add_comm_group = {to_fun := normed_add_group_hom.op_norm _inst_3, map_zero' := _, add_le' := _, neg' := _}.to_seminormed_add_comm_group

source

@[protected, instance]

noncomputable def normed_add_group_hom.to_normed_add_comm_group {V₁ : Type u_1} {V₂ : Type u_2} [normed_add_comm_group V₁] [normed_add_comm_group V₂] :

normed_add_comm_group (normed_add_group_hom V₁ V₂)

Normed group homomorphisms themselves form a normed group with respect to the operator norm.

Equations

normed_add_group_hom.to_normed_add_comm_group = {to_fun := normed_add_group_hom.op_norm normed_add_comm_group.to_seminormed_add_comm_group, map_zero' := _, add_le' := _, neg' := _, eq_zero_of_map_eq_zero' := _}.to_normed_add_comm_group

source

def normed_add_group_hom.coe_fn_add_hom {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] :

normed_add_group_hom V₁ V₂ →+ V₁ → V₂

Coercion of a normed_add_group_hom is an add_monoid_hom. Similar to add_monoid_hom.coe_fn.

Equations

normed_add_group_hom.coe_fn_add_hom = {to_fun := coe_fn normed_add_group_hom.has_coe_to_fun, map_zero' := _, map_add' := _}

source

@[simp]

theorem normed_add_group_hom.coe_fn_add_hom_apply {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (x : normed_add_group_hom V₁ V₂) (ᾰ : V₁) :

⇑normed_add_group_hom.coe_fn_add_hom x ᾰ = ⇑x ᾰ

source

@[simp]

theorem normed_add_group_hom.coe_sum {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {ι : Type u_1} (s : finset ι) (f : ι → normed_add_group_hom V₁ V₂) :

⇑(s.sum (λ (i : ι), f i)) = s.sum (λ (i : ι), ⇑(f i))

source

theorem normed_add_group_hom.sum_apply {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {ι : Type u_1} (s : finset ι) (f : ι → normed_add_group_hom V₁ V₂) (v : V₁) :

⇑(s.sum (λ (i : ι), f i)) v = s.sum (λ (i : ι), ⇑(f i) v)

source

@[protected, instance]

noncomputable def normed_add_group_hom.distrib_mul_action {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {R : Type u_1} [monoid_with_zero R] [distrib_mul_action R V₂] [pseudo_metric_space R] [has_bounded_smul R V₂] :

distrib_mul_action R (normed_add_group_hom V₁ V₂)

Equations

normed_add_group_hom.distrib_mul_action = function.injective.distrib_mul_action normed_add_group_hom.coe_fn_add_hom normed_add_group_hom.coe_injective normed_add_group_hom.coe_smul

source

@[protected, instance]

noncomputable def normed_add_group_hom.module {V₁ : Type u_2} {V₂ : Type u_3} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {R : Type u_1} [semiring R] [module R V₂] [pseudo_metric_space R] [has_bounded_smul R V₂] :

module R (normed_add_group_hom V₁ V₂)

Equations

normed_add_group_hom.module = function.injective.module R normed_add_group_hom.coe_fn_add_hom normed_add_group_hom.coe_injective normed_add_group_hom.module._proof_1

source

@[protected]

noncomputable def normed_add_group_hom.comp {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] (g : normed_add_group_hom V₂ V₃) (f : normed_add_group_hom V₁ V₂) :

normed_add_group_hom V₁ V₃

The composition of continuous normed group homs.

Equations

g.comp f = (g.to_add_monoid_hom.comp f.to_add_monoid_hom).mk_normed_add_group_hom (‖g‖ * ‖f‖) _

source

@[simp]

theorem normed_add_group_hom.comp_apply {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] (g : normed_add_group_hom V₂ V₃) (f : normed_add_group_hom V₁ V₂) (ᾰ : V₁) :

⇑(g.comp f) ᾰ = ⇑g (⇑f ᾰ)

source

theorem normed_add_group_hom.norm_comp_le {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] (g : normed_add_group_hom V₂ V₃) (f : normed_add_group_hom V₁ V₂) :

‖g.comp f‖ ≤ ‖g‖ * ‖f‖

source

theorem normed_add_group_hom.norm_comp_le_of_le {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] {f : normed_add_group_hom V₁ V₂} {g : normed_add_group_hom V₂ V₃} {C₁ C₂ : ℝ} (hg : ‖g‖ ≤ C₂) (hf : ‖f‖ ≤ C₁) :

‖g.comp f‖ ≤ C₂ * C₁

source

theorem normed_add_group_hom.norm_comp_le_of_le' {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] {f : normed_add_group_hom V₁ V₂} {g : normed_add_group_hom V₂ V₃} (C₁ C₂ C₃ : ℝ) (h : C₃ = C₂ * C₁) (hg : ‖g‖ ≤ C₂) (hf : ‖f‖ ≤ C₁) :

‖g.comp f‖ ≤ C₃

source

noncomputable def normed_add_group_hom.comp_hom {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] :

normed_add_group_hom V₂ V₃ →+ normed_add_group_hom V₁ V₂ →+ normed_add_group_hom V₁ V₃

Composition of normed groups hom as an additive group morphism.

Equations

normed_add_group_hom.comp_hom = add_monoid_hom.mk' (λ (g : normed_add_group_hom V₂ V₃), add_monoid_hom.mk' (λ (f : normed_add_group_hom V₁ V₂), g.comp f) _) normed_add_group_hom.comp_hom._proof_2

source

@[simp]

theorem normed_add_group_hom.comp_zero {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] (f : normed_add_group_hom V₂ V₃) :

f.comp 0 = 0

source

@[simp]

theorem normed_add_group_hom.zero_comp {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] (f : normed_add_group_hom V₁ V₂) :

0.comp f = 0

source

theorem normed_add_group_hom.comp_assoc {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] {V₄ : Type u_1} [seminormed_add_comm_group V₄] (h : normed_add_group_hom V₃ V₄) (g : normed_add_group_hom V₂ V₃) (f : normed_add_group_hom V₁ V₂) :

(h.comp g).comp f = h.comp (g.comp f)

source

theorem normed_add_group_hom.coe_comp {V₁ : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] (f : normed_add_group_hom V₁ V₂) (g : normed_add_group_hom V₂ V₃) :

⇑(g.comp f) = ⇑g ∘ ⇑f

source

def normed_add_group_hom.incl {V : Type u_1} [seminormed_add_comm_group V] (s : add_subgroup V) :

normed_add_group_hom ↥s V

The inclusion of an add_subgroup, as bounded group homomorphism.

Equations

normed_add_group_hom.incl s = {to_fun := coe coe_to_lift, map_add' := _, bound' := _}

source

@[simp]

theorem normed_add_group_hom.incl_apply {V : Type u_1} [seminormed_add_comm_group V] (s : add_subgroup V) (ᾰ : ↥s) :

⇑(normed_add_group_hom.incl s) ᾰ = ↑ᾰ

source

theorem normed_add_group_hom.norm_incl {V : Type u_1} [seminormed_add_comm_group V] {V' : add_subgroup V} (x : ↥V') :

‖⇑(normed_add_group_hom.incl V') x‖ = ‖x‖

source

def normed_add_group_hom.ker {V₁ : Type u_3} {V₂ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) :

add_subgroup V₁

The kernel of a bounded group homomorphism. Naturally endowed with a seminormed_add_comm_group instance.

Equations

f.ker = f.to_add_monoid_hom.ker

source

theorem normed_add_group_hom.mem_ker {V₁ : Type u_3} {V₂ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) (v : V₁) :

v ∈ f.ker ↔ ⇑f v = 0

source

@[simp]

theorem normed_add_group_hom.ker.lift_apply_coe {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] (f : normed_add_group_hom V₁ V₂) (g : normed_add_group_hom V₂ V₃) (h : g.comp f = 0) (v : V₁) :

↑(⇑(normed_add_group_hom.ker.lift f g h) v) = ⇑f v

source

def normed_add_group_hom.ker.lift {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] (f : normed_add_group_hom V₁ V₂) (g : normed_add_group_hom V₂ V₃) (h : g.comp f = 0) :

normed_add_group_hom V₁ ↥(g.ker)

Given a normed group hom f : V₁ → V₂ satisfying g.comp f = 0 for some g : V₂ → V₃, the corestriction of f to the kernel of g.

Equations

normed_add_group_hom.ker.lift f g h = {to_fun := λ (v : V₁), ⟨⇑f v, _⟩, map_add' := _, bound' := _}

source

@[simp]

theorem normed_add_group_hom.ker.incl_comp_lift {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] (f : normed_add_group_hom V₁ V₂) (g : normed_add_group_hom V₂ V₃) (h : g.comp f = 0) :

(normed_add_group_hom.incl g.ker).comp (normed_add_group_hom.ker.lift f g h) = f

source

@[simp]

theorem normed_add_group_hom.ker_zero {V₁ : Type u_3} {V₂ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] :

0.ker = ⊤

source

theorem normed_add_group_hom.coe_ker {V₁ : Type u_3} {V₂ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) :

↑(f.ker) = ⇑f ⁻¹' {0}

source

theorem normed_add_group_hom.is_closed_ker {V₁ : Type u_3} [seminormed_add_comm_group V₁] {V₂ : Type u_1} [normed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) :

is_closed ↑(f.ker)

source

def normed_add_group_hom.range {V₁ : Type u_3} {V₂ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) :

add_subgroup V₂

The image of a bounded group homomorphism. Naturally endowed with a seminormed_add_comm_group instance.

Equations

f.range = f.to_add_monoid_hom.range

source

theorem normed_add_group_hom.mem_range {V₁ : Type u_3} {V₂ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) (v : V₂) :

v ∈ f.range ↔ ∃ (w : V₁), ⇑f w = v

source

@[simp]

theorem normed_add_group_hom.mem_range_self {V₁ : Type u_3} {V₂ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) (v : V₁) :

⇑f v ∈ f.range

source

theorem normed_add_group_hom.comp_range {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] (f : normed_add_group_hom V₁ V₂) (g : normed_add_group_hom V₂ V₃) :

(g.comp f).range = add_subgroup.map g.to_add_monoid_hom f.range

source

theorem normed_add_group_hom.incl_range {V₁ : Type u_3} [seminormed_add_comm_group V₁] (s : add_subgroup V₁) :

(normed_add_group_hom.incl s).range = s

source

@[simp]

theorem normed_add_group_hom.range_comp_incl_top {V₁ : Type u_3} {V₂ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) :

(f.comp (normed_add_group_hom.incl ⊤)).range = f.range

source

def normed_add_group_hom.norm_noninc {V : Type u_1} {W : Type u_2} [seminormed_add_comm_group V] [seminormed_add_comm_group W] (f : normed_add_group_hom V W) :

Prop

A normed_add_group_hom is norm-nonincreasing if ‖f v‖ ≤ ‖v‖ for all v.

Equations

f.norm_noninc = ∀ (v : V), ‖⇑f v‖ ≤ ‖v‖

source

theorem normed_add_group_hom.norm_noninc.norm_noninc_iff_norm_le_one {V : Type u_1} {W : Type u_2} [seminormed_add_comm_group V] [seminormed_add_comm_group W] {f : normed_add_group_hom V W} :

f.norm_noninc ↔ ‖f‖ ≤ 1

source

theorem normed_add_group_hom.norm_noninc.zero {V₁ : Type u_3} {V₂ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] :

0.norm_noninc

source

theorem normed_add_group_hom.norm_noninc.id {V : Type u_1} [seminormed_add_comm_group V] :

(normed_add_group_hom.id V).norm_noninc

source

theorem normed_add_group_hom.norm_noninc.comp {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] {g : normed_add_group_hom V₂ V₃} {f : normed_add_group_hom V₁ V₂} (hg : g.norm_noninc) (hf : f.norm_noninc) :

(g.comp f).norm_noninc

source

@[simp]

theorem normed_add_group_hom.norm_noninc.neg_iff {V₁ : Type u_3} {V₂ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {f : normed_add_group_hom V₁ V₂} :

(-f).norm_noninc ↔ f.norm_noninc

source

theorem normed_add_group_hom.norm_eq_of_isometry {V : Type u_1} {W : Type u_2} [seminormed_add_comm_group V] [seminormed_add_comm_group W] {f : normed_add_group_hom V W} (hf : isometry ⇑f) (v : V) :

‖⇑f v‖ = ‖v‖

source

theorem normed_add_group_hom.isometry_id {V : Type u_1} [seminormed_add_comm_group V] :

isometry ⇑(normed_add_group_hom.id V)

source

theorem normed_add_group_hom.isometry_comp {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] {g : normed_add_group_hom V₂ V₃} {f : normed_add_group_hom V₁ V₂} (hg : isometry ⇑g) (hf : isometry ⇑f) :

isometry ⇑(g.comp f)

source

theorem normed_add_group_hom.norm_noninc_of_isometry {V : Type u_1} {W : Type u_2} [seminormed_add_comm_group V] [seminormed_add_comm_group W] {f : normed_add_group_hom V W} (hf : isometry ⇑f) :

f.norm_noninc

source

def normed_add_group_hom.equalizer {V : Type u_1} {W : Type u_2} [seminormed_add_comm_group V] [seminormed_add_comm_group W] (f g : normed_add_group_hom V W) :

add_subgroup V

The equalizer of two morphisms f g : normed_add_group_hom V W.

Equations

f.equalizer g = (f - g).ker

source

def normed_add_group_hom.equalizer.ι {V : Type u_1} {W : Type u_2} [seminormed_add_comm_group V] [seminormed_add_comm_group W] (f g : normed_add_group_hom V W) :

normed_add_group_hom ↥(f.equalizer g) V

The inclusion of f.equalizer g as a normed_add_group_hom.

Equations

normed_add_group_hom.equalizer.ι f g = normed_add_group_hom.incl (f.equalizer g)

source

theorem normed_add_group_hom.equalizer.comp_ι_eq {V : Type u_1} {W : Type u_2} [seminormed_add_comm_group V] [seminormed_add_comm_group W] (f g : normed_add_group_hom V W) :

f.comp (normed_add_group_hom.equalizer.ι f g) = g.comp (normed_add_group_hom.equalizer.ι f g)

source

@[simp]

theorem normed_add_group_hom.equalizer.lift_apply_coe {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} [seminormed_add_comm_group V] [seminormed_add_comm_group W] [seminormed_add_comm_group V₁] {f g : normed_add_group_hom V W} (φ : normed_add_group_hom V₁ V) (h : f.comp φ = g.comp φ) (v : V₁) :

↑(⇑(normed_add_group_hom.equalizer.lift φ h) v) = ⇑φ v

source

def normed_add_group_hom.equalizer.lift {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} [seminormed_add_comm_group V] [seminormed_add_comm_group W] [seminormed_add_comm_group V₁] {f g : normed_add_group_hom V W} (φ : normed_add_group_hom V₁ V) (h : f.comp φ = g.comp φ) :

normed_add_group_hom V₁ ↥(f.equalizer g)

If φ : normed_add_group_hom V₁ V is such that f.comp φ = g.comp φ, the induced morphism normed_add_group_hom V₁ (f.equalizer g).

Equations

normed_add_group_hom.equalizer.lift φ h = {to_fun := λ (v : V₁), ⟨⇑φ v, _⟩, map_add' := _, bound' := _}

source

@[simp]

theorem normed_add_group_hom.equalizer.ι_comp_lift {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} [seminormed_add_comm_group V] [seminormed_add_comm_group W] [seminormed_add_comm_group V₁] {f g : normed_add_group_hom V W} (φ : normed_add_group_hom V₁ V) (h : f.comp φ = g.comp φ) :

(normed_add_group_hom.equalizer.ι f g).comp (normed_add_group_hom.equalizer.lift φ h) = φ

source

noncomputable def normed_add_group_hom.equalizer.lift_equiv {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} [seminormed_add_comm_group V] [seminormed_add_comm_group W] [seminormed_add_comm_group V₁] {f g : normed_add_group_hom V W} :

{φ // f.comp φ = g.comp φ} ≃ normed_add_group_hom V₁ ↥(f.equalizer g)

The lifting property of the equalizer as an equivalence.

Equations

normed_add_group_hom.equalizer.lift_equiv = {to_fun := λ (φ : {φ // f.comp φ = g.comp φ}), normed_add_group_hom.equalizer.lift ↑φ _, inv_fun := λ (ψ : normed_add_group_hom V₁ ↥(f.equalizer g)), ⟨(normed_add_group_hom.equalizer.ι f g).comp ψ, _⟩, left_inv := _, right_inv := _}

source

@[simp]

theorem normed_add_group_hom.equalizer.lift_equiv_symm_apply_coe {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} [seminormed_add_comm_group V] [seminormed_add_comm_group W] [seminormed_add_comm_group V₁] {f g : normed_add_group_hom V W} (ψ : normed_add_group_hom V₁ ↥(f.equalizer g)) :

↑(⇑(normed_add_group_hom.equalizer.lift_equiv.symm) ψ) = (normed_add_group_hom.equalizer.ι f g).comp ψ

source

@[simp]

theorem normed_add_group_hom.equalizer.lift_equiv_apply {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} [seminormed_add_comm_group V] [seminormed_add_comm_group W] [seminormed_add_comm_group V₁] {f g : normed_add_group_hom V W} (φ : {φ // f.comp φ = g.comp φ}) :

⇑normed_add_group_hom.equalizer.lift_equiv φ = normed_add_group_hom.equalizer.lift ↑φ _

source

noncomputable def normed_add_group_hom.equalizer.map {V₁ : Type u_3} {V₂ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {W₁ : Type u_6} {W₂ : Type u_7} [seminormed_add_comm_group W₁] [seminormed_add_comm_group W₂] {f₁ g₁ : normed_add_group_hom V₁ W₁} {f₂ g₂ : normed_add_group_hom V₂ W₂} (φ : normed_add_group_hom V₁ V₂) (ψ : normed_add_group_hom W₁ W₂) (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ) :

normed_add_group_hom ↥(f₁.equalizer g₁) ↥(f₂.equalizer g₂)

Given φ : normed_add_group_hom V₁ V₂ and ψ : normed_add_group_hom W₁ W₂ such that ψ.comp f₁ = f₂.comp φ and ψ.comp g₁ = g₂.comp φ, the induced morphism normed_add_group_hom (f₁.equalizer g₁) (f₂.equalizer g₂).

Equations

normed_add_group_hom.equalizer.map φ ψ hf hg = normed_add_group_hom.equalizer.lift (φ.comp (normed_add_group_hom.equalizer.ι f₁ g₁)) _

source

@[simp]

theorem normed_add_group_hom.equalizer.ι_comp_map {V₁ : Type u_3} {V₂ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {W₁ : Type u_6} {W₂ : Type u_7} [seminormed_add_comm_group W₁] [seminormed_add_comm_group W₂] {f₁ g₁ : normed_add_group_hom V₁ W₁} {f₂ g₂ : normed_add_group_hom V₂ W₂} {φ : normed_add_group_hom V₁ V₂} {ψ : normed_add_group_hom W₁ W₂} (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ) :

(normed_add_group_hom.equalizer.ι f₂ g₂).comp (normed_add_group_hom.equalizer.map φ ψ hf hg) = φ.comp (normed_add_group_hom.equalizer.ι f₁ g₁)

source

@[simp]

theorem normed_add_group_hom.equalizer.map_id {V₁ : Type u_3} [seminormed_add_comm_group V₁] {W₁ : Type u_6} [seminormed_add_comm_group W₁] {f₁ g₁ : normed_add_group_hom V₁ W₁} :

normed_add_group_hom.equalizer.map (normed_add_group_hom.id V₁) (normed_add_group_hom.id W₁) rfl rfl = normed_add_group_hom.id ↥(f₁.equalizer g₁)

source

theorem normed_add_group_hom.equalizer.comm_sq₂ {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] {W₁ : Type u_6} {W₂ : Type u_7} {W₃ : Type u_8} [seminormed_add_comm_group W₁] [seminormed_add_comm_group W₂] [seminormed_add_comm_group W₃] {f₁ : normed_add_group_hom V₁ W₁} {f₂ : normed_add_group_hom V₂ W₂} {f₃ : normed_add_group_hom V₃ W₃} {φ : normed_add_group_hom V₁ V₂} {ψ : normed_add_group_hom W₁ W₂} {φ' : normed_add_group_hom V₂ V₃} {ψ' : normed_add_group_hom W₂ W₃} (hf : ψ.comp f₁ = f₂.comp φ) (hf' : ψ'.comp f₂ = f₃.comp φ') :

(ψ'.comp ψ).comp f₁ = f₃.comp (φ'.comp φ)

source

theorem normed_add_group_hom.equalizer.map_comp_map {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃] {W₁ : Type u_6} {W₂ : Type u_7} {W₃ : Type u_8} [seminormed_add_comm_group W₁] [seminormed_add_comm_group W₂] [seminormed_add_comm_group W₃] {f₁ g₁ : normed_add_group_hom V₁ W₁} {f₂ g₂ : normed_add_group_hom V₂ W₂} {f₃ g₃ : normed_add_group_hom V₃ W₃} {φ : normed_add_group_hom V₁ V₂} {ψ : normed_add_group_hom W₁ W₂} {φ' : normed_add_group_hom V₂ V₃} {ψ' : normed_add_group_hom W₂ W₃} (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ) (hf' : ψ'.comp f₂ = f₃.comp φ') (hg' : ψ'.comp g₂ = g₃.comp φ') :

(normed_add_group_hom.equalizer.map φ' ψ' hf' hg').comp (normed_add_group_hom.equalizer.map φ ψ hf hg) = normed_add_group_hom.equalizer.map (φ'.comp φ) (ψ'.comp ψ) _ _

source

theorem normed_add_group_hom.equalizer.ι_norm_noninc {V : Type u_1} {W : Type u_2} [seminormed_add_comm_group V] [seminormed_add_comm_group W] {f g : normed_add_group_hom V W} :

(normed_add_group_hom.equalizer.ι f g).norm_noninc

source

theorem normed_add_group_hom.equalizer.lift_norm_noninc {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} [seminormed_add_comm_group V] [seminormed_add_comm_group W] [seminormed_add_comm_group V₁] {f g : normed_add_group_hom V W} (φ : normed_add_group_hom V₁ V) (h : f.comp φ = g.comp φ) (hφ : φ.norm_noninc) :

(normed_add_group_hom.equalizer.lift φ h).norm_noninc

The lifting of a norm nonincreasing morphism is norm nonincreasing.

source

theorem normed_add_group_hom.equalizer.norm_lift_le {V : Type u_1} {W : Type u_2} {V₁ : Type u_3} [seminormed_add_comm_group V] [seminormed_add_comm_group W] [seminormed_add_comm_group V₁] {f g : normed_add_group_hom V W} (φ : normed_add_group_hom V₁ V) (h : f.comp φ = g.comp φ) (C : ℝ) (hφ : ‖φ‖ ≤ C) :

‖normed_add_group_hom.equalizer.lift φ h‖ ≤ C

If φ satisfies ‖φ‖ ≤ C, then the same is true for the lifted morphism.

source

theorem normed_add_group_hom.equalizer.map_norm_noninc {V₁ : Type u_3} {V₂ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {W₁ : Type u_6} {W₂ : Type u_7} [seminormed_add_comm_group W₁] [seminormed_add_comm_group W₂] {f₁ g₁ : normed_add_group_hom V₁ W₁} {f₂ g₂ : normed_add_group_hom V₂ W₂} {φ : normed_add_group_hom V₁ V₂} {ψ : normed_add_group_hom W₁ W₂} (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ) (hφ : φ.norm_noninc) :

(normed_add_group_hom.equalizer.map φ ψ hf hg).norm_noninc

source

theorem normed_add_group_hom.equalizer.norm_map_le {V₁ : Type u_3} {V₂ : Type u_4} [seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] {W₁ : Type u_6} {W₂ : Type u_7} [seminormed_add_comm_group W₁] [seminormed_add_comm_group W₂] {f₁ g₁ : normed_add_group_hom V₁ W₁} {f₂ g₂ : normed_add_group_hom V₂ W₂} {φ : normed_add_group_hom V₁ V₂} {ψ : normed_add_group_hom W₁ W₂} (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ) (C : ℝ) (hφ : ‖φ.comp (normed_add_group_hom.equalizer.ι f₁ g₁)‖ ≤ C) :

‖normed_add_group_hom.equalizer.map φ ψ hf hg‖ ≤ C

mathlib3 documentation

Normed groups homomorphisms #

The operator norm #

Addition of normed group homs #

The zero normed group hom #

The identity normed group hom #

The negation of a normed group hom #

Subtraction of normed group homs #

Scalar actions on normed group homs #

Normed group structure on normed group homs #

Module structure on normed group homs #

Composition of normed group homs #

Kernel #

Range #