+record is_archimedean_riesz_space (K) (S:riesz_space K) : Prop
+\def
+ { ars_archimedean: ∃u.∀n.∀a.∀p:n > O.
+ le ? S
+ (absolute_value ? S a)
+ ((inv ? (sum_field K n) (not_eq_sum_field_zero ? n p))* u) →
+ a = 0
+ }.
+
+record archimedean_riesz_space (K:ordered_field_ch0) : Type \def
+ { ars_riesz_space:> riesz_space K;
+ ars_archimedean_property: is_archimedean_riesz_space ? ars_riesz_space
+ }.
+
+record is_integral (K) (R:archimedean_riesz_space K) (I:R→K) : Prop
+\def
+ { i_positive: ∀f:R. le ? R 0 f → of_le K 0 (I f);
+ i_linear1: ∀f,g:R. I (f + g) = I f + I g;
+ i_linear2: ∀f:R.∀k:K. I (k*f) = k*(I f)
+ }.
+
+definition is_weak_unit ≝
+(* This definition is by Spitters. He cites Fremlin 353P, but:
+ 1. that theorem holds only in f-algebras (as in Spitters, but we are
+ defining it on Riesz spaces)
+ 2. Fremlin proves |x|/\u=0 \to u=0. How do we remove the absolute value?
+ λR:real.λV:archimedean_riesz_space R.λunit: V.
+ ∀x:V. meet x unit = 0 → u = 0.
+ 3. Fremlin proves u > 0 implies x /\ u > 0 > 0 for Archimedean spaces
+ only. We pick this definition for now.
+*) λR:real.λV:archimedean_riesz_space R.λe:V.
+ ∀v:V. lt ? V 0 v → lt ? V 0 (meet ? V v e).
+
+(* Here we are avoiding a construction (the quotient space to define
+ f=g iff I(|f-g|)=0 *)
+record integration_riesz_space (R:real) : Type \def
+ { irs_archimedean_riesz_space:> archimedean_riesz_space R;
+ irs_unit: irs_archimedean_riesz_space;
+ irs_weak_unit: is_weak_unit ? ? irs_unit;
+ integral: irs_archimedean_riesz_space → R;
+ irs_integral_properties: is_integral ? ? integral;
+ irs_limit1:
+ ∀f:irs_archimedean_riesz_space.
+ tends_to ?
+ (λn.integral (meet ? irs_archimedean_riesz_space f
+ ((sum_field R n)*irs_unit)))
+ (integral f);
+ irs_limit2:
+ ∀f:irs_archimedean_riesz_space.
+ tends_to ?
+ (λn.
+ integral (meet ? irs_archimedean_riesz_space f
+ ((inv ? (sum_field R (S n))
+ (not_eq_sum_field_zero R (S n) (le_S_S O n (le_O_n n)))
+ ) * irs_unit))) 0;
+ irs_quotient_space1:
+ ∀f,g:irs_archimedean_riesz_space.
+ integral (absolute_value ? irs_archimedean_riesz_space (f - g)) = 0 → f=g
+ }.
+
+definition induced_norm_fun ≝
+ λR:real.λV:integration_riesz_space R.λf:V.
+ integral ? ? (absolute_value ? ? f).
+
+lemma induced_norm_is_norm:
+ ∀R:real.∀V:integration_riesz_space R.is_norm ? V (induced_norm_fun ? V).