proposition: Lemma __admitted__interchange_sup (S : T -> U -> R) : (forall x, has_sup [set r | exists y, r = S x y]) -> has_sup [set r | exists x, r = sup [set r | exists y, r = S x y]] -> sup [set r | exists x, r = sup [set r | exists y, r = S x y]] = sup [set r | exists y, r == sup [set r | exists x, r = S x y]].
proof: Proof. Proof using Type. Admitted. End SupInterchange. #[deprecated(since="mathcomp-analysis 0.6.2", note="lacks proof, use __admitted__interchange_sup explicitly if you really want to use this lemma")] Notation interchange_sup := __admitted__interchange_sup. Section PSumInterchange. Context {R : realType} {T U : choiceType}. Lemma __admitted__interchange_psum (S : T -> U -> R) : (forall x, summable (S x)) -> summable (fun x => psum (fun y => S x y)) -> psum (fun x => psum (fun y => S x y)) = psum (fun y => psum (fun x => S x y)). Proof using Type. Admitted. End PSumInterchange. #[deprecated(since="mathcomp-analysis 0.6.2", note="lacks proof, use __admitted__interchange_psum explicitly if you really want to use this lemma")] Notation interchange_psum := __admitted__interchange_psum. Section SumTheory. Context {R : realType} {T : choiceType}. Implicit Types (S : T -> R). Lemma psum_sum S : (forall x, 0 <= S x) -> psum S = sum S. Proof. move=> ge0_S; rewrite /sum [X in _-X]psum_eq0 ?subr0. by move=> x; rewrite fneg_ge0. by apply/eq_psum=> x; rewrite fpos_ge0. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp) xfinmap ereal reals discrete realseq mathcomp.classical(classical_sets functions mathcomp_extra) topology