import analysis.normed.group.basic

noncomputable theory

open_locale nnreal big_operators

structure normed_add_group_hom (V W : Type*) [seminormed_add_comm_group V]

[seminormed_add_comm_group W] :=

(to_fun : V → W)

(map_add' : ∀ v₁ v₂, to_fun (v₁ + v₂) = to_fun v₁ + to_fun v₂)

(bound' : ∃ C, ∀ v, ‖to_fun v‖ ≤ C * ‖v‖)

namespace add_monoid_hom

variables {V W : Type*} [seminormed_add_comm_group V] [seminormed_add_comm_group W]

{f g : normed_add_group_hom V W}

def mk_normed_add_group_hom (f : V →+ W)

(C : ℝ) (h : ∀ v, ‖f v‖ ≤ C * ‖v‖) : normed_add_group_hom V W :=

{ bound' := ⟨C, h⟩, ..f }

def mk_normed_add_group_hom' (f : V →+ W) (C : ℝ≥0) (hC : ∀ x, ‖f x‖₊ ≤ C * ‖x‖₊) :

normed_add_group_hom V W :=

{ bound' := ⟨C, hC⟩ .. f}

end add_monoid_hom

lemma exists_pos_bound_of_bound {V W : Type*} [seminormed_add_comm_group V]

[seminormed_add_comm_group W]

{f : V → W} (M : ℝ) (h : ∀x, ‖f x‖ ≤ M * ‖x‖) :

∃ N, 0 < N ∧ ∀x, ‖f x‖ ≤ N * ‖x‖ :=

⟨max M 1, lt_of_lt_of_le zero_lt_one (le_max_right _ _), λx, calc

‖f x‖ ≤ M * ‖x‖ : h x

... ≤ max M 1 * ‖x‖ : mul_le_mul_of_nonneg_right (le_max_left _ _) (norm_nonneg _) ⟩

namespace normed_add_group_hom

variables {V V₁ V₂ V₃ : Type*} [seminormed_add_comm_group V] [seminormed_add_comm_group V₁]

[seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃]

variables {f g : normed_add_group_hom V₁ V₂}

instance : has_coe_to_fun (normed_add_group_hom V₁ V₂) (λ _, V₁ → V₂) :=

⟨normed_add_group_hom.to_fun⟩

initialize_simps_projections normed_add_group_hom (to_fun → apply)

lemma coe_inj (H : (f : V₁ → V₂) = g) : f = g :=

by cases f; cases g; congr'; exact funext H

lemma coe_injective : @function.injective (normed_add_group_hom V₁ V₂) (V₁ → V₂) coe_fn :=

by apply coe_inj

lemma coe_inj_iff : f = g ↔ (f : V₁ → V₂) = g := ⟨congr_arg _, coe_inj⟩

@[ext] lemma ext (H : ∀ x, f x = g x) : f = g := coe_inj $ funext H

lemma ext_iff : f = g ↔ ∀ x, f x = g x := ⟨by rintro rfl x; refl, ext⟩

variables (f g)

@[simp] lemma to_fun_eq_coe : f.to_fun = f := rfl

@[simp] lemma coe_mk (f) (h₁) (h₂) (h₃) : ⇑(⟨f, h₁, h₂, h₃⟩ : normed_add_group_hom V₁ V₂) = f := rfl

@[simp] lemma coe_mk_normed_add_group_hom (f : V₁ →+ V₂) (C) (hC) :

⇑(f.mk_normed_add_group_hom C hC) = f := rfl

@[simp] lemma coe_mk_normed_add_group_hom' (f : V₁ →+ V₂) (C) (hC) :

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

def to_add_monoid_hom (f : normed_add_group_hom V₁ V₂) : V₁ →+ V₂ :=

add_monoid_hom.mk' f f.map_add'

@[simp] lemma coe_to_add_monoid_hom : ⇑f.to_add_monoid_hom = f := rfl

lemma to_add_monoid_hom_injective :

function.injective (@normed_add_group_hom.to_add_monoid_hom V₁ V₂ _ _) :=

λ f g h, coe_inj $ show ⇑f.to_add_monoid_hom = g, by { rw h, refl }

@[simp] lemma mk_to_add_monoid_hom (f) (h₁) (h₂) :

(⟨f, h₁, h₂⟩ : normed_add_group_hom V₁ V₂).to_add_monoid_hom = add_monoid_hom.mk' f h₁ := rfl

instance : add_monoid_hom_class (normed_add_group_hom V₁ V₂) V₁ V₂ :=

{ coe := coe_fn,

coe_injective' := coe_injective,

map_add := λ f, f.to_add_monoid_hom.map_add,

map_zero := λ f, f.to_add_monoid_hom.map_zero }

lemma bound : ∃ C, 0 < C ∧ ∀ x, ‖f x‖ ≤ C * ‖x‖ :=

let ⟨C, hC⟩ := f.bound' in exists_pos_bound_of_bound _ hC

theorem antilipschitz_of_norm_ge {K : ℝ≥0} (h : ∀ x, ‖x‖ ≤ K * ‖f x‖) :

antilipschitz_with K f :=

antilipschitz_with.of_le_mul_dist $

λ x y, by simpa only [dist_eq_norm, map_sub] using h (x - y)

def surjective_on_with (f : normed_add_group_hom V₁ V₂) (K : add_subgroup V₂) (C : ℝ) : Prop :=

∀ h ∈ K, ∃ g, f g = h ∧ ‖g‖ ≤ C*‖h‖

lemma surjective_on_with.mono {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' :=

intros k k_in,

rcases h k k_in with ⟨g, rfl, hg⟩,

use [g, rfl],

by_cases Hg : ‖f g‖ = 0,

{ simpa [Hg] using hg },

{ exact hg.trans ((mul_le_mul_right $ (ne.symm Hg).le_iff_lt.mp (norm_nonneg _)).mpr H) }

lemma surjective_on_with.exists_pos {f : normed_add_group_hom V₁ V₂} {K : add_subgroup V₂} {C : ℝ}

(h : f.surjective_on_with K C) : ∃ C' > 0, f.surjective_on_with K C' :=

refine ⟨|C| + 1, _, _⟩,

{ linarith [abs_nonneg C] },

{ apply h.mono,

linarith [le_abs_self C] }

lemma surjective_on_with.surj_on {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 :=

λ x hx, (h x hx).imp $ λ a ⟨ha, _⟩, ⟨set.mem_univ _, ha⟩

def op_norm (f : normed_add_group_hom V₁ V₂) := Inf {c | 0 ≤ c ∧ ∀ x, ‖f x‖ ≤ c * ‖x‖}

instance has_op_norm : has_norm (normed_add_group_hom V₁ V₂) := ⟨op_norm⟩

lemma norm_def : ‖f‖ = Inf {c | 0 ≤ c ∧ ∀ x, ‖f x‖ ≤ c * ‖x‖} := rfl

lemma bounds_nonempty {f : normed_add_group_hom V₁ V₂} :

∃ c, c ∈ { c | 0 ≤ c ∧ ∀ x, ‖f x‖ ≤ c * ‖x‖ } :=

let ⟨M, hMp, hMb⟩ := f.bound in ⟨M, le_of_lt hMp, hMb⟩

lemma bounds_bdd_below {f : normed_add_group_hom V₁ V₂} :

bdd_below {c | 0 ≤ c ∧ ∀ x, ‖f x‖ ≤ c * ‖x‖} :=

⟨0, λ _ ⟨hn, _⟩, hn⟩

lemma op_norm_nonneg : 0 ≤ ‖f‖ :=

le_cInf bounds_nonempty (λ _ ⟨hx, _⟩, hx)

theorem le_op_norm (x : V₁) : ‖f x‖ ≤ ‖f‖ * ‖x‖ :=

obtain ⟨C, Cpos, hC⟩ := f.bound,

replace hC := hC x,

by_cases h : ‖x‖ = 0,

{ rwa [h, mul_zero] at ⊢ hC },

have hlt : 0 < ‖x‖ := lt_of_le_of_ne (norm_nonneg x) (ne.symm h),

exact (div_le_iff hlt).mp (le_cInf bounds_nonempty (λ c ⟨_, hc⟩,

(div_le_iff hlt).mpr $ by { apply hc })),

theorem le_op_norm_of_le {c : ℝ} {x} (h : ‖x‖ ≤ c) : ‖f x‖ ≤ ‖f‖ * c :=

le_trans (f.le_op_norm x) (mul_le_mul_of_nonneg_left h f.op_norm_nonneg)

theorem le_of_op_norm_le {c : ℝ} (h : ‖f‖ ≤ c) (x : V₁) : ‖f x‖ ≤ c * ‖x‖ :=

(f.le_op_norm x).trans (mul_le_mul_of_nonneg_right h (norm_nonneg x))

theorem lipschitz : lipschitz_with ⟨‖f‖, op_norm_nonneg f⟩ f :=

lipschitz_with.of_dist_le_mul $ λ x y,

by { rw [dist_eq_norm, dist_eq_norm, ←map_sub], apply le_op_norm }

protected lemma uniform_continuous (f : normed_add_group_hom V₁ V₂) :

uniform_continuous f := f.lipschitz.uniform_continuous

protected lemma continuous (f : normed_add_group_hom V₁ V₂) : continuous f :=

f.uniform_continuous.continuous

lemma ratio_le_op_norm (x : V₁) : ‖f x‖ / ‖x‖ ≤ ‖f‖ :=

div_le_of_nonneg_of_le_mul (norm_nonneg _) f.op_norm_nonneg (le_op_norm _ _)

lemma op_norm_le_bound {M : ℝ} (hMp: 0 ≤ M) (hM : ∀ x, ‖f x‖ ≤ M * ‖x‖) :

‖f‖ ≤ M :=

cInf_le bounds_bdd_below ⟨hMp, hM⟩

lemma op_norm_eq_of_bounds {M : ℝ} (M_nonneg : 0 ≤ M)

(h_above : ∀ x, ‖f x‖ ≤ M*‖x‖) (h_below : ∀ N ≥ 0, (∀ x, ‖f x‖ ≤ N*‖x‖) → M ≤ N) :

‖f‖ = M :=

le_antisymm (f.op_norm_le_bound M_nonneg h_above)

((le_cInf_iff normed_add_group_hom.bounds_bdd_below ⟨M, M_nonneg, h_above⟩).mpr $

λ N ⟨N_nonneg, hN⟩, h_below N N_nonneg hN)

theorem op_norm_le_of_lipschitz {f : normed_add_group_hom V₁ V₂} {K : ℝ≥0}

(hf : lipschitz_with K f) :

‖f‖ ≤ K :=

f.op_norm_le_bound K.2 $ λ x, by simpa only [dist_zero_right, map_zero] using hf.dist_le_mul x 0

lemma mk_normed_add_group_hom_norm_le (f : V₁ →+ V₂) {C : ℝ} (hC : 0 ≤ C)

(h : ∀ x, ‖f x‖ ≤ C * ‖x‖) :

‖f.mk_normed_add_group_hom C h‖ ≤ C :=

op_norm_le_bound _ hC h

lemma mk_normed_add_group_hom_norm_le' (f : V₁ →+ V₂) {C : ℝ} (h : ∀x, ‖f x‖ ≤ C * ‖x‖) :

‖f.mk_normed_add_group_hom C h‖ ≤ max C 0 :=

op_norm_le_bound _ (le_max_right _ _) $ λ x, (h x).trans $

mul_le_mul_of_nonneg_right (le_max_left _ _) (norm_nonneg x)

alias mk_normed_add_group_hom_norm_le ← _root_.add_monoid_hom.mk_normed_add_group_hom_norm_le

alias mk_normed_add_group_hom_norm_le' ← _root_.add_monoid_hom.mk_normed_add_group_hom_norm_le'

instance : has_add (normed_add_group_hom V₁ V₂) :=

⟨λ f g, (f.to_add_monoid_hom + g.to_add_monoid_hom).mk_normed_add_group_hom (‖f‖ + ‖g‖) $ λ v, calc

‖f v + g v‖

≤ ‖f v‖ + ‖g v‖ : norm_add_le _ _

... ≤ ‖f‖ * ‖v‖ + ‖g‖ * ‖v‖ : add_le_add (le_op_norm f v) (le_op_norm g v)

... = (‖f‖ + ‖g‖) * ‖v‖ : by rw add_mul⟩

theorem op_norm_add_le : ‖f + g‖ ≤ ‖f‖ + ‖g‖ :=

mk_normed_add_group_hom_norm_le _ (add_nonneg (op_norm_nonneg _) (op_norm_nonneg _)) _

library_note "addition on function coercions"

@[simp] lemma coe_add (f g : normed_add_group_hom V₁ V₂) : ⇑(f + g) = (f + g : V₁ → V₂) := rfl

@[simp] lemma add_apply (f g : normed_add_group_hom V₁ V₂) (v : V₁) :

(f + g : normed_add_group_hom V₁ V₂) v = f v + g v := rfl

instance : has_zero (normed_add_group_hom V₁ V₂) :=

⟨(0 : V₁ →+ V₂).mk_normed_add_group_hom 0 (by simp)⟩

instance : inhabited (normed_add_group_hom V₁ V₂) := ⟨0⟩

theorem op_norm_zero : ‖(0 : normed_add_group_hom V₁ V₂)‖ = 0 :=

le_antisymm (cInf_le bounds_bdd_below

⟨ge_of_eq rfl, λ _, le_of_eq (by { rw [zero_mul], exact norm_zero })⟩)

(op_norm_nonneg _)

theorem op_norm_zero_iff {V₁ V₂ : Type*} [normed_add_comm_group V₁] [normed_add_comm_group V₂]

{f : normed_add_group_hom V₁ V₂} : ‖f‖ = 0 ↔ f = 0 :=

iff.intro

(λ hn, ext (λ x, norm_le_zero_iff.1

(calc _ ≤ ‖f‖ * ‖x‖ : le_op_norm _ _

... = _ : by rw [hn, zero_mul])))

(λ hf, by rw [hf, op_norm_zero] )

@[simp] lemma coe_zero : ⇑(0 : normed_add_group_hom V₁ V₂) = (0 : V₁ → V₂) := rfl

@[simp] lemma zero_apply (v : V₁) : (0 : normed_add_group_hom V₁ V₂) v = 0 := rfl

variables {f g}

variable (V)

def id : normed_add_group_hom V V :=

(add_monoid_hom.id V).mk_normed_add_group_hom 1 (by simp [le_refl])

lemma norm_id_le : ‖(id V : normed_add_group_hom V V)‖ ≤ 1 :=

op_norm_le_bound _ zero_le_one (λx, by simp)

lemma norm_id_of_nontrivial_seminorm (h : ∃ (x : V), ‖x‖ ≠ 0 ) :

‖(id V)‖ = 1 :=

le_antisymm (norm_id_le V) $ let ⟨x, hx⟩ := h in

have _ := (id V).ratio_le_op_norm x,

by rwa [id_apply, div_self hx] at this

lemma norm_id {V : Type*} [normed_add_comm_group V] [nontrivial V] : ‖(id V)‖ = 1 :=

refine norm_id_of_nontrivial_seminorm V _,

obtain ⟨x, hx⟩ := exists_ne (0 : V),

exact ⟨x, ne_of_gt (norm_pos_iff.2 hx)⟩,

lemma coe_id : ((normed_add_group_hom.id V) : V → V) = (_root_.id : V → V) := rfl

instance : has_neg (normed_add_group_hom V₁ V₂) :=

⟨λ f, (-f.to_add_monoid_hom).mk_normed_add_group_hom (‖f‖) (λ v, by simp [le_op_norm f v])⟩

@[simp] lemma coe_neg (f : normed_add_group_hom V₁ V₂) : ⇑(-f) = (-f : V₁ → V₂) := rfl

@[simp] lemma neg_apply (f : normed_add_group_hom V₁ V₂) (v : V₁) :

(-f : normed_add_group_hom V₁ V₂) v = - (f v) := rfl

lemma op_norm_neg (f : normed_add_group_hom V₁ V₂) : ‖-f‖ = ‖f‖ :=

by simp only [norm_def, coe_neg, norm_neg, pi.neg_apply]

instance : has_sub (normed_add_group_hom V₁ V₂) :=

⟨λ f g,

{ bound' :=

begin

simp only [add_monoid_hom.sub_apply, add_monoid_hom.to_fun_eq_coe, sub_eq_add_neg],

exact (f + -g).bound'

end,

.. (f.to_add_monoid_hom - g.to_add_monoid_hom) }⟩

@[simp] lemma coe_sub (f g : normed_add_group_hom V₁ V₂) : ⇑(f - g) = (f - g : V₁ → V₂) := rfl

@[simp] lemma sub_apply (f g : normed_add_group_hom V₁ V₂) (v : V₁) :

(f - g : normed_add_group_hom V₁ V₂) v = f v - g v := rfl

section has_smul

variables {R R' : Type*}

[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₂]

instance : has_smul R (normed_add_group_hom V₁ V₂) :=

{ smul := λ r f,

{ to_fun := r • f,

map_add' := (r • f.to_add_monoid_hom).map_add',

bound' := let ⟨b, hb⟩ := f.bound' in ⟨dist r 0 * b, λ x, begin

have := dist_smul_pair r (f x) (f 0),

rw [map_zero, smul_zero, dist_zero_right, dist_zero_right] at this,

rw mul_assoc,

refine this.trans _,

refine mul_le_mul_of_nonneg_left _ dist_nonneg,

exact hb x

end⟩ } }

@[simp] lemma coe_smul (r : R) (f : normed_add_group_hom V₁ V₂) : ⇑(r • f) = r • f := rfl

@[simp] lemma smul_apply (r : R) (f : normed_add_group_hom V₁ V₂) (v : V₁) : (r • f) v = r • f v :=

rfl

instance [smul_comm_class R R' V₂] : smul_comm_class R R' (normed_add_group_hom V₁ V₂) :=

{ smul_comm := λ r r' f, ext $ λ v, smul_comm _ _ _ }

instance [has_smul R R'] [is_scalar_tower R R' V₂] :

is_scalar_tower R R' (normed_add_group_hom V₁ V₂) :=

{ smul_assoc := λ r r' f, ext $ λ v, smul_assoc _ _ _ }

instance [distrib_mul_action Rᵐᵒᵖ V₂] [is_central_scalar R V₂] :

is_central_scalar R (normed_add_group_hom V₁ V₂) :=

{ op_smul_eq_smul := λ r f, ext $ λ v, op_smul_eq_smul _ _ }

end has_smul

instance has_nat_scalar : has_smul ℕ (normed_add_group_hom V₁ V₂) :=

{ smul := λ n f,

{ to_fun := n • f,

map_add' := (n • f.to_add_monoid_hom).map_add',

bound' := let ⟨b, hb⟩ := f.bound' in ⟨n • b, λ v, begin

rw [pi.smul_apply, nsmul_eq_mul, mul_assoc],

exact (norm_nsmul_le _ _).trans (mul_le_mul_of_nonneg_left (hb _) (nat.cast_nonneg _)),

end⟩ } }

@[simp] lemma coe_nsmul (r : ℕ) (f : normed_add_group_hom V₁ V₂) : ⇑(r • f) = r • f := rfl

@[simp] lemma nsmul_apply (r : ℕ) (f : normed_add_group_hom V₁ V₂) (v : V₁) : (r • f) v = r • f v :=

rfl

instance has_int_scalar : has_smul ℤ (normed_add_group_hom V₁ V₂) :=

{ smul := λ z f,

{ to_fun := z • f,

map_add' := (z • f.to_add_monoid_hom).map_add',

bound' := let ⟨b, hb⟩ := f.bound' in ⟨‖z‖ • b, λ v, begin

rw [pi.smul_apply, smul_eq_mul, mul_assoc],

exact (norm_zsmul_le _ _).trans (mul_le_mul_of_nonneg_left (hb _) $ norm_nonneg _),

end⟩ } }

@[simp] lemma coe_zsmul (r : ℤ) (f : normed_add_group_hom V₁ V₂) : ⇑(r • f) = r • f := rfl

@[simp] lemma zsmul_apply (r : ℤ) (f : normed_add_group_hom V₁ V₂) (v : V₁) : (r • f) v = r • f v :=

rfl

instance : add_comm_group (normed_add_group_hom V₁ V₂) :=

coe_injective.add_comm_group _ rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _ _, rfl) (λ _ _, rfl)

instance to_seminormed_add_comm_group : seminormed_add_comm_group (normed_add_group_hom V₁ V₂) :=

add_group_seminorm.to_seminormed_add_comm_group

{ to_fun := op_norm,

map_zero' := op_norm_zero,

neg' := op_norm_neg,

add_le' := op_norm_add_le }

instance to_normed_add_comm_group {V₁ V₂ : Type*} [normed_add_comm_group V₁]

[normed_add_comm_group V₂] :

normed_add_comm_group (normed_add_group_hom V₁ V₂) :=

add_group_norm.to_normed_add_comm_group

{ to_fun := op_norm,

map_zero' := op_norm_zero,

neg' := op_norm_neg,

add_le' := op_norm_add_le,

eq_zero_of_map_eq_zero' := λ f, op_norm_zero_iff.1 }

def coe_fn_add_hom : normed_add_group_hom V₁ V₂ →+ (V₁ → V₂) :=

{ to_fun := coe_fn, map_zero' := coe_zero, map_add' := coe_add}

@[simp] lemma coe_sum {ι : Type*} (s : finset ι) (f : ι → normed_add_group_hom V₁ V₂) :

⇑(∑ i in s, f i) = ∑ i in s, (f i) :=

(coe_fn_add_hom : _ →+ (V₁ → V₂)).map_sum f s

lemma sum_apply {ι : Type*} (s : finset ι) (f : ι → normed_add_group_hom V₁ V₂) (v : V₁) :

(∑ i in s, f i) v = ∑ i in s, (f i v) :=

by simp only [coe_sum, finset.sum_apply]

instance {R : Type*} [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₂) :=

function.injective.distrib_mul_action coe_fn_add_hom coe_injective coe_smul

instance {R : Type*} [semiring R] [module R V₂]

[pseudo_metric_space R] [has_bounded_smul R V₂] :

module R (normed_add_group_hom V₁ V₂) :=

function.injective.module _ coe_fn_add_hom coe_injective coe_smul

protected def comp (g : normed_add_group_hom V₂ V₃) (f : normed_add_group_hom V₁ V₂) :

normed_add_group_hom V₁ V₃ :=

(g.to_add_monoid_hom.comp f.to_add_monoid_hom).mk_normed_add_group_hom (‖g‖ * ‖f‖) $ λ v, calc

‖g (f v)‖ ≤ ‖g‖ * ‖f v‖ : le_op_norm _ _

... ≤ ‖g‖ * (‖f‖ * ‖v‖) : mul_le_mul_of_nonneg_left (le_op_norm _ _) (op_norm_nonneg _)

... = ‖g‖ * ‖f‖ * ‖v‖ : by rw mul_assoc

lemma norm_comp_le (g : normed_add_group_hom V₂ V₃) (f : normed_add_group_hom V₁ V₂) :

‖g.comp f‖ ≤ ‖g‖ * ‖f‖ :=

mk_normed_add_group_hom_norm_le _ (mul_nonneg (op_norm_nonneg _) (op_norm_nonneg _)) _

lemma norm_comp_le_of_le {g : normed_add_group_hom V₂ V₃} {C₁ C₂ : ℝ} (hg : ‖g‖ ≤ C₂)

(hf : ‖f‖ ≤ C₁) :

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

le_trans (norm_comp_le g f) $ mul_le_mul hg hf (norm_nonneg _) (le_trans (norm_nonneg _) hg)

lemma norm_comp_le_of_le' {g : normed_add_group_hom V₂ V₃} (C₁ C₂ C₃ : ℝ) (h : C₃ = C₂ * C₁)

(hg : ‖g‖ ≤ C₂) (hf : ‖f‖ ≤ C₁) : ‖g.comp f‖ ≤ C₃ :=

by { rw h, exact norm_comp_le_of_le hg hf }

def comp_hom :

normed_add_group_hom V₂ V₃ →+ normed_add_group_hom V₁ V₂ →+ normed_add_group_hom V₁ V₃ :=

add_monoid_hom.mk' (λ g, add_monoid_hom.mk' (λ f, g.comp f)

(by { intros, ext, exact map_add g _ _ }))

(by { intros, ext, simp only [comp_apply, pi.add_apply, function.comp_app,

add_monoid_hom.add_apply, add_monoid_hom.mk'_apply, coe_add] })

@[simp] lemma comp_zero (f : normed_add_group_hom V₂ V₃) :

f.comp (0 : normed_add_group_hom V₁ V₂) = 0 :=

by { ext, exact map_zero f }

@[simp] lemma zero_comp (f : normed_add_group_hom V₁ V₂) :

(0 : normed_add_group_hom V₂ V₃).comp f = 0 :=

by { ext, refl }

lemma comp_assoc {V₄: Type* } [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) :=

by { ext, refl }

lemma coe_comp (f : normed_add_group_hom V₁ V₂) (g : normed_add_group_hom V₂ V₃) :

(g.comp f : V₁ → V₃) = (g : V₂ → V₃) ∘ (f : V₁ → V₂) := rfl

end normed_add_group_hom

namespace normed_add_group_hom

variables {V W V₁ V₂ V₃ : Type*} [seminormed_add_comm_group V] [seminormed_add_comm_group W]

[seminormed_add_comm_group V₁] [seminormed_add_comm_group V₂] [seminormed_add_comm_group V₃]

@[simps] def incl (s : add_subgroup V) : normed_add_group_hom s V :=

{ to_fun := (coe : s → V),

map_add' := λ v w, add_subgroup.coe_add _ _ _,

bound' := ⟨1, λ v, by { rw [one_mul], refl }⟩ }

lemma norm_incl {V' : add_subgroup V} (x : V') : ‖incl _ x‖ = ‖x‖ :=

rfl

section kernels

variables (f : normed_add_group_hom V₁ V₂) (g : normed_add_group_hom V₂ V₃)

def ker : add_subgroup V₁ := f.to_add_monoid_hom.ker

lemma mem_ker (v : V₁) : v ∈ f.ker ↔ f v = 0 :=

by { erw f.to_add_monoid_hom.mem_ker, refl }

@[simps] def ker.lift (h : g.comp f = 0) :

normed_add_group_hom V₁ g.ker :=

{ to_fun := λ v, ⟨f v, by { erw g.mem_ker, show (g.comp f) v = 0, rw h, refl }⟩,

map_add' := λ v w, by { simp only [map_add], refl },

bound' := f.bound' }

@[simp] lemma ker.incl_comp_lift (h : g.comp f = 0) :

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

by { ext, refl }

lemma ker_zero : (0 : normed_add_group_hom V₁ V₂).ker = ⊤ :=

by { ext, simp [mem_ker] }

lemma coe_ker : (f.ker : set V₁) = (f : V₁ → V₂) ⁻¹' {0} := rfl

lemma is_closed_ker {V₂ : Type*} [normed_add_comm_group V₂] (f : normed_add_group_hom V₁ V₂) :

is_closed (f.ker : set V₁) :=

f.coe_ker ▸ is_closed.preimage f.continuous (t1_space.t1 0)

end kernels

section range

variables (f : normed_add_group_hom V₁ V₂) (g : normed_add_group_hom V₂ V₃)

def range : add_subgroup V₂ := f.to_add_monoid_hom.range

lemma mem_range (v : V₂) : v ∈ f.range ↔ ∃ w, f w = v :=

by { rw [range, add_monoid_hom.mem_range], refl }

lemma mem_range_self (v : V₁) : f v ∈ f.range :=

⟨v, rfl⟩

lemma comp_range : (g.comp f).range = add_subgroup.map g.to_add_monoid_hom f.range :=

by { erw add_monoid_hom.map_range, refl }

lemma incl_range (s : add_subgroup V₁) : (incl s).range = s :=

by { ext x, exact ⟨λ ⟨y, hy⟩, by { rw ← hy; simp }, λ hx, ⟨⟨x, hx⟩, by simp⟩⟩ }

lemma range_comp_incl_top : (f.comp (incl (⊤ : add_subgroup V₁))).range = f.range :=

by simpa [comp_range, incl_range, ← add_monoid_hom.range_eq_map]

end range

variables {f : normed_add_group_hom V W}

def norm_noninc (f : normed_add_group_hom V W) : Prop :=

∀ v, ‖f v‖ ≤ ‖v‖

namespace norm_noninc

lemma norm_noninc_iff_norm_le_one : f.norm_noninc ↔ ‖f‖ ≤ 1 :=

refine ⟨λ h, _, λ h, λ v, _⟩,

{ refine op_norm_le_bound _ (zero_le_one) (λ v, _),

simpa [one_mul] using h v },

{ simpa using le_of_op_norm_le f h v }

lemma zero : (0 : normed_add_group_hom V₁ V₂).norm_noninc :=

λ v, by simp

lemma id : (id V).norm_noninc :=

λ v, le_rfl

lemma comp {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 :=

λ v, (hg (f v)).trans (hf v)

@[simp] lemma neg_iff {f : normed_add_group_hom V₁ V₂} : (-f).norm_noninc ↔ f.norm_noninc :=

⟨λ h x, by { simpa using h x }, λ h x, (norm_neg (f x)).le.trans (h x)⟩

end norm_noninc

section isometry

lemma norm_eq_of_isometry {f : normed_add_group_hom V W} (hf : isometry f) (v : V) :

‖f v‖ = ‖v‖ :=

(add_monoid_hom_class.isometry_iff_norm f).mp hf v

lemma isometry_id : @isometry V V _ _ (id V) :=

isometry_id

lemma isometry_comp {g : normed_add_group_hom V₂ V₃} {f : normed_add_group_hom V₁ V₂}

(hg : isometry g) (hf : isometry f) :

isometry (g.comp f) :=

hg.comp hf

lemma norm_noninc_of_isometry (hf : isometry f) : f.norm_noninc :=

λ v, le_of_eq $ norm_eq_of_isometry hf v

end isometry

variables {W₁ W₂ W₃ : Type*} [seminormed_add_comm_group W₁] [seminormed_add_comm_group W₂]

[seminormed_add_comm_group W₃]

variables (f) (g : normed_add_group_hom V W)

variables {f₁ g₁ : normed_add_group_hom V₁ W₁}

variables {f₂ g₂ : normed_add_group_hom V₂ W₂}

variables {f₃ g₃ : normed_add_group_hom V₃ W₃}

def equalizer := (f - g).ker

namespace equalizer

def ι : normed_add_group_hom (f.equalizer g) V := incl _

lemma comp_ι_eq : f.comp (ι f g) = g.comp (ι f g) :=

by { ext, rw [comp_apply, comp_apply, ← sub_eq_zero, ← normed_add_group_hom.sub_apply], exact x.2 }

variables {f g}

def lift (φ : normed_add_group_hom V₁ V) (h : f.comp φ = g.comp φ) :

normed_add_group_hom V₁ (f.equalizer g) :=

{ to_fun := λ v, ⟨φ v, show (f - g) (φ v) = 0,

by rw [normed_add_group_hom.sub_apply, sub_eq_zero, ← comp_apply, h, comp_apply]⟩,

map_add' := λ v₁ v₂, by { ext, simp only [map_add, add_subgroup.coe_add, subtype.coe_mk] },

bound' := by { obtain ⟨C, C_pos, hC⟩ := φ.bound, exact ⟨C, hC⟩ } }

@[simp] lemma ι_comp_lift (φ : normed_add_group_hom V₁ V) (h : f.comp φ = g.comp φ) :

(ι _ _).comp (lift φ h) = φ :=

by { ext, refl }

def lift_equiv : {φ : normed_add_group_hom V₁ V // f.comp φ = g.comp φ} ≃

normed_add_group_hom V₁ (f.equalizer g) :=

{ to_fun := λ φ, lift φ φ.prop,

inv_fun := λ ψ, ⟨(ι f g).comp ψ, by { rw [← comp_assoc, ← comp_assoc, comp_ι_eq] }⟩,

left_inv := λ φ, by simp,

right_inv := λ ψ, by { ext, refl } }

def map (φ : 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₂) :=

lift (φ.comp $ ι _ _) $

by { simp only [← comp_assoc, ← hf, ← hg], simp only [comp_assoc, comp_ι_eq] }

variables {φ : normed_add_group_hom V₁ V₂} {ψ : normed_add_group_hom W₁ W₂}

variables {φ' : normed_add_group_hom V₂ V₃} {ψ' : normed_add_group_hom W₂ W₃}

@[simp] lemma ι_comp_map (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ) :

(ι f₂ g₂).comp (map φ ψ hf hg) = φ.comp (ι _ _) :=

ι_comp_lift _ _

@[simp] lemma map_id : map (id V₁) (id W₁) rfl rfl = id (f₁.equalizer g₁) :=

by { ext, refl }

lemma comm_sq₂ (hf : ψ.comp f₁ = f₂.comp φ) (hf' : ψ'.comp f₂ = f₃.comp φ') :

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

by rw [comp_assoc, hf, ← comp_assoc, hf', comp_assoc]

lemma map_comp_map (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ)

(hf' : ψ'.comp f₂ = f₃.comp φ') (hg' : ψ'.comp g₂ = g₃.comp φ') :

(map φ' ψ' hf' hg').comp (map φ ψ hf hg) =

map (φ'.comp φ) (ψ'.comp ψ) (comm_sq₂ hf hf') (comm_sq₂ hg hg') :=

by { ext, refl }

lemma ι_norm_noninc : (ι f g).norm_noninc := λ v, le_rfl

lemma lift_norm_noninc (φ : normed_add_group_hom V₁ V) (h : f.comp φ = g.comp φ)

(hφ : φ.norm_noninc) :

(lift φ h).norm_noninc :=

hφ

lemma norm_lift_le (φ : normed_add_group_hom V₁ V) (h : f.comp φ = g.comp φ)

(C : ℝ) (hφ : ‖φ‖ ≤ C) : ‖(lift φ h)‖ ≤ C := hφ

lemma map_norm_noninc (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ)

(hφ : φ.norm_noninc) : (map φ ψ hf hg).norm_noninc :=

lift_norm_noninc _ _ $ hφ.comp ι_norm_noninc

lemma norm_map_le (hf : ψ.comp f₁ = f₂.comp φ) (hg : ψ.comp g₁ = g₂.comp φ)

(C : ℝ) (hφ : ‖φ.comp (ι f₁ g₁)‖ ≤ C) : ‖map φ ψ hf hg‖ ≤ C :=

norm_lift_le _ _ _ hφ

end equalizer

end normed_add_group_hom