namespace http://mathhub.info/MitM/core/functional-analysis ❚

import base http://mathhub.info/MitM/Foundation ❚
import calculus http://mathhub.info/MitM/core/calculus ❚
import algebra http://mathhub.info/MitM/core/algebra ❚
import topo http://mathhub.info/MitM/core/topology ❚
import arith http://mathhub.info/MitM/core/arithmetics ❚

theory NormedSpace : base:?Logic =
	include ☞algebra:?Vectorspace ❙
	include ☞algebra:?RealField ❙
	
	theory normedspace_theory : base:?Logic =
		include ☞algebra:?Vectorspace/vectorspace_theory (realField) ❙
		norm : universe ⟶  ℝ^+ ❘ # || 1 || ❙
		
		axiom_multiplicativity : ⊦ ∀[x : universe] ∀[a : ℝ] ☞arith:?RealArithmetics?multiplication (☞arith?RealArithmetics?absolute a) || x || ≐ || (scalarmult) a x ||❙
		axiom_subadditivity : ⊦ ∀[x : universe] ∀[y : universe] (|| op x y ||) ≤ (||x|| + ||y||) ❘// ⊦ ||(x + y)|| ≤ (||x|| + ||y||) ❙
		axiom_positivity : ⊦ ∀[x : universe] 0 ≤ || x || ❙
		axiom_definiteness : ⊦ ∀[x : universe] 0.0 ≐ || x || ⇔ x ≐ unit ❙ // ⊦ ||x||≐0 ⇔ x ≐ e  ❙
	❚ 
	normedSpace : kind ❘ = Mod ☞?NormedSpace/normedspace_theory ❙
	
	include ☞calculus:?MetricSpace ❙
	
	implicit view NormedSpaceAsMetricSpace : calculus:?MetricSpace/metricSpace_theory -> ?NormedSpace/normedspace_theory =
		universe = universe ❙ 
		d = [x : universe, y : universe] || x - y ||❙
		axiom_triangleInequality = sketch "follows from axiom_subadditivity" ❙
		axiom_isPseudoMetric = sketch "follows from axiom_positivity, and from the symmetry in the metric as implied by multiplicativity" ❙
	❚
❚
	

theory BanachSpace : base:?Logic =
  include ?NormedSpace ❙
	include ☞calculus:?Completeness ❙
	
	theory normedmetric_theory =
		include ?NormedSpace/normedspace_theory ❙
		structure ms : calculus:?MetricSpace/metricSpace_theory abbrev ?NormedSpace/NormedSpaceAsMetricSpace ❙
	❚
	normedmetric = Mod ☞?BanachSpace/normedmetric_theory ❙

	banach : {n : normedSpace} prop ❘ = [n] complete n ❙ // TODO also as models-of ❙
❚

theory BanachAlgebra : base:?Logic =
  include ?BanachSpace ❙
  
  
❚

// theory NormedRealVectorSpaces : base:?Logic =
	include algebra:?RealVectorspace ❙
	include arith:?RealArithmetics ❙
	// TODO generalize ❙
	// include ?NormedSpace ❙
	
	Norm: ℝ1.universe ⟶ ℝ^+ ❘ = [x] |x| ❘ # || 1 || ❙
	Axiom_Multiplicativity : ⊦ ∀[x : ℝ1.universe] ∀[α : ℝ] || (ℝ1.scalarmult) α x || ≐ | α | ⋅ || x || ❙ // error: type of bound variable too big: kind ❙
	Axiom_Subadditivity : ⊦ ∀[x] ∀[y] (|| (ℝ1.op) x y ||) ≤ (||x|| + ||y||) ❙
	Axiom_Positivity : ⊦ ∀[x] 0 ≤ || x || ❙
	Axiom_Definiteness : ⊦ ∀[x] ||x||≐0 ⇔ x ≐ (ℝ1.unit)  ❙
❚