+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 ≝
+ λ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 ? V).
+ intros;
+ apply mk_is_norm;
+ [ apply mk_is_semi_norm;
+ [ unfold induced_norm;
+ intros;
+ apply i_positive;
+ [ apply (irs_integral_properties ? V)
+ | (* difficile *)
+ elim daemon
+ ]
+ | intros;
+ unfold induced_norm;
+ (* facile *)
+ elim daemon
+ | intros;
+ unfold induced_norm;
+ (* difficile *)
+ elim daemon
+ ]
+ | intros;
+ unfold induced_norm in H;
+ apply irs_quotient_space1;
+ unfold minus;
+ rewrite < plus_comm;
+ rewrite < eq_zero_opp_zero;
+ rewrite > zero_neutral;
+ assumption
+ ].
+qed.
+
+definition distance_induced_by_integral ≝
+ λR:real.λV:integration_riesz_space R.
+ induced_distance ? ? (induced_norm R V).
+
+theorem distance_induced_by_integral_is_distance:
+ ∀R:real.∀V:integration_riesz_space R.
+ is_distance ? ? (distance_induced_by_integral ? V).
+ intros;
+ unfold distance_induced_by_integral;
+ apply induced_distance_is_distance;
+ apply induced_norm_is_norm.
+qed.
+